François Bourdoncle
ABSTRACT
Abstract interpretation is a formal method that enables the static determination (i.e. at compile-time) of the dynamic properties (i.e. at run-time) of programs. We present an abstract interpretation-based method, called abstract debugging, which enables the static and formal debugging of programs, prior to their execution, by finding the origin of potential bugs as well as necessary conditions for these bugs not to occur at run-time. We show how invariant assertions and intermittent assertions, such as termination, can be used to formally debug programs. Finally, we show how abstract debugging can be effectively and efficiently applied to higher-order imperative programs with exceptions and jumps to non-local labels, and present the Syntox system that enables the abstract debugging of the Pascal language by the determination of the range of the scalar variables of programs.
- 1.Alfred V. Aho, Ravi Sethi and Jeffrey D. Ullman: "Compilers m Principles, Techniques and Tools", Addison-Wesley Publishing Company (1986) Google Scholar
Digital Library
- 2.John P. Banning: "An Efficient Way to Find the Side Effects of Procedure Calls and the Aliases of Variables", Proc. of the 6th ACM Syrup. on POPL (1979) 29-41 Google ScholarDigital Library
- 3.Francois Bourdoncle: "Interprocedural Abstract Interpretation of Block Structured Languages with Nested Procedures, Aliasing and Recursivity", Proc. of the International Workshop PLILP'90, Lecture Notes in Computer Science 456, Springer- Verlag (1990) 307-323 Google ScholarDigital Library
- 4.Francois Bourdoncle: "Abstract Interpretation By Dynamic Partitioning", Journal of Functional Programming, Vol. 2, No. 4 (1992) 407-435Google ScholarCross Ref
- 5.Franqois Bourdoncle: "Sdmantiques des langages impdratifs d'ordre sup~rieur et interpretation abstraite", Ph.D. dissertation, Ecole Polytechnique (1992)Google Scholar
- 6.Franqois Bourdoncle: "Efficient Chaotic Iteration Strategies with Widenings", Proc. of the International Conf. on Formal Methods in Programming and their Applications, Lecture Notes in Computer Science, Springer-Verlag (1993) to appearGoogle Scholar
- 7.Keith D. Cooper: "Analyzing Aliases of Reference FoImal Parameters", Proc. of the 12th ACM Syrup. on POPL (1985) 281-290 Google ScholarDigital Library
- 8.Patrick and Radhia Cousot: "Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints", Proc. of the 4th ACM Syrup. on POPL (1977) 238-252 Google ScholarDigital Library
- 9.Patrick Cousot: "Asynchronous iterative methods for solving a fixpoint system of monotone equations", Research Report IMAG-RR-88, Universitd Scientifique et M~dicale de Grenoble (1977)Google Scholar
- 10.Patrick Cousot and Nicolas Halbwachs: "Automatic discovery of linear constraints among variables of a program", Proc. of the 5th ACM Syrup. on POPL (1978) 84-97 Google ScholarDigital Library
- 11.Patrick Cousot: "M~thodes it~ratives de construction et d'approximation de points fixes d'op~rateurs monotones sur un treillis. Analyse s~mantique de progranunes", Ph.D. dissertation, Universit6 Scientifique et M~dicale de Grenoble (1978)Google Scholar
- 12.Patrick and Radhia Cousot: "Static determination of dynamic properties of recursive procedures", Formal Description of Programming Concepts, North Holland Publishing Company (1978) 237-277Google Scholar
- 13.Patrick Cousot: "Semantic foundations of program analysis" in Muchnick and Jones Eds., Program Flow Analysis, Theory and Applications, Prentice-Hall (1981) 303-343Google Scholar
- 14.Alan J. Demers, Anne Neirynck and Prakash Panangaden: "Computation of Aliases and Support Sets", Proc. of the 14th ACM Syrup. on POPL (I987) 274-283 Google ScholarDigital Library
- 15.Alain Deutsch: "On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications'', Proc. of the 17th ACM Syrup. on POPL (1990) Google ScholarDigital Library
- 16.Alain Deutsch: "A Storeless Model of Aliasing and its Abstractions using Finite Representations of Right-Regular Equivalence Relations", Proc. of the IEEE'92 International Conf. on Computer Languages, IEEE Press (1992)Google Scholar
- 17.William H. Harrison: "Compiler Analysis of the Value Ranges for Variables", IEEE Transactions on software engineering, Vol. SE-3, No. 3, (1977) 243-250Google ScholarDigital Library
- 18.Rajiv Gupta: "A Fresh Look at Optimizing Array Bound Checking", Proc. of SIGPLAN '90 Conf. on Programming Language Design and Implementation (1990) 272-282 Google ScholarDigital Library
- 19.Neil D. Jones and Steven Muchnick: "A Flexible Approach to Interprocedural Data Flow Analysis and Programs with Recursive Data Structures", in Proc. of the 9th ACM Symp. on POPL (1982) Google ScholarDigital Library
- 20.William Landi and Barbara G. Ryder: "Pointer-induced Aliasing: A Problem Classification", Proc. of the 18th ACM Symp. on POPL (1991) 93-103 Google ScholarDigital Library
- 21.Victoria Markstein, John Cocke and Peter Markstein: "Optimization of Range Checking",Proc. of the SIGPLAN' 82 Syrup. on Compiler Construction (1982) 114-119 Google ScholarDigital Library
- 22.Jan Stransky: "A lattice for Abstract Interpretation of Dynamic (Lisp-like) Structures", Information and Computation 101 (1992) 70-102 Google ScholarDigital Library
- 23.Micha Shark and Amir Pnueli: "Two Approaches to Interprocedural Data Flow Analysis" in Muchnick and Jones Eds., Program Flow Analysis, Theory and Applications, Prentice- Hall (1981) 189-233Google Scholar
- 24.Andrew P. Tolmach and Andrew W. Appel: "Debugging Standard ML Without Reverse Engineering", Proc. 1990 ACM Conf. on Lisp and Functional Programming, ACM Press (1990) 1-12 Google ScholarDigital Library
- 25.G.A. Venkatesh and Charles N. Fisher: "SPARE: A Development Environment For Program Analysis Algorithms", IEEE Transactions on software engineering. Vol. 18. No. 4. (1992) 304-318 Google ScholarDigital Library
Index Terms
- Abstract debugging of higher-order imperative languages
Recommendations
Abstract debugging of higher-order imperative languages
Abstract interpretation is a formal method that enables the static determination (i.e. at compile-time) of the dynamic properties (i.e. at run-time) of programs. We present an abstract interpretation-based method, called abstract debugging, which ...
Pilsner: a compositionally verified compiler for a higher-order imperative language
ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional ProgrammingCompiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different ...
Debugging native extensions of dynamic languages
ManLang '18: Proceedings of the 15th International Conference on Managed Languages & RuntimesMany dynamic programming languages such as Ruby and Python enable developers to use so called native extensions, code implemented in typically statically compiled languages like C and C++. However, debuggers for these dynamic languages usually lack ...
Comments