@article(BagnaraHZ08SCP, author = "R. Bagnara and P. M. Hill and E. Zaffanella", year = "2008", title = "The {Parma Polyhedra Library}: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems", journal = "Science of Computer Programming", volume = "72", number = "1--2", pages = "3--21", url = "http://doi.acm.org/10.1016/j.scico.2007.08.001", ) @misc(BarST-SMT-10, author = "C. Barrett and A. Stump and C. Tinelli and S. Boehme and D. Cok and D. Deharbe and B. Dutertre and P. Fontaine and V. Ganesh and A. Griggio and J. Grundy and P. Jackson and A. Oliveras and S. Krsti\IeC {\'c} and M. Moskal and L. de Moura and R Sebastiani and T. D. Cok and J. Hoenicke", year = "2010", title = "C.: The SMT-LIB Standard: Version 2.0", url = "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.190.4897", ) @incollection(bjorner10, author = "N. Bj{\o }rner", year = "2010", title = "Linear Quantifier Elimination as an Abstract Decision Procedure", editor = "J{"u}rgen Giesl and Reiner H{"a}hnle", booktitle = "Automated Reasoning", series = "Lecture Notes in Computer Science", volume = "6173", publisher = "Springer Berlin / Heidelberg", pages = "316--330", url = "http://dx.doi.org/10.1007/978-3-642-14203-1\_27", ) @inproceedings(BlanchetEtAl-PLDI03, author = "B{.} Blanchet and P{.} Cousot and R{.} Cousot and J{.} Feret and L{.} Mauborgne and A{.} Min\'e and D{.} Monniaux and X{.} Rival", year = "2003", title = "A Static Analyzer for Large Safety-Critical Software", booktitle = "Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI'03)", publisher = "ACM Press", address = "San Diego, California, USA", pages = "196--207", url = "http://dx.doi.org/10.1145/781131.781153", ) @inproceedings(DBLP:conf/vmcai/Bradley11, author = "A. R. Bradley", year = "2011", title = "SAT-Based Model Checking without Unrolling", booktitle = "VMCAI", pages = "70--87", url = "http://dx.doi.org/10.1007/978-3-642-18275-4_7", ) @inproceedings(DBLP:conf/ictac/BradleyM06, author = "A. R. Bradley and Z. Manna", year = "2006", title = "Verification Constraint Problems with Strengthening", booktitle = "ICTAC", pages = "35--49", url = "http://dx.doi.org/10.1007/11921240_3", ) @inproceedings(DBLP:conf/popl/CaspiPHP87, author = "P. Caspi and D. Pilaud and N. Halbwachs and J. Plaice", year = "1987", title = "Lustre: A Declarative Language for Programming Synchronous Systems", booktitle = "POPL", pages = "178--188", url = "http://doi.acm.org/10.1145/41625.41641", ) @inproceedings(saeChampion, author = "A. Champion and R. Delmas and P.L. Garoche and P. Roux", year = "2011", title = "Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems", booktitle = "SAE Int. J. Aerosp.", pages = "850--858", url = "http://dx.doi.org/10.4271/2011-01-2558", ) @inproceedings(DBLP:conf/popl/CousotC77, author = "P. Cousot and R. Cousot", year = "1977", title = "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints", booktitle = "POPL", pages = "238--252", url = "http://doi.acm.org/10.1145/512950.512973", ) @inproceedings(DBLP:conf/atva/DammDHJPPSWW07, author = "Werner Damm and Stefan Disch and Hardi Hungar and Swen Jacobs and Jun Pang and Florian Pigorsch and Christoph Scholl and Uwe Waldmann and Boris Wirtz", year = "2007", title = "Exact State Set Representations in the Verification of Linear Hybr id Systems with Large Discrete State Space", booktitle = "ATVA", pages = "425--440", url = "http://dx.doi.org/10.1007/978-3-540-75596-8_30", ) @inproceedings(dierkes11, author = "M. Dierkes", year = "2011", title = "Formal Analysis of a Triplex Sensor Voter in an Industrial Context", editor = "G. Sala\"un and B. Sch\"atz", booktitle = "Proceedings of the 16th edition of FMICS", series = "LNCS", volume = "6959", publisher = "Springer", pages = "102--116", url = "http://dx.doi.org/10.1007/978-3-642-24431-5_9", ) @misc(dierkes2012, author = "M. Dierkes and D. K\"astner", year = "2012", title = "Transferring Stability Proof Obligations from Model Level to Code Level", url = "http://www.erts2012.org/Site/0P2RUC89/5C-1.pdf", ) @misc(een2011, author = "N. Een and A. Mishchenko and R. Brayton", year = "2011", title = "Efficient Implementation of Property Directed Reachability", url = "http://dl.acm.org/citation.cfm?id=2157675", ) @article(mathsat5, author = "A. Griggio", year = "2012", title = "{A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic}", journal = "JSAT", volume = "8", pages = "1--27", url = "http://jsat.ewi.tudelft.nl/content/volume8/JSAT8_1_Griggio.pdf", ) @article(DBLP:journals/fmsd/Jeannet03, author = "B. Jeannet", year = "2003", title = "Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems", journal = "Formal Methods in System Design", volume = "23", number = "1", pages = "5--37", url = "http://dx.doi.org/10.1023/A:1024480913162", ) @inproceedings(KahGT-NFM-11, author = "T. Kahsai and Y. Ge and C. Tinelli", year = "2011", title = "Instantiation-Based Invariant Discovery", editor = "M. Bobaru and K. Havelundand G. Holzmann and R. Joshi", booktitle = "Proceedings of the 3rd NASA Formal Methods Symposium (Pasadena, CA, USA)", series = "Lecture Notes in Computer Science", volume = "6617", publisher = "Springer", pages = "192--207", url = "http://dl.acm.org/citation.cfm?id=1986326", ) @inproceedings(DBLP:journals/corr/abs-1111-0372, author = "T. Kahsai and C. Tinelli", year = "2011", title = "{PK}ind: A parallel k-induction based model checker", booktitle = "PDMC", pages = "55--62", url = "http://dx.doi.org/10.4204/EPTCS.72.6", ) @inproceedings(DBLP:conf/tacas/McMillan08, author = "Kenneth L. McMillan", year = "2008", title = "Quantified Invariant Generation Using an Interpolating Saturation Prover", booktitle = "TACAS", pages = "413--427", url = "http://dx.doi.org/10.1007/978-3-540-78800-3_31", ) @inproceedings(DBLP:conf/lpar/Monniaux08, author = "D. Monniaux", year = "2008", title = "A Quantifier Elimination Algorithm for Linear Real Arithmetic", booktitle = "LPAR", pages = "243--257", url = "http://dx.doi.org/10.1007/978-3-540-89439-1_18", ) @inproceedings(DBLP:conf/tacas/MouraB08, author = "L. M. de Moura and N. Bj{\o }rner", year = "2008", title = "Z3: An Efficient {SMT} Solver", booktitle = "TACAS", pages = "337--340", url = "http://dx.doi.org/10.1007/978-3-540-78800-3_24", ) @inproceedings(DBLP:conf/cav/MouraRS03, author = "L. M. de Moura and H. Rue{\ss } and M. Sorea", year = "2003", title = "Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A)", booktitle = "CAV", pages = "14--26", url = "http://doi.acm.org/10.1007/978-3-540-45069-6_2", ) @article(Nipkow10, author = "T. Nipkow", year = "2010", title = "Linear Quantifier Elimination", journal = "J. Autom. Reasoning", volume = "45", number = "2", pages = "189--212", url = "http://dx.doi.org/10.1007/s10817-010-9183-0", ) @article(DBLP:journals/entcs/RouxDG10, author = "P. Roux and R. Delmas and P.L. Garoche", year = "2010", title = "SMT-AI: an Abstract Interpreter as Oracle for k-induction", journal = "Electr. Notes Theor. Comput. Sci.", volume = "267", number = "2", url = "http://dx.doi.org/10.1016/j.entcs.2010.09.018", ) @inproceedings(RouxGaroche2011, author = "P. Roux and R. Jobredeaux and P.L. Garoche and E. F{\'e}ron", year = "2012", title = "A generic ellipsoid abstract domain for linear time invariant systems", booktitle = "Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control", pages = "105--114", url = "http://doi.acm.org/10.1145/2185632.2185651", ) @inproceedings(DBLP:conf/fmcad/SheeranSS00, author = "M. Sheeran and S. Singh and G. St{\r a}lmarck", year = "2000", title = "Checking Safety Properties Using Induction and a {SAT}-Solver", booktitle = "FMCAD", pages = "108--125", url = "http://dx.doi.org/10.1007/3-540-40922-X_8", )