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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.