Bibliography

[All70]

Frances E. Allen. Control flow analysis. SIGPLAN Not., 5(7):1–19, July 1970.

[ALSU06]

Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison Wesley, 2006.

[AMN17]

Esben Sparre Andreasen, Anders Møller, and Benjamin Barslev Nielsen. Systematic approaches for increasing soundness and precision of static analyzers. In Proceedings of the 6th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis, SOAP@PLDI 2017, Barcelona, Spain, June 18, 2017, pages 31–36. ACM, 2017.

[And94]

Lars Ole Andersen. Program analysis and specialization for the C programming language. PhD thesis, University of Copenhagen, 1994.

[BR02]

Thomas Ball and Sriram K. Rajamani. The SLAM project: debugging system software via static analysis. In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002, pages 1–3. ACM, 2002.

[BS19]

Andrew Booker and Andrew Sutherland. Sum of three cubes for 42 finally solved – using real life planetary computer. https://www.bristol.ac.uk/news/2019/september/sum-of-three-cubes-.html, 2019.

[CC76]

Patrick Cousot and Radhia Cousot. Static determination of dynamic properties of programs. In Proceedings of the 2nd International Symposium on Programming, Paris, France, pages 106–130. Dunod, 1976.

[CC77]

Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pages 238–252. ACM, 1977.

[CC79a]

Patrick Cousot and Radhia Cousot. Constructive versions of Tarski’s fixed point theorems. Pacific Journal of Mathematics, 82(1):43–57, 1979.

[CC79b]

Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979, pages 269–282. ACM, 1979.

[CC92]

Patrick Cousot and Radhia Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In Programming Language Implementation and Logic Programming, 4th International Symposium, PLILP’92, Leuven, Belgium, August 26-28, 1992, Proceedings, volume 631 of Lecture Notes in Computer Science, pages 269–295. Springer, 1992.

[Cou77]

Patrick Cousot. Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Res. rep. R.R. 88, Laboratoire IMAG, Universite scientifique et m ´ edicale de ´ Grenoble, Grenoble, France, Sep. 1977. 15 p.

[CWZ90]

David R. Chase, Mark N. Wegman, and Frank Kenneth Zadeck. Analysis of pointers and structures. In Proceedings of the ACM SIGPLAN’90 Conference on Programming Language Design and Implementation (PLDI), White Plains, New York, USA, June 20-22, 1990, pages 296–310. ACM, 1990.

[Dam84]

Luis Damas. Type assignment in programming languages. PhD thesis, The University of Edinburgh, 1984.

[Dij70]

Edsger W. Dijkstra. Notes on structured programming. Technical Report EWD249, Technological University Eindhoven, 1970.

[FSDF93]

Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN’93 Conference on Programming Language Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June 23-25, 1993, pages 237–247. ACM, 1993.

[GF64]

Bernard A. Galler and Michael J. Fischer. An improved equivalence algorithm. Commun. ACM, 7(5):301–303, 1964.

[GLR15]

Roberto Giacobazzi, Francesco Logozzo, and Francesco Ranzato. Analyzing program analyses. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 261–273. ACM, 2015.

[GRS00]

Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361–416, 2000.

[Hec77]

Matthew S. Hecht. Flow Analysis of Computer Programs. Elsevier Science Inc., New York, NY, USA, 1977.

[Hen93]

Fritz Henglein. Type inference with polymorphic recursion. ACM Trans. Program. Lang. Syst., 15(2):253–289, 1993.

[Hin69]

Roger Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the american mathematical society, 146:29–60, 1969.

[JLB+15]

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 247–259. ACM, 2015.

[Kil73]

Gary A. Kildall. A unified approach to global program optimization. In Conference Record of the ACM Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, October 1973, pages 194–206. ACM, 1973.

[Kle52]

Stephen Cole Kleene. Introduction to Metamathematics. North-Holland Publ. Comp., Amsterdam, 1952.

[KTU90]

Assaf J. Kfoury, Jerzy Tiuryn, and Pawel Urzyczyn. ML typability is DEXPTIME-complete. In CAAP ’90, 15th Colloquium on Trees in Algebra and Programming, Copenhagen, Denmark, May 15-18, 1990, Proceedings, volume 431 of Lecture Notes in Computer Science, pages 206–220. Springer, 1990.

[KTU93]

Assaf J. Kfoury, Jerzy Tiuryn, and Pawel Urzyczyn. Type reconstruction in the presence of polymorphic recursion. ACM Trans. Program. Lang. Syst., 15(2):290–311, 1993.

[KU77]

John B. Kam and Jeffrey D. Ullman. Monotone data flow analysis frameworks. Acta Inf., 7:305–317, 1977.

[LSS+15]

Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondrej ˇ Lhotak, J Nelson Amaral, Bor-Yuh Evan Chang, Samuel Z Guyer, ´ Uday P Khedker, Anders Møller, and Dimitrios Vardoulakis. In defense of soundiness: A manifesto. Communications of the ACM, 58(2):44–46, 2015.

[Mai90]

Harry G. Mairson. Deciding ML typability is complete for deterministic exponential time. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, pages 382–401. ACM Press, 1990.

[Mil78]

Robin Milner. A theory of type polymorphism in programming. Journal of computer and system sciences, 17(3):348–375, 1978.

[Ric53]

Henry Gordon Rice. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 74(2):358–366, 1953.

[Roo19]

Eric Roosendaal. On the 3x + 1 problem. http://www.ericr.nl/wondrous/, 2019.

[SP81]

Micha Sharir and Amir Pnueli. Two approaches to interprocedural data flow analysis, chapter 7, pages 189–234. Prentice-Hall, 1981.

[Ste96]

Bjarne Steensgaard. Points-to analysis in almost linear time. In Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, pages 32–41. ACM, 1996.

[Tar55]

Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285–309, 1955.

[Tur37]

Alan Mathison Turing. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London mathematical society, 2(1):230–265, 1937.

[Wan87]

Mitchell Wand. A simple algorithm and proof for type inference. Fundamenta Informaticae, 10(2):115–121, 1987.