[1] Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holik, Ahmed
Rezine, Philipp Rümmer, and Jari Stenman.
String constraints for verification.
In
CAV, pages 150–166, 2014.
🔎
[2] Aws Albarghouthi and Kenneth L. McMillan.
Beautiful interpolants.
In
CAV, pages 313–329, 2013.
🔎
[3] Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, and
Natasha Sharygina.
Safari: Smt-based abstraction for arrays with interpolants.
In
CAV, pages 679–685, 2012.
🔎
[4] Sam Bayless, Celina Val, Thomas Ball, Holger Hoos, and Alan Hu.
Efficient Modular SAT Solving for IC3.
2013.
🔎
[5] Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, and
Christoph M. Wintersteiger.
Resourceful reachability as horn-la.
In
LPAR, pages 137–146, 2013.
🔎
[6] Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko.
A constraint-based approach to solving games on infinite graphs.
In
POPL, pages 221–234, 2014.
🔎
[7] Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko.
Program verification as satisfiability modulo theories.
In
SMT@IJCAR, pages 3–11, 2012.
🔎
[8] Nikolaj Bjørner, Arie Gurfinkel, Konstantin Korovin, and Ori Lahav.
Instantiations, Zippers and EPR Interpolation.
In
Short paper at LPAR 19, 2013a.
🔎
[9] Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko.
On solving universally quantified horn clauses.
In
SAS, pages 105–125, 2013b.
🔎
[10] Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko.
Higher-order program verification as satisfiability modulo theories
with algebraic data-types.
CoRR, abs/1306.5264, 2013c.
🔎
[11] Aaron R. Bradley.
SAT-Based Model Checking without Unrolling.
In
VMCAI, pages 70–87, 2011.
🔎
[12] Hana Chockler, Alexander Ivrii, and Arie Matsliah.
Computing interpolants without proofs.
In Armin Biere, Amir Nahir, and Tanja Vos, editors,
Hardware
and Software: Verification and Testing, volume 7857 of
Lecture Notes
in Computer Science, pages 72–85. Springer Berlin Heidelberg, 2013.
🔎
[13] Alessandro Cimatti and Alberto Griggio.
Software Model Checking via IC3.
In
CAV, pages 277–293, 2012.
🔎
[14] Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta.
Parameter synthesis with ic3.
In
FMCAD, pages 165–168, 2013.
🔎
[15] Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta.
IC3 Modulo Theories via Implicit Predicate Abstraction.
In
TACAS, pages 46–61, 2014.
🔎
[16] Niklas Eén, Alan Mishchenko, and Robert K. Brayton.
Efficient implementation of property directed reachability.
In
FMCAD, pages 125–134, 2011.
🔎
[17] Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko.
Synthesizing software verifiers from proof rules.
In
PLDI, 2012.
🔎
[18] Arie Gurfinkel, Anton Belov, and Joao Marques-Silva.
Synthesizing safe bit-precise invariants.
In
TACAS, pages 93–108, 2014.
🔎
[19] Krystof Hoder and Nikolaj Bjørner.
Generalized Property Directed Reachability.
In
SAT, pages 157–171, 2012.
🔎
[20] Shachar Itzhaky, Nikolaj Bjørner, Thomas W. Reps, Mooly Sagiv, and Aditya V.
Thakur.
Property-directed shape analysis.
In
CAV, pages 35–51, 2014.
🔎
[21] Roland Kindermann, Tommi A. Junttila, and Ilkka Niemelä.
SMT-Based Induction Methods for Timed Systems.
In
FORMATS, pages 171–187, 2012.
🔎
[22] Johannes Kloos, Rupak Majumdar, Filip Niksic, and Ruzica Piskac.
Incremental, inductive coverability.
In
CAV, pages 158–173, 2013.
🔎
[23] Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, and Edmund M. Clarke.
Automatic Abstraction in SMT-Based Unbounded Software Model
Checking.
In
CAV, pages 846–862, 2013.
🔎
[24] Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki.
Smt-based model checking for recursive programs.
In
CAV, pages 17–34, 2014.
🔎
[25] Kenneth L. McMillan.
Lazy annotation revisited.
In
CAV, pages 243–259, 2014.
🔎
[26] Philipp Rümmer, Hossein Hojjat, and Viktor Kuncak.
Disjunctive interpolants for horn-clause verification.
In
CAV, pages 347–363, 2013.
🔎