@misc(MAP,
 title        = "The MAP transformation system",
 note         = "Available at \texttt {www.iasi.cnr.it/\~{}proietti/system.html}",
)
@inproceedings(AGCSAS12,
 author       = "Aws Albarghouthi and Arie Gurfinkel and Marsha Chechik",
 year         = "2012",
 title        = "Craig Interpretation",
 booktitle    = "Proceedings of SAS",
 pages        = "300--316",
 doi          = "10.1007/978-3-642-33125-1_21",
)
@inproceedings(AlbarghouthiGC12,
 author       = "Aws Albarghouthi and Arie Gurfinkel and Marsha Chechik",
 year         = "2012",
 title        = "From Under-Approximations to Over-Approximations and Back",
 booktitle    = "Proceedings of TACAS",
 pages        = "157--172",
 doi          = "10.1007/978-3-642-28756-5_12",
)
@inproceedings(AlbarghouthiLGC12,
 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    = "Proceedings of CAV",
 pages        = "672--678",
 doi          = "10.1007/978-3-642-31424-7_48",
)
@inproceedings(AlbertGHP07,
 author       = "Elvira Albert and Miguel G{\'o}mez-Zamalloa and Laurent Hubert and Germ{\'a}n Puebla",
 year         = "2007",
 title        = "Verification of Java Bytecode Using Analysis and Transformation of Logic Programs",
 booktitle    = "Proceedings of PADL",
 pages        = "124--139",
 doi          = "10.1007/978-3-540-69611-7_8",
)
@article(Bag&08,
 author       = "Roberto Bagnara and Patricia M. Hill and E.nea Zaffanella",
 year         = "2008",
 title        = "The {P}arma {P}olyhedra {L}ibrary: {T}oward 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",
 doi          = "10.1016/j.scico.2007.08.001",
)
@inproceedings(Beyer13,
 author       = "Dirk Beyer",
 year         = "2013",
 title        = "Competition on Software Verification - (SV-COMP)",
 booktitle    = "Proceedings of TACAS",
 pages        = "594--609",
 doi          = "10.1007/978-3-642-36742-7_43",
)
@inproceedings(BjornerMR12,
 author       = "Nikolaj Bj{\o }rner and Kenneth McMillan and Andrey Rybalchenko",
 year         = "2012",
 title        = "Program Verification as Satisfiability Modulo Theories",
 booktitle    = "Proceedings of SMT",
 pages        = "3--11",
)
@inproceedings(Bradley11,
 author       = "Aaron R. Bradley",
 year         = "2011",
 title        = "SAT-Based Model Checking without Unrolling",
 booktitle    = "Proceedings of VMCAI",
 series       = "LNCS 6538",
 publisher    = "Springer",
 pages        = "70--87",
 doi          = "10.1007/978-3-642-18275-4_7",
)
@inproceedings(GuzmanCHS12,
 author       = "P. {Chico de Guzm{\'a}n} and M. Carro and M. V. Hermenegildo and P. J. Stuckey",
 year         = "2012",
 title        = "A General Implementation Framework for Tabled {CLP}",
 booktitle    = "Proceedings of FLOPS",
 pages        = "104--119",
 doi          = "10.1007/978-3-642-29822-6_11",
)
@inproceedings(mathsat5,
 author       = "Alessandro Cimatti and Alberto Griggio and Bastiaan Schaafsma and Roberto Sebastiani",
 year         = "2013",
 title        = "{The MathSAT5 SMT Solver}",
 editor       = "Nir Piterman and Scott Smolka",
 booktitle    = "Proceedings of TACAS",
 series       = "LNCS",
 volume       = "7795",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-36742-7_7",
)
@inproceedings(Codognet95,
 author       = "Philippe Codognet",
 year         = "1995",
 title        = "A Tabulation Method for Constraint Logic Programming",
 booktitle    = "Symposium and Exhibition on Industrial Applications of Prolog",
)
@inproceedings(Cousot_POPL77,
 author       = "Patrick Cousot and Radhia Cousot",
 year         = "1977",
 title        = "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints",
 booktitle    = "Proceedings of POPL",
 publisher    = "ACM",
 pages        = "238--252",
 doi          = "10.1145/512950.512973",
)
@article(interpolant,
 author       = "W. Craig",
 year         = "1957",
 title        = "Linear Reasoning: A New Form of the {Herbrand-Gentzen} Theorem",
 journal      = "Journal of Symbolic Logic",
 volume       = "22",
 number       = "3",
 pages        = "250--268",
 doi          = "10.2307/2963593",
)
@inproceedings(DeAngelisFPP12b,
 author       = "Emanuele {De Angelis} and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti",
 year         = "2013",
 title        = "Specialization with Constrained Generalization for Software Model Checking",
 booktitle    = "Proceedings of LOPSTR",
 series       = "LNCS 7844",
 publisher    = "Springer",
 pages        = "51--70",
 doi          = "10.1007/978-3-642-38197-3\_5",
)
@article(De&14c,
 author       = "Emanuele {De Angelis} and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti",
 year         = "2014",
 title        = "Program Verification via Iterated Specialization",
 journal      = "Science of Computer Programming (Special Issue on PEPM 2013)",
 doi          = "10.1016/j.scico.2014.05.017",
)
@inproceedings(DeAngelisFPP14,
 author       = "Emanuele {De Angelis} and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti",
 year         = "2014",
 title        = "VeriMAP: {A} Tool for Verifying Programs through Transformations",
 booktitle    = "Proceedings of TACAS",
 pages        = "568--574",
 doi          = "10.1007/978-3-642-54862-8_47",
)
@inproceedings(Du&13,
 author       = "Gregory J. Duck and Joxan Jaffar and Nicolas C. H. Koh",
 year         = "2013",
 title        = "Constraint-Based Program Reasoning with Heaps and Separation",
 booktitle    = "Proceedings of {CP}",
 series       = "LNCS 8124",
 publisher    = "Springer",
 pages        = "282--298",
 doi          = "10.1007/978-3-642-40627-0_24",
)
@article(EtG96,
 author       = "Sandro Etalle and Maurizio Gabbrielli",
 year         = "1996",
 title        = "Transformations of CLP Modules",
 journal      = "Theoretical Computer Science",
 volume       = "166",
 number       = "1{\&}2",
 pages        = "101--146",
 doi          = "10.1016/0304-3975(95)00148-4",
)
@inproceedings(Fi&00b,
 author       = "Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti",
 year         = "2000",
 title        = "Automated strategies for specializing constraint logic programs",
 booktitle    = "Proceedings of LOPSTR",
 doi          = "10.1007/3-540-45142-0_8",
)
@article(Fi&13a,
 author       = "Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti and Valerio Senni",
 year         = "2013",
 title        = "Generalization Strategies for the Verification of Infinite State Systems",
 journal      = "Theory and Practice of Logic Programming",
 volume       = "13",
 number       = "2",
 pages        = "175--199",
 doi          = "10.1017/S1471068411000627",
)
@inproceedings(GaK14,
 author       = "John P. Gallagher and Bishoksan Kafle",
 year         = "2014",
 title        = "Analysis and Transformation Tools for Constrained Horn Clause Verification",
 booktitle    = "Proceedings of ICLP (to appear)",
)
@article(GangeNSSS13,
 author       = "Graeme Gange and Jorge A. Navas and Peter Schachte and Harald S{\o }ndergaard and Peter J. Stuckey",
 year         = "2013",
 title        = "Failure tabled constraint logic programming by interpolation",
 journal      = "Theory and Practice of Logic Programming",
 volume       = "13",
 number       = "4-5",
 pages        = "593--607",
 doi          = "10.1017/S1471068413000379",
)
@inproceedings(GrebenshchikovLPR12,
 author       = "Sergey Grebenshchikov and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko",
 year         = "2012",
 title        = "Synthesizing Software Verifiers from Proof Rules",
 booktitle    = "Proceedings of PLDI",
 pages        = "405--416",
 doi          = "10.1145/2254064.2254112",
)
@inproceedings(DAGGER08,
 author       = "Bhargav S. Gulavani and Supratik Chakraborty and Aditya V. Nori and Sriram K. Rajamani",
 year         = "2008",
 title        = "Automatically Refining Abstract Interpretations",
 booktitle    = "Proceedings of TACAS",
 pages        = "443--458",
 doi          = "10.1007/978-3-540-78800-3_33",
)
@inproceedings(GulavaniR06,
 author       = "Bhargav S. Gulavani and Sriram K. Rajamani",
 year         = "2006",
 title        = "Counterexample Driven Refinement for Abstract Interpretation",
 booktitle    = "Proceedings of TACAS",
 pages        = "474--488",
 doi          = "10.1007/11691372_34",
)
@inproceedings(GuptaR09,
 author       = "Ashutosh Gupta and Andrey Rybalchenko",
 year         = "2009",
 title        = "InvGen: An Efficient Invariant Generator",
 booktitle    = "Proceedings of CAV",
 pages        = "634--640",
 doi          = "10.1007/978-3-642-02658-4_48",
)
@article(HalbwachsPR97,
 author       = "Nicolas Halbwachs and Yann-Erick Proy and Patrick Roumanoff",
 year         = "1997",
 title        = "Verification of Real-Time Systems using Linear Relation Analysis",
 journal      = "Formal Methods in System Design",
 volume       = "11",
 number       = "2",
 pages        = "157--185",
 doi          = "10.1023/A:1008678014487",
)
@inproceedings(HoderBM11,
 author       = "Krystof Hoder and Nikolaj Bj{\o }rner and Leonardo Mendon\c {c}a de Moura",
 year         = "2011",
 title        = "$\mu Z$ - An Efficient Engine for Fixed Points with Constraints",
 booktitle    = "Proceedings of CAV",
 pages        = "457--462",
 doi          = "10.1007/978-3-642-22110-1_36",
)
@inproceedings(JaffarL87,
 author       = "J. Jaffar and J. Lassez",
 year         = "1987",
 title        = "Constraint Logic Programming",
 booktitle    = "Proceedings of POPL",
 pages        = "111--119",
 doi          = "10.1145/41625.41635",
)
@inproceedings(JaffarSV09,
 author       = "J. Jaffar and A. E. Santosa and R. Voicu",
 year         = "2009",
 title        = "An Interpolation Method for {CLP} Traversal",
 booktitle    = "Proceedings of CP",
 pages        = "454--469",
 doi          = "10.1007/978-3-642-04244-7_37",
)
@inproceedings(JaffarMNS12,
 author       = "Joxan Jaffar and Vijayaraghavan Murali and Jorge A. Navas and Andrew E. Santosa",
 year         = "2012",
 title        = "{TRACER}: {A} Symbolic Execution Tool for Verification",
 booktitle    = "Proceedings of CAV",
 pages        = "758--766",
 doi          = "10.1007/978-3-642-31424-7_61",
)
@techreport(Duality,
 author       = "Kenneth McMillan and Andrey Rybalchenko",
 year         = "2013",
 title        = "Computing Relational Fixed Points using Interpolation",
 type         = "Technical Report",
 institution  = "MSR-TR-2013-6",
)
@inproceedings(McMillan10,
 author       = "Kenneth L. McMillan",
 year         = "2010",
 title        = "Lazy Annotation for Program Testing and Verification",
 booktitle    = "Proceedings of CAV",
 pages        = "104--118",
 doi          = "10.1007/978-3-642-14295-6_10",
)
@inproceedings(MouraB08,
 author       = "Leonardo Mendon\c {c}a de Moura and Nikolaj Bj{\o }rner",
 year         = "2008",
 title        = "Z3: An Efficient SMT Solver",
 booktitle    = "Proceedings of TACAS",
 pages        = "337--340",
 doi          = "10.1007/978-3-540-78800-3_24",
)
@inproceedings(NeculaMRW02,
 author       = "George C. Necula and Scott McPeak and Shree Prakash Rahul and Westley Weimer",
 year         = "2002",
 title        = "CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs",
 booktitle    = "Proceedings of CC",
 pages        = "213--228",
 doi          = "10.1007/3-540-45937-5_16",
)
@inproceedings(PeraltaG98,
 author       = "J. C. Peralta and J. P. Gallagher and H. Saglam",
 year         = "1998",
 title        = "Analysis of {I}mperative {P}rograms through {A}nalysis of {C}onstraint {L}ogic {P}rograms",
 booktitle    = "Proceedings of the 5th {I}nternational {S}ymposium on {S}tatic {A}nalysis, {SAS}~'98",
 series       = "Lecture Notes in Computer Science 1503",
 publisher    = "Springer",
 pages        = "246--261",
 doi          = "10.1007/3-540-49727-7\_15",
)
@inproceedings(PueblaAH06,
 author       = "Germ{\'a}n Puebla and Elvira Albert and Manuel V. Hermenegildo",
 year         = "2006",
 title        = "Abstract Interpretation with Specialized Definitions",
 booktitle    = "Proceedings of SAS",
 pages        = "107--126",
 doi          = "10.1007/11823230_8",
)
@inproceedings(disjunctive-intps,
 author       = "Philipp R{\"u}mmer and Hossein Hojjat and Viktor Kuncak",
 year         = "2013",
 title        = "Disjunctive Interpolants for Horn-Clause Verification",
 booktitle    = "Proceedings of CAV",
 pages        = "347--363",
 doi          = "10.1007/978-3-642-39799-8_24",
)
@inproceedings(ViG14,
 author       = "Yakir Vizel and Arie Gurfinkel",
 year         = "2014",
 title        = "Interpolating Property Directed Reachability",
 booktitle    = "Proceedings of CAV",
 doi          = "10.1007/978-3-319-08867-9_17",
)
@inproceedings(WangYGI07,
 author       = "Chao Wang and Zijiang Yang and Aarti Gupta and Franjo Ivancic",
 year         = "2007",
 title        = "Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra",
 booktitle    = "Proceedings of CAV",
 pages        = "352--365",
 doi          = "10.1007/978-3-540-73368-3_40",
)