References

  1. Aws Albarghouthi, Arie Gurfinkel & Marsha Chechik (2012): Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. In: VMCAI, doi:10.1007/978-3-642-27940-9_4.
  2. Aws Albarghouthi, Yi Li, Arie Gurfinkel & Marsha Chechik (2012): Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. In: CAV, doi:10.1007/978-3-642-31424-7_48.
  3. Angelo Brillout, Daniel Kroening, Philipp Rümmer & Thomas Wahl (2010): An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. In: IJCAR, doi:10.1007/978-3-642-14203-1_33.
  4. Roberto Bruttomesso, Edgar Pek, Natasha Sharygina & Aliaksei Tsitovich (2010): The OpenSMT Solver. In: TACAS, doi:10.1007/978-3-642-12002-2_12.
  5. Jürgen Christ, Jochen Hoenicke & Alexander Nutz (2012): SMTInterpol: An Interpolating SMT Solver. In: SPIN, doi:10.1007/978-3-642-31759-0_19.
  6. Byron Cook, Andreas Podelski & Andrey Rybalchenko (2005): Abstraction Refinement for Termination. In: SAS, doi:10.1007/11547662_8.
  7. Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012): HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). In: TACAS, doi:10.1007/978-3-642-28756-5_46.
  8. Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012): Synthesizing software verifiers from proof rules. In: PLDI, doi:10.1145/2254064.2254112.
  9. Alberto Griggio, Thi Thieu Hoa Le & Roberto Sebastiani (2011): Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. In: TACAS, doi:10.1007/978-3-642-19835-9_13.
  10. Ashutosh Gupta (2011): Constraint solving for verification. TUM.
  11. Ashutosh Gupta, Corneliu Popeea & Andrey Rybalchenko (2011): Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL, doi:10.1145/1926385.1926424.
  12. Ashutosh Gupta, Corneliu Popeea & Andrey Rybalchenko (2011): Solving Recursion-Free Horn Clauses over LI+UIF. In: APLAS, doi:10.1007/978-3-642-25318-8_16.
  13. Ashutosh Gupta, Corneliu Popeea & Andrey Rybalchenko (2011): Threader: A Constraint-Based Verifier for Multi-threaded Programs. In: CAV, doi:10.1007/978-3-642-22110-1_32.
  14. Matthias Heizmann, Jochen Hoenicke & Andreas Podelski (2010): Nested interpolants. In: POPL, doi:10.1145/1706299.1706353.
  15. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar & Kenneth L. McMillan (2004): Abstractions from proofs. In: POPL, doi:10.1145/964001.964021.
  16. Krystof Hoder & Nikolaj Bjørner (2012): Generalized Property Directed Reachability. In: SAT, doi:10.1007/978-3-642-31612-8_13.
  17. Joxan Jaffar, Andrew E. Santosa & Razvan Voicu (2009): An Interpolation Method for CLP Traversal. In: CP, pp. 454–469, doi:10.1007/978-3-642-04244-7_37.
  18. Ranjit Jhala & Kenneth L. McMillan (2005): Interpolant-Based Transition Relation Approximation. In: CAV, doi:10.1007/11513988_6.
  19. Daniel Kroening & Georg Weissenbacher (2011): Interpolation-Based Software Verification with Wolverine. In: CAV, doi:10.1007/978-3-642-22110-1_45.
  20. Kenneth L. McMillan (2006): Lazy Abstraction with Interpolants. In: CAV, doi:10.1007/11817963_14.
  21. Andreas Podelski & Andrey Rybalchenko (2004): A Complete Method for the Synthesis of Linear Ranking Functions. In: VMCAI, doi:10.1007/978-3-540-24622-0_20.
  22. Corneliu Popeea & Andrey Rybalchenko (2012): Compositional Termination Proofs for Multi-threaded Programs. In: TACAS, doi:10.1007/978-3-642-28756-5_17.
  23. Philipp Rümmer, Hossein Hojjat & Viktor Kuncak (2013): Classifying and Solving Horn clauses for verification. In: VSTTE, doi:10.1007/978-3-642-54108-7_1.
  24. Ondrej Sery, Grigory Fedyukovich & Natasha Sharygina (2012): FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization. In: ATVA, doi:10.1007/978-3-642-33386-6_17.
  25. The Intelligent Systems Laboratory (2001): SICStus Prolog User's Manual. Swedish Institute of Computer Science. Release 3.8.7.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org