Jan Midtgaard
Flemming Nielson
ABSTRACT
We present an iterated approach to statically analyze programs of two processes communicating by message passing. Our analysis operates over a domain of lattice-valued regular expressions, and computes increasingly better approximations of each process's communication behavior. Overall the work extends traditional semantics-based program analysis techniques to automatically reason about message passing in a manner that can simultaneously analyze both values of variables as well as message order, message content, and their interdependencies.
- A. Aiken. Introduction to set constraint-based program analysis. SCP, 35(2-3):79--111, 1999. Google Scholar
Digital Library
- F. Bourdoncle. Abstract debugging of higher-order imperative languages. In PLDI'93, pages 46--55, 1993. Google ScholarDigital Library
- J. A. Brzozowski. Derivatives of regular expressions. Journal of the ACM, 11(4):481--494, 1964. Google ScholarDigital Library
- P. Cousot. Semantic foundations of program analysis. In Program Flow Analysis: Theory and Applications, chapter 10, pages 303--342. Prentice-Hall, 1981.Google Scholar
- P. Cousot. Abstracting induction by extrapolation and interpolation. In VMCAI'15, volume 8931 of LNCS, pages 19--42, 2015. Google ScholarDigital Library
- P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proc. of the Second International Symposium on Programming, pages 106--130, 1976.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'77, pages 238--252, 1977. Google ScholarDigital Library
- P. Cousot and R. Cousot. Semantic analysis of Communicating Sequential Processes. In ICALP'80, volume 85 of LNCS, pages 119--133, 1980. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2-3):103--179, 1992. Google ScholarDigital Library
- P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In PLILP'92, volume 631 of LNCS, pages 269--295, 1992. Google ScholarDigital Library
- B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002.Google ScholarCross Ref
- M. Dezani-Ciancaglini and U. de'Liguoro. Sessions and session types: An overview. In WS-FM'09, Revised Selected Papers, volume 6194 of LNCS, pages 1--28, 2009. Google ScholarDigital Library
- J. Feret. Confidentiality analysis of mobile systems. In SAS'00, volume 1824 of LNCS, pages 135--154, 2000. Google ScholarDigital Library
- J. Feret. Abstract interpretation-based static analysis of mobile ambients. In SAS'01, volume 2126 of LNCS, pages 412--430, 2001. Google ScholarDigital Library
- T. Freeman and F. Pfenning. Refinement types for ML. In PLDI'91, pages 268--277, 1991. Google ScholarDigital Library
- G. Grätzer. General Lattice Theory. Pure and Applied Mathematics. Academic Press, 1978.Google ScholarCross Ref
- N. Halbwachs. Delay analysis in synchronous programs. In CAV'93, volume 697 of LNCS, pages 333--346, 1993. Google ScholarDigital Library
- K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In POPL'08, pages 273--284, 2008. Google ScholarDigital Library
- T. Le Gall and B. Jeannet. Lattice automata: A representation for languages on infinite alphabets, and some applications to verification. In SAS'07, volume 4634 of LNCS, pages 52--68, 2007. Google ScholarDigital Library
- T. Le Gall, B. Jeannet, and T. Jéron. Verification of communication protocols using abstract interpretation of FIFO queues. In AMAST'06, volume 4019 of LNCS, pages 204--219, 2006. Google ScholarDigital Library
- F. Logozzo. Separate compositional analysis of class-based object-oriented languages. In AMAST'04, volume 3116 of LNCS, pages 334--348, 2004.Google Scholar
- J. Midtgaard, F. Nielson, and H. R. Nielson. A parametric abstract domain for lattice-valued regular expressions. In SAS'16, volume 9837 of LNCS, 2016.Google Scholar
- A. Miné. Relational thread-modular static value analysis by abstract interpretation. In VMCAI'14, volume 8318 of LNCS, pages 39--58, 2014. Google ScholarDigital Library
- D. Monniaux. A minimalistic look at widening operators. HOSC, 22(2):145--154, 2009. Google ScholarDigital Library
- F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer, 1999. Google ScholarDigital Library
- H. R. Nielson and F. Nielson. Flow logic: a multi-paradigmatic approach to static analysis. In The Essence of Computation: Complexity, Analysis, Transformation, volume 2566 of LNCS, pages 223--244, 2002. Google ScholarDigital Library
- P. M. Rondon, M. Kawaguci, and R. Jhala. Liquid types. In PLDI'08, pages 159--169, 2008. Google ScholarDigital Library
- R. Rydhof Hansen, J. G. Jensen, F. Nielson, and H. R. Nielson. Abstract interpretation of mobile ambients. In SAS'99, volume 1694 of LNCS, pages 134--148, 1999. Google ScholarDigital Library
- D. Sangiorgi. On the origins of bisimulation and coinduction. TOPLAS, 31(4), 2009. Google ScholarDigital Library
- V. T. Vasconcelos, S. Gay, and A. Ravara. Typechecking a multithreaded functional language with session types. TCS, 368(1-2):64--87, 2006. Google ScholarDigital Library
- A. Venet. Automatic determination of communication topologies in mobile systems. In SAS'98, volume 1503 of LNCS, pages 152--167, 1998. Google ScholarDigital Library
Index Terms
- Iterated process analysis over lattice-valued regular expressions
Recommendations
Pushdown control-flow analysis for free
POPL '16Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Pushdown control-flow analysis for free
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesTraditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Shape analysis in a functional language by using regular languages
Shape analysis is concerned with the compile-time determination of the 'shape' the heap may take at runtime, meaning by this the pointer chains that may happen within, and between, the data structures built by the program. This includes detecting alias ...
Comments