References

  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 http://doi.acm.org/10.1145/876638.876643.
  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 http://doi.acm.org/10.1145/512950.512973.
  3. Patrick Cousot & Radhia Cousot (1977): Static Determination of Dynamic Properties of Generalized Type Unions. SIGPLAN Not. 12(3), pp. 77–94. Available at http://doi.acm.org/10.1145/390017.808314.
  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 https://doi.org/10.1007/978-3-319-96142-2_3.
  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 http://doi.acm.org/10.1145/1217975.1217981.
  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 http://doi.acm.org/10.1145/1637837.1637856.
  7. David Greve (2017): Generalization Correctness. http://www.cs.utexas.edu/users/moore/acl2/workshop-2017/slides-rump/greve-ACL2-2017.pdf.
  8. David Greve (2018): FuzzM: Fuzzing with Models. https://github.com/collins-research/FuzzM.
  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 http://dx.doi.org/10.1007/s10990-006-8609-1.
  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 http://dl.acm.org/citation.cfm?id=2485288.2485480.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org