1. R. Bagnara, P. M. Hill & E. Zaffanella (2008): The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems. Science of Computer Programming 72(1–2), pp. 3–21. Available at
  2. C. Barrett, A. Stump, C. Tinelli, S. Boehme, D. Cok, D. Deharbe, B. Dutertre, P. Fontaine, V. Ganesh, A. Griggio, J. Grundy, P. Jackson, A. Oliveras, S. Krsti\'c, M. Moskal, L. de Moura, R Sebastiani, T. D. Cok & J. Hoenicke (2010): C.: The SMT-LIB Standard: Version 2.0. Available at
  3. N. Bjørner (2010): Linear Quantifier Elimination as an Abstract Decision Procedure. In: J"urgen Giesl & Reiner H"ahnle: Automated Reasoning, Lecture Notes in Computer Science 6173. Springer Berlin / Heidelberg, pp. 316–330. Available at
  4. B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux & X. Rival (2003): A Static Analyzer for Large Safety-Critical Software. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI'03). ACM Press, San Diego, California, USA, pp. 196–207. Available at
  5. A. R. Bradley (2011): SAT-Based Model Checking without Unrolling. In: VMCAI, pp. 70–87. Available at
  6. A. R. Bradley & Z. Manna (2006): Verification Constraint Problems with Strengthening. In: ICTAC, pp. 35–49. Available at
  7. P. Caspi, D. Pilaud, N. Halbwachs & J. Plaice (1987): Lustre: A Declarative Language for Programming Synchronous Systems. In: POPL, pp. 178–188. Available at
  8. A. Champion, R. Delmas, P.L. Garoche & P. Roux (2011): Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems. In: SAE Int. J. Aerosp., pp. 850–858. Available at
  9. P. Cousot & R. Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: POPL, pp. 238–252. Available at
  10. Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann & Boris Wirtz (2007): Exact State Set Representations in the Verification of Linear Hybr id Systems with Large Discrete State Space. In: ATVA, pp. 425–440. Available at
  11. M. Dierkes (2011): Formal Analysis of a Triplex Sensor Voter in an Industrial Context. In: G. Salaün & B. Schätz: Proceedings of the 16th edition of FMICS, LNCS 6959. Springer, pp. 102–116. Available at
  12. M. Dierkes & D. Kästner (2012): Transferring Stability Proof Obligations from Model Level to Code Level. Available at
  13. N. Een, A. Mishchenko & R. Brayton (2011): Efficient Implementation of Property Directed Reachability. Available at
  14. A. Griggio (2012): A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. JSAT 8, pp. 1–27. Available at
  15. B. Jeannet (2003): Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems. Formal Methods in System Design 23(1), pp. 5–37. Available at
  16. T. Kahsai, Y. Ge & C. Tinelli (2011): Instantiation-Based Invariant Discovery. In: M. Bobaru, K. Havelundand G. Holzmann & R. Joshi: Proceedings of the 3rd NASA Formal Methods Symposium (Pasadena, CA, USA), Lecture Notes in Computer Science 6617. Springer, pp. 192–207. Available at
  17. T. Kahsai & C. Tinelli (2011): PKind: A parallel k-induction based model checker. In: PDMC, pp. 55–62. Available at
  18. Kenneth L. McMillan (2008): Quantified Invariant Generation Using an Interpolating Saturation Prover. In: TACAS, pp. 413–427. Available at
  19. D. Monniaux (2008): A Quantifier Elimination Algorithm for Linear Real Arithmetic. In: LPAR, pp. 243–257. Available at
  20. L. M. de Moura & N. Bjørner (2008): Z3: An Efficient SMT Solver. In: TACAS, pp. 337–340. Available at
  21. L. M. de Moura, H. Rueß & M. Sorea (2003): Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A). In: CAV, pp. 14–26. Available at
  22. T. Nipkow (2010): Linear Quantifier Elimination. J. Autom. Reasoning 45(2), pp. 189–212. Available at
  23. P. Roux, R. Delmas & P.L. Garoche (2010): SMT-AI: an Abstract Interpreter as Oracle for k-induction. Electr. Notes Theor. Comput. Sci. 267(2). Available at
  24. P. Roux, R. Jobredeaux, P.L. Garoche & E. Féron (2012): A generic ellipsoid abstract domain for linear time invariant systems. In: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, pp. 105–114. Available at
  25. M. Sheeran, S. Singh & G. Stålmarck (2000): Checking Safety Properties Using Induction and a SAT-Solver. In: FMCAD, pp. 108–125. Available at

Comments and questions to:
For website issues: