@inproceedings(AlbarghouthiVMCAI12,
 author       = "Aws Albarghouthi and Arie Gurfinkel and Marsha Chechik",
 year         = "2012",
 title        = "Whale: An Interpolation-Based Algorithm for Inter-procedural Verification",
 booktitle    = "VMCAI",
 doi          = "10.1007/978-3-642-27940-9\_4",
)
@inproceedings(AlbarghouthiCAV12,
 author       = "Aws Albarghouthi and Yi Li and Arie Gurfinkel and Marsha Chechik",
 year         = "2012",
 title        = "Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification",
 booktitle    = "CAV",
 doi          = "10.1007/978-3-642-31424-7\_48",
)
@inproceedings(PrincessIJCAR10,
 author       = "Angelo Brillout and Daniel Kroening and Philipp R{\"u}mmer and Thomas Wahl",
 year         = "2010",
 title        = "An Interpolating Sequent Calculus for Quantifier-Free {P}resburger Arithmetic",
 booktitle    = "IJCAR",
 doi          = "10.1007/978-3-642-14203-1\_33",
)
@inproceedings(OpenSmtTACAS10,
 author       = "Roberto Bruttomesso and Edgar Pek and Natasha Sharygina and Aliaksei Tsitovich",
 year         = "2010",
 title        = "The {OpenSMT} Solver",
 booktitle    = "TACAS",
 doi          = "10.1007/978-3-642-12002-2\_12",
)
@inproceedings(HoenickeSPIN12,
 author       = "J{\"u}rgen Christ and Jochen Hoenicke and Alexander Nutz",
 year         = "2012",
 title        = "SMTInterpol: An Interpolating {SMT} Solver",
 booktitle    = "SPIN",
 doi          = "10.1007/978-3-642-31759-0\_19",
)
@inproceedings(SAS05,
 author       = "Byron Cook and Andreas Podelski and Andrey Rybalchenko",
 year         = "2005",
 title        = "Abstraction Refinement for Termination",
 booktitle    = "SAS",
 doi          = "10.1007/11547662\_8",
)
@inproceedings(SVCOMP12,
 author       = "Sergey Grebenshchikov and Ashutosh Gupta and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko",
 year         = "2012",
 title        = "{HSF(C)}: A Software Verifier Based on {Horn} Clauses - (Competition Contribution)",
 booktitle    = "TACAS",
 doi          = "10.1007/978-3-642-28756-5\_46",
)
@inproceedings(PLDI12,
 author       = "Sergey Grebenshchikov and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko",
 year         = "2012",
 title        = "Synthesizing software verifiers from proof rules",
 booktitle    = "PLDI",
 doi          = "10.1145/2254064.2254112",
)
@inproceedings(GriggioTACAS11,
 author       = "Alberto Griggio and Thi Thieu Hoa Le and Roberto Sebastiani",
 year         = "2011",
 title        = "Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic",
 booktitle    = "TACAS",
 doi          = "10.1007/978-3-642-19835-9\_13",
)
@phdthesis(GuptaPhD,
 author       = "Ashutosh Gupta",
 year         = "2011",
 title        = "Constraint solving for verification",
 school       = "TUM",
)
@inproceedings(POPL11,
 author       = "Ashutosh Gupta and Corneliu Popeea and Andrey Rybalchenko",
 year         = "2011",
 title        = "Predicate abstraction and refinement for verifying multi-threaded programs",
 booktitle    = "POPL",
 doi          = "10.1145/1926385.1926424",
)
@inproceedings(APLAS11,
 author       = "Ashutosh Gupta and Corneliu Popeea and Andrey Rybalchenko",
 year         = "2011",
 title        = "Solving Recursion-Free {Horn} Clauses over {LI+UIF}",
 booktitle    = "APLAS",
 doi          = "10.1007/978-3-642-25318-8\_16",
)
@inproceedings(CAV11,
 author       = "Ashutosh Gupta and Corneliu Popeea and Andrey Rybalchenko",
 year         = "2011",
 title        = "Threader: A Constraint-Based Verifier for Multi-threaded Programs",
 booktitle    = "CAV",
 doi          = "10.1007/978-3-642-22110-1\_32",
)
@inproceedings(HeizmannPOPL10,
 author       = "Matthias Heizmann and Jochen Hoenicke and Andreas Podelski",
 year         = "2010",
 title        = "Nested interpolants",
 booktitle    = "POPL",
 doi          = "10.1145/1706299.1706353",
)
@inproceedings(JhalaPOPL04,
 author       = "Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and Kenneth L. McMillan",
 year         = "2004",
 title        = "Abstractions from proofs",
 booktitle    = "POPL",
 doi          = "10.1145/964001.964021",
)
@inproceedings(GenPDRSAT12,
 author       = "Krystof Hoder and Nikolaj Bj{\o }rner",
 year         = "2012",
 title        = "Generalized Property Directed Reachability",
 booktitle    = "SAT",
 doi          = "10.1007/978-3-642-31612-8\_13",
)
@inproceedings(JaffarCP09,
 author       = "Joxan Jaffar and Andrew E. Santosa and Razvan Voicu",
 year         = "2009",
 title        = "An Interpolation Method for {CLP} Traversal",
 booktitle    = "CP",
 pages        = "454--469",
 doi          = "10.1007/978-3-642-04244-7\_37",
)
@inproceedings(JhalaCAV05,
 author       = "Ranjit Jhala and Kenneth L. McMillan",
 year         = "2005",
 title        = "Interpolant-Based Transition Relation Approximation",
 booktitle    = "CAV",
 doi          = "10.1007/11513988\_6",
)
@inproceedings(WeissenbacherCAV11,
 author       = "Daniel Kroening and Georg Weissenbacher",
 year         = "2011",
 title        = "Interpolation-Based Software Verification with {Wolverine}",
 booktitle    = "CAV",
 doi          = "10.1007/978-3-642-22110-1\_45",
)
@inproceedings(McMillanCAV06,
 author       = "Kenneth L. McMillan",
 year         = "2006",
 title        = "Lazy Abstraction with Interpolants",
 booktitle    = "CAV",
 doi          = "10.1007/11817963\_14",
)
@inproceedings(VMCAI04,
 author       = "Andreas Podelski and Andrey Rybalchenko",
 year         = "2004",
 title        = "A Complete Method for the Synthesis of Linear Ranking Functions",
 booktitle    = "VMCAI",
 doi          = "10.1007/978-3-540-24622-0\_20",
)
@inproceedings(TACAS12,
 author       = "Corneliu Popeea and Andrey Rybalchenko",
 year         = "2012",
 title        = "Compositional Termination Proofs for Multi-threaded Programs",
 booktitle    = "TACAS",
 doi          = "10.1007/978-3-642-28756-5\_17",
)
@inproceedings(RummerVSTTE13,
 author       = "Philipp R{\"u}mmer and Hossein Hojjat and Viktor Kuncak",
 year         = "2013",
 title        = "Classifying and Solving {H}orn clauses for verification",
 booktitle    = "VSTTE",
 doi          = "10.1007/978-3-642-54108-7\_1",
)
@inproceedings(SharyginaATVA12,
 author       = "Ondrej Sery and Grigory Fedyukovich and Natasha Sharygina",
 year         = "2012",
 title        = "{FunFrog}: Bounded Model Checking with Interpolation-Based Function Summarization",
 booktitle    = "ATVA",
 doi          = "10.1007/978-3-642-33386-6\_17",
)
@manual(sicstus,
 author       = "{The Intelligent Systems Laboratory}",
 year         = "2001",
 title        = "SICStus Prolog User's Manual",
 organization = "Swedish Institute of Computer Science",
 note         = "Release 3.8.7",
)