@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",
)