References

  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 http://doi.acm.org/10.1016/j.scico.2007.08.001.
  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 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.190.4897.
  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 http://dx.doi.org/10.1007/978-3-642-14203-1_27.
  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 http://dx.doi.org/10.1145/781131.781153.
  5. A. R. Bradley (2011): SAT-Based Model Checking without Unrolling. In: VMCAI, pp. 70–87. Available at http://dx.doi.org/10.1007/978-3-642-18275-4_7.
  6. A. R. Bradley & Z. Manna (2006): Verification Constraint Problems with Strengthening. In: ICTAC, pp. 35–49. Available at http://dx.doi.org/10.1007/11921240_3.
  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 http://doi.acm.org/10.1145/41625.41641.
  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 http://dx.doi.org/10.4271/2011-01-2558.
  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 http://doi.acm.org/10.1145/512950.512973.
  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 http://dx.doi.org/10.1007/978-3-540-75596-8_30.
  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 http://dx.doi.org/10.1007/978-3-642-24431-5_9.
  12. M. Dierkes & D. Kästner (2012): Transferring Stability Proof Obligations from Model Level to Code Level. Available at http://www.erts2012.org/Site/0P2RUC89/5C-1.pdf.
  13. N. Een, A. Mishchenko & R. Brayton (2011): Efficient Implementation of Property Directed Reachability. Available at http://dl.acm.org/citation.cfm?id=2157675.
  14. A. Griggio (2012): A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. JSAT 8, pp. 1–27. Available at http://jsat.ewi.tudelft.nl/content/volume8/JSAT8_1_Griggio.pdf.
  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 http://dx.doi.org/10.1023/A:1024480913162.
  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 http://dl.acm.org/citation.cfm?id=1986326.
  17. T. Kahsai & C. Tinelli (2011): PKind: A parallel k-induction based model checker. In: PDMC, pp. 55–62. Available at http://dx.doi.org/10.4204/EPTCS.72.6.
  18. Kenneth L. McMillan (2008): Quantified Invariant Generation Using an Interpolating Saturation Prover. In: TACAS, pp. 413–427. Available at http://dx.doi.org/10.1007/978-3-540-78800-3_31.
  19. D. Monniaux (2008): A Quantifier Elimination Algorithm for Linear Real Arithmetic. In: LPAR, pp. 243–257. Available at http://dx.doi.org/10.1007/978-3-540-89439-1_18.
  20. L. M. de Moura & N. Bjørner (2008): Z3: An Efficient SMT Solver. In: TACAS, pp. 337–340. Available at http://dx.doi.org/10.1007/978-3-540-78800-3_24.
  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 http://doi.acm.org/10.1007/978-3-540-45069-6_2.
  22. T. Nipkow (2010): Linear Quantifier Elimination. J. Autom. Reasoning 45(2), pp. 189–212. Available at http://dx.doi.org/10.1007/s10817-010-9183-0.
  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 http://dx.doi.org/10.1016/j.entcs.2010.09.018.
  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 http://doi.acm.org/10.1145/2185632.2185651.
  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 http://dx.doi.org/10.1007/3-540-40922-X_8.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org