@inproceedings(Al&12,
 author       = "F.~Alberti and R.~Bruttomesso and S.~Ghilardi and S.~Ranise and N.~Sharygina",
 year         = "2012",
 title        = "{SAFARI}: {SMT}-based Abstraction For Arrays with Interpolants",
 booktitle    = "Proceedings of the 24th International Conference on Computer Aided Verification, CAV~'12",
 series       = "Lecture Notes in Computer Science 7358",
 publisher    = "Springer",
 pages        = "679--685",
 doi          = "10.1007/978-3-642-31424-7\_49",
)
@inproceedings(Be&07,
 author       = "D.~Beyer and T.~A. Henzinger and R.~Majumdar and A.~Rybalchenko",
 year         = "2007",
 title        = "Invariant Synthesis for Combined Theories",
 booktitle    = "Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation, ~VMCAI~'07",
 series       = "Lecture Notes in Computer Science 4349",
 publisher    = "Springer",
 pages        = "378--394",
 doi          = "10.1007/978-3-540-69738-1\_27",
)
@inproceedings(Bl&02,
 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         = "2002",
 title        = "Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software",
 booktitle    = "The Essence of Computation",
 series       = "Lecture Notes in Computer Science",
 volume       = "2566",
 publisher    = "Springer",
 pages        = "85--108",
 doi          = "10.1007/3-540-36377-7\_5",
)
@inproceedings(Br&06,
 author       = "Aaron~R. Bradley and Zohar Manna and Henny~B. Sipma",
 year         = "2006",
 title        = "What's decidable about arrays?",
 booktitle    = "Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI~'06",
 series       = "Lecture Notes in Computer Science",
 volume       = "3855",
 publisher    = "Springer",
 pages        = "427--442",
 doi          = "10.1007/11609773\_28",
)
@inproceedings(BrS09,
 author       = "M.~Bravenboer and Y.~Smaragdakis",
 year         = "2009",
 title        = "Strictly declarative specification of sophisticated points-to analyses",
 editor       = "S.~Arora and G.~T. Leavens",
 booktitle    = "Proceedings of the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA~'09",
 publisher    = "ACM",
 pages        = "243--262",
 doi          = "10.1145/1640089.1640108",
)
@article(BuD77,
 author       = "R.~M. Burstall and J.~Darlington",
 year         = "1977",
 title        = "A Trans\-form\-ation System for Developing Recursive Pro\-grams",
 journal      = "Journal of the {ACM}",
 volume       = "24",
 number       = "1",
 pages        = "44--67",
 doi          = "10.1145/321992.321996",
)
@inproceedings(CoC77,
 author       = "P.~Cousot and R.~Cousot",
 year         = "1977",
 title        = "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Pro\-grams by Construction of Approximation of Fixpoints",
 booktitle    = "Proceedings of the 4th {ACM-SIGPLAN} Symposium on Principles of Pro\-gramming Languages,~POPL~'77",
 publisher    = "{ACM}",
 pages        = "238--252",
 doi          = "10.1145/512950.512973",
)
@inproceedings(Co&11,
 author       = "P.~Cousot and R.~Cousot and F.~Logozzo",
 year         = "2011",
 title        = "A parametric segmentation functor for fully automatic and scalable array content analysis",
 booktitle    = "Proceedings of the 38th ACM Symposium on Principles of programming languages, POPL~'11",
 publisher    = "ACM",
 pages        = "105--118",
 doi          = "10.1145/1926385.1926399",
)
@inproceedings(CoH78,
 author       = "P.~Cousot and N.~Halbwachs",
 year         = "1978",
 title        = "Automatic Discovery of Linear Restraints among Variables of a Program",
 booktitle    = "Proceedings of the Fifth ACM Symposium on Principles of Programming Languages,~POPL~'78",
 publisher    = "{ACM}",
 pages        = "84--96",
 doi          = "10.1145/512760.512770",
)
@inproceedings(CuW00,
 author       = "B.~Cui and D.~S. Warren",
 year         = "2000",
 title        = "A System for Tabled Constraint Logic Programming",
 editor       = "J.~W. Lloyd",
 booktitle    = "Proceedings of the First International Conference on Computational Logic,~CL~2000, London, UK, July 24-28, 2000",
 series       = "Lecture Notes in Artificial Intelligence 1861",
 publisher    = "Springer-Verlag",
 pages        = "478--492",
 doi          = "10.1007/3-540-44957-4\_32",
)
@inproceedings(De&13b,
 author       = "E.~{De~Angelis} and F.~Fioravanti and A.~Pettorossi and M.~Proietti",
 year         = "2013",
 title        = "Specialization with Constrained Generalization for Software Model Checking",
 booktitle    = "Proceedings of the 22nd International Symposium Logic-Based Program Synthesis and Transformation, LOPSTR~'12",
 series       = "Lecture Notes in Computer Science",
 volume       = "7844",
 pages        = "51--70",
 doi          = "10.1007/978-3-642-38197-3\_5",
)
@inproceedings(De&13a,
 author       = "E.~{De~Angelis} and F.~Fioravanti and A.~Pettorossi and M.~Proietti",
 year         = "2013",
 title        = "{V}erifying {P}rograms via {I}terated {S}pecialization",
 booktitle    = "Proceedings of the {ACM} {SIGPLAN} 2013 {W}orkshop on {P}artial {E}valuation and {P}rogram {M}anipulation, PEPM~'13",
 publisher    = "ACM",
 pages        = "43--52",
 doi          = "10.1145/2426890.2426899",
)
@article(De&99,
 author       = "D.~{De Schreye} and R.~Gl{\"u}ck and J.~J{\o }rgensen and M.~Leuschel and B.~Martens and M.~H. S{\o }rensen",
 year         = "1999",
 title        = "Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments",
 journal      = "Journal of Logic Programming",
 volume       = "41",
 number       = "2--3",
 pages        = "231--277",
 doi          = "10.1016/S0743-1066(99)00030-8",
)
@inproceedings(DeP99,
 author       = "G.~Delzanno and A.~Podelski",
 year         = "1999",
 title        = "Model Checking in {CLP}",
 editor       = "R.~Cleaveland",
 booktitle    = "5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,~TACAS~'99",
 series       = "Lecture Notes in Computer Science 1579",
 publisher    = "Springer-Verlag",
 pages        = "223--239",
 doi          = "10.1007/3-540-49059-0\_16",
)
@article(EtG96,
 author       = "S.~Etalle and M.~Gabbrielli",
 year         = "1996",
 title        = "Trans\-form\-ations of {CLP} Modules",
 journal      = "Theoretical Computer Science",
 volume       = "166",
 pages        = "101--146",
 doi          = "10.1016/0304-3975(95)00148-4",
)
@inproceedings(Fi&01a,
 author       = "F.~Fioravanti and A.~Pettorossi and M.~Proietti",
 year         = "2001",
 title        = "Verifying {CTL} Properties of Infinite State Systems by Specializing Constraint Logic Programs",
 booktitle    = "Proceedings of the {ACM SIGPLAN} Workshop on Verification and Computational Logic VCL~'01, Florence, Italy",
 series       = "Technical Report DSSE-TR-2001-3",
 publisher    = "University of Southampton, UK",
 pages        = "85--96",
)
@inproceedings(Fi&04a,
 author       = "F.~Fioravanti and A.~Pettorossi and M.~Proietti",
 year         = "2004",
 title        = "Transformation Rules for Locally Stratified Constraint Logic Programs",
 editor       = "K.-K. Lau and M.~Bruynooghe",
 booktitle    = "Program Development in Computational Logic",
 series       = "Lecture Notes in Computer Science 3049",
 publisher    = "Springer-Verlag",
 pages        = "292--340",
 doi          = "10.1007/978-3-540-25951-0\_10",
)
@inproceedings(Fi&11b,
 author       = "F.~Fioravanti and A.~Pettorossi and M.~Proietti and V.~Senni",
 year         = "2011",
 title        = "Improving Reachability Analysis of Infinite State Systems by Specialization",
 editor       = "G.~Delzanno and I.~Potapov",
 booktitle    = "Proceedings of the 5th International Workshop on Reachability Problems, RP~'11, September 28-30, 2011, Genova, Italy",
 series       = "Lecture Notes in Computer Science 6945",
 publisher    = "Springer",
 pages        = "165--179",
 doi          = "10.1007/978-3-642-24288-5\_15",
)
@article(Fi&13a,
 author       = "F.~Fioravanti and A.~Pettorossi and M.~Proietti and V.~Senni",
 year         = "2013",
 title        = "Generalization Strategies for the Verification of Infinite State Systems",
 journal      = "Theory and Practice of Logic Programming. Special Issue on the 25th {A}nnual GULP {C}onference",
 volume       = "13",
 number       = "2",
 pages        = "175--199",
 doi          = "10.1017/S1471068411000627",
)
@article(Fla04,
 author       = "C.~Flanagan",
 year         = "2004",
 title        = "Automatic software model checking via constraint logic",
 journal      = "Sci. Comput. Program.",
 volume       = "50",
 number       = "1--3",
 pages        = "253--270",
 doi          = "10.1016/j.scico.2004.01.006",
)
@inproceedings(FlQ02,
 author       = "C.~Flanagan and S.~Qadeer",
 year         = "2002",
 title        = "Predicate abstraction for software verification",
 booktitle    = "Proceedings of the 29th ACM Symposium on Principles of programming languages, POPL '02",
 publisher    = "ACM",
 pages        = "191--202",
 doi          = "10.1145/503272.503291",
)
@inproceedings(Go&05,
 author       = "D.~Gopan and T.~W. Reps and S.~Sagiv",
 year         = "2005",
 title        = "A framework for numeric analysis of array operations",
 booktitle    = "Proceedings of the 32nd ACM SIGPLAN-SIGACT {S}ymposium on {P}rinciples of programming languages, POPL~'05",
 publisher    = "ACM",
 pages        = "338--350",
 doi          = "10.1145/1047659.1040333",
)
@inproceedings(HSF,
 author       = "S.~Grebenshchikov and A.~Gupta and N.~P. Lopes and C.~Popeea and A.~Rybalchenko",
 year         = "2012",
 title        = "{HSF(C): A Software Verifier based on Horn Clauses}",
 editor       = "C.~Flanagan and B.~K{\"o}nig",
 booktitle    = "Proc. of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS~'12",
 series       = "Lecture Notes in Computer Science 7214",
 publisher    = "Springer",
 pages        = "549--551",
 doi          = "10.1007/978-3-642-28756-5\_46",
)
@inproceedings(Gr&12,
 author       = "S.~Grebenshchikov and N.~P. Lopes and C.~Popeea and A.~Rybalchenko",
 year         = "2012",
 title        = "Synthesizing software verifiers from proof rules",
 booktitle    = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI~'12",
 publisher    = "ACM",
 pages        = "405--416",
 doi          = "10.1145/2345156.2254112",
)
@inproceedings(Gu&08,
 author       = "B.~S. Gulavani and S.~Chakraborty and A.~V. Nori and S.~K. Rajamani",
 year         = "2008",
 title        = "{A}utomatically {R}efining {A}bstract {I}nterpretations",
 booktitle    = "Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS~'08",
 series       = "Lecture Notes in Computer Science 4963",
 publisher    = "Springer",
 pages        = "443--458",
 doi          = "10.1007/978-3-540-78800-3\_33",
)
@inproceedings(HaP08,
 author       = "N.~Halbwachs and M.~P{\'e}ron",
 year         = "2008",
 title        = "Discovering properties about arrays in simple programs",
 booktitle    = "Proceedings of the ACM Conference on Programming language design and implementation, PLDI '08",
 publisher    = "ACM",
 pages        = "339--348",
 doi          = "10.1145/1375581.1375623",
)
@inproceedings(HeG06,
 author       = "K.~S. Henriksen and J.~P. Gallagher",
 year         = "2006",
 title        = "Abstract Interpretation of PIC Programs through Logic Programming",
 booktitle    = "Proceedings of the 6th IEEE International Workshop on Source Code Analysis and Manipulation, SCAM~'06",
 publisher    = "IEEE",
 pages        = "103 -- 179",
 doi          = "10.1016/0743-1066(92)90030-7",
)
@article(JaM94,
 author       = "J.~Jaffar and M.~Maher",
 year         = "1994",
 title        = "Constraint Logic Programming: A Survey",
 journal      = "Journal of Logic Programming",
 volume       = "19/20",
 pages        = "503--581",
 doi          = "10.1016/0743-1066(94)90033-7",
)
@unpublished(Ja&11c,
 author       = "J.~Jaffar and J.~A. Navas and A.~E. Santosa",
 year         = "2012",
 title        = "{TRACER}: {A} {S}ymbolic {E}xecution {T}ool for {V}erification",
 doi          = "10.1007/978-3-642-31424-7\_61",
)
@inproceedings(Ja&11b,
 author       = "J.~Jaffar and J.~A. Navas and A.~E. Santosa",
 year         = "2012",
 title        = "Unbounded {S}ymbolic {E}xecution for {Program} {V}erification",
 booktitle    = "{P}roceedings of the 2nd {I}nternational {C}onference on {R}untime {V}erification, {RV}~'11",
 series       = "Lecture Notes in Computer Science 7186",
 publisher    = "Springer",
 pages        = "396--411",
 doi          = "10.1007/978-3-642-29860-8\_32",
)
@article(JhM09,
 author       = "R.~Jhala and R.~Majumdar",
 year         = "2009",
 title        = "Software model checking",
 journal      = "ACM Computing Surveys",
 volume       = "41",
 number       = "4",
 pages        = "21:1--21:54",
 doi          = "10.1145/1592434.1592438",
)
@inproceedings(JhM07,
 author       = "R.~Jhala and K.~L. McMillan",
 year         = "2007",
 title        = "Array abstractions from proofs",
 booktitle    = "Proceedings of the 19th International Conference on Computer Aided Verification, CAV~'07",
 series       = "Lecture Notes in Computer Science",
 volume       = "4590",
 publisher    = "Springer",
 pages        = "193--206",
 doi          = "10.1007/978-3-540-73368-3\_23",
)
@book(Jo&93,
 author       = "N.~D. Jones and C.~K. Gomard and P.~Sestoft",
 year         = "1993",
 title        = "Partial Evaluation and Automatic Pro\-gram Generation",
 publisher    = "Prentice Hall",
)
@inproceedings(KoV09,
 author       = "L.~Kov\'{a}cs and A.~Voronkov",
 year         = "2009",
 title        = "Finding Loop Invariants for Programs over Arrays Using a Theorem Prover",
 booktitle    = "Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering, FASE~'09",
 series       = "Lecture Notes in Computer Science 5503",
 publisher    = "Springer",
 pages        = "470--485",
 doi          = "10.1007/978-3-642-00593-0\_33",
)
@article(LaB07,
 author       = "S.~K. Lahiri and R.~E. Bryant",
 year         = "2007",
 title        = "Predicate abstraction with indexed predicates",
 journal      = "ACM Trans. Comput. Log.",
 volume       = "9",
 number       = "1",
 publisher    = "ACM",
 doi          = "10.1145/1297658.1297662",
)
@inproceedings(La&13,
 author       = "D.~Larraz and E.~Rodr\'{\i }guez-Carbonell and A.~Rubio",
 year         = "2013",
 title        = "{SMT}-Based Array Invariant Generation",
 booktitle    = "14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI~'13, Rome, Italy, January 20-22, 2013",
 series       = "Lecture Notes in Computer Science 7737",
 publisher    = "Springer",
 pages        = "169--188",
 doi          = "10.1007/978-3-642-35873-9\_12",
)
@article(LeB02,
 author       = "M.~Leuschel and M.~Bruynooghe",
 year         = "2002",
 title        = "Logic program specialisation through partial deduction: Control issues",
 journal      = "Theory and Practice of Logic Programming",
 volume       = "2",
 number       = "4\&5",
 pages        = "461--515",
 doi          = "10.1017/S147106840200145X",
)
@unpublished(MAP,
 author       = "{MAP}",
 title        = "The {MAP} transformation system",
)
@inproceedings(McM08,
 author       = "K.~L. McMillan",
 year         = "2008",
 title        = "Quantified invariant generation using an interpolating saturation prover",
 booktitle    = "Proceedings of 14th international conference on Tools and algorithms for the construction and analysis of systems, TACAS~'08",
 series       = "Lecture Notes in Computer Science",
 volume       = "4963",
 publisher    = "Springer",
 pages        = "413--427",
 doi          = "10.1007/978-3-540-78800-3\_31",
)
@article(Mi&10,
 author       = "S.~P. Miller and M.~W. Whalen and D.~D. Cofer",
 year         = "2010",
 title        = "Software model checking takes off",
 journal      = "Commun. ACM",
 volume       = "53",
 number       = "2",
 publisher    = "ACM",
 pages        = "58--64",
 doi          = "10.1145/1646353.1646372",
)
@inproceedings(NiL00,
 author       = "U.~Nilsson and J.~L{\"u}bcke",
 year         = "2000",
 title        = "Constraint Logic Programming for Local and Symbolic Model-Checking",
 editor       = "J.~W. Lloyd",
 booktitle    = "Proceedings of the First International Conference on Computational Logic,~CL~2000, London, UK, July 24-28, 2000",
 series       = "Lecture Notes in Artificial Intelligence 1861",
 publisher    = "Springer-Verlag",
 pages        = "384--398",
 doi          = "10.1007/3-540-44957-4\_26",
)
@inproceedings(PeG02,
 author       = "J.~C. Peralta and J.~P. Gallagher",
 year         = "2003",
 title        = "Convex Hull Abstractions in Specialization of {CLP} Programs",
 editor       = "M.~Leuschel",
 booktitle    = "Logic Based Program Synthesis and Tranformation, 12th International Workshop, LOPSTR~'02, Madrid, Spain, September 17--20, 2002, Revised Selected Papers",
 series       = "Lecture Notes in Computer Science 2664",
 publisher    = "Springer",
 pages        = "90--108",
 doi          = "10.1007/3-540-45013-0\_8",
)
@inproceedings(Pe&98,
 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",
 editor       = "G.~{L}evi",
 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",
)
@incollection(PoR07,
 author       = "A.~Podelski and A.~Rybalchenko",
 year         = "2007",
 title        = "{ARMC}: {T}he {L}ogical {C}hoice for {S}oftware {M}odel {C}hecking with {A}bstraction {R}efinement",
 editor       = "M.~Hanus",
 booktitle    = "Practical Aspects of Declarative Languages, {PADL}~'07",
 series       = "Lecture Notes in Computer Science 4354",
 publisher    = "Springer",
 pages        = "245--259",
 doi          = "10.1007/978-3-540-69611-7\_16",
)
@article(Rep98,
 author       = "T.~W. Reps",
 year         = "1998",
 title        = "Program analysis via graph reachability",
 journal      = "Information and Software Technology",
 volume       = "40",
 number       = "11--12",
 pages        = "701--726",
 doi          = "10.1016/S0950-5849(98)00093-7",
)
@inproceedings(Ryb10,
 author       = "A.~Rybalchenko",
 year         = "2010",
 title        = "Constraint Solving for Program Verification: Theory and Practice by Example",
 editor       = "T.~Touili and B.~Cook and P.~Jackson",
 booktitle    = "Proceedings of the 22nd International Conference on Computer Aided Verification,~CAV~'10",
 series       = "Lecture Notes in Computer Science 6174",
 publisher    = "Springer",
 pages        = "57--71",
 doi          = "10.1007/978-3-642-14295-6\_7",
)
@article(Ry&10,
 author       = "A.~Rybalchenko and V.~Sofronie-Stokkermans",
 year         = "2010",
 title        = "Constraint solving for interpolation",
 journal      = "Journal of Symbolic Computation",
 volume       = "45",
 number       = "11",
 pages        = "1212--1233",
 doi          = "10.1007/978-3-540-69738-1\_25",
)
@inproceedings(Sch98,
 author       = "D.~A. Schmidt",
 year         = "1998",
 title        = "Data flow analysis is model checking of abstract interpretations",
 booktitle    = "Proceedings of the 25th ACM SIGPLAN-SIGACT {S}ymposium on {P}rinciples of {P}rogramming {L}anguages, POPL~'98",
 publisher    = "ACM",
 pages        = "38--48",
 doi          = "10.1145/268946.268950",
)
@inproceedings(Se&09,
 author       = "M.~N. Seghir and A.~Podelski and T.~Wies",
 year         = "2009",
 title        = "Abstraction Refinement for Quantified Array Assertions",
 booktitle    = "Proceeding of the 16th International Symposium on Static Analysis, SAS~'09",
 series       = "Lecture Notes in Computer Science 5673",
 publisher    = "Springer",
 pages        = "3--18",
 doi          = "10.1007/978-3-642-03237-0\_3",
)
@inproceedings(TaS84,
 author       = "H.~Tamaki and T.~Sato",
 year         = "1984",
 title        = "Unfold/Fold Trans\-form\-ation of Logic Pro\-grams",
 editor       = "S.-{\r A}. T{{\"a}}rnlund",
 booktitle    = "Proceedings of the Second International Conference on Logic Pro\-gramming,~ICLP~'84",
 publisher    = "Uppsala University",
 address      = "Uppsala, Sweden",
 pages        = "127--138",
)
@techreport(TaS86,
 author       = "H.~Tamaki and T.~Sato",
 year         = "1986",
 title        = "A Generalized Correctness Proof of the Unfold/Fold Logic Pro\-gram Trans\-form\-ation",
 type         = "Technical Report",
 number       = "86-4",
 institution  = "Ibaraki University",
 address      = "Japan",
)
@inproceedings(WhL04,
 author       = "J.~Whaley and M.~S. Lam",
 year         = "2004",
 title        = "Cloning-based context-sensitive pointer alias analysis using binary decision diagrams",
 booktitle    = "Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, PLDI~'04",
 publisher    = "ACM",
 pages        = "131--144",
 doi          = "10.1145/996841.996859",
)