1. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu & Helmut Veith (2003): Counterexample-guided Abstraction Refinement for Symbolic Model Checking. J. ACM 50(5), pp. 752–794. Available at
  2. Patrick Cousot & Radhia Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '77. ACM, New York, NY, USA, pp. 238–252. Available at
  3. Patrick Cousot & Radhia Cousot (1977): Static Determination of Dynamic Properties of Generalized Type Unions. SIGPLAN Not. 12(3), pp. 77–94. Available at
  4. Andrew Gacek, John Backes, Mike Whalen, Lucas G. Wagner & Elaheh Ghassabani (2018): The JKind Model Checker. In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, pp. 20–27. Available at
  5. David Greve (2006): Parameterized Congruences in ACL2. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 '06. ACM, New York, NY, USA, pp. 28–34. Available at
  6. David Greve (2009): Assuming Termination. In: Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 '09. ACM, New York, NY, USA, pp. 114–122. Available at
  7. David Greve (2017): Generalization Correctness.
  8. David Greve (2018): FuzzM: Fuzzing with Models.
  9. David Greve & Konrad Slind (2013): A Step-Indexing Approach to Partial Functions. In: Ruben Gamboa & Jared Davis: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, Laramie, Wyoming, USA , May 30-31, 2013, Electronic Proceedings in Theoretical Computer Science 114. Open Publishing Association, pp. 42–53, doi:10.4204/EPTCS.114.4.
  10. N. Halbwachs, P. Caspi, P. Raymond & D. Pilaud (1991): The synchronous data flow programming language LUSTRE. Proceedings of the IEEE 79(9), pp. 1305–1320, doi:10.1109/5.97300.
  11. Antoine Miné (2006): The Octagon Abstract Domain. Higher Order Symbol. Comput. 19(1), pp. 31–100. Available at
  12. Tobias Welp & Andreas Kuehlmann (2013): QF_BV Model Checking with Property Directed Reachability. In: Proceedings of the Conference on Design, Automation and Test in Europe, DATE '13. EDA Consortium, San Jose, CA, USA, pp. 791–796. Available at

Comments and questions to:
For website issues: