diff --git a/README b/README index e99e4cb5..950c8019 100644 --- a/README +++ b/README @@ -8,7 +8,7 @@ integrated. Below SL stands for the symbolic-heap fragment of separation logic with inductive definitions and existential quantifiers. -See the subfolder "papers" for electronic versions of papers mentioned and +See the subfolder "doc/papers" for electronic versions of papers mentioned and bibliographic information in BibTeX format. ================================================================================ @@ -16,39 +16,42 @@ TOOLS: Under active development (published): sl_prove.native: A cyclic theorem prover for SL entailments - (see README.APLAS12). + (see doc/README.APLAS12). sl_satcheck.native: A decision procedure for satisfiability of SL formulas - (see README.CSL-LICS14). + (see doc/README.CSL-LICS14). sl_disprove.native: A heuristic procedure for disproving SL entailments - (see README.TABLEAUX15). + (see doc/README.TABLEAUX15). +sl_modelcheck.native: A model checker for SL with arbitrary inductive predicates + (see doc/README.POPL16) + while_prove.native: A cyclic prover for a program logic over simple while-programs with pointers and dynamic allocation. Preconditions are expressed in SL and the prover can search for proofs of termination or - safety (see README.SAS14). + safety (see doc/README.SAS14). while_abduce.native: A cyclic prover like while_prove, but which attempts to infer a suitable inductively-defined precondition such that the target program will terminate/execute safely. NB this includes inferring the - inductive definitions themselves (see README.SAS14). + inductive definitions themselves (see doc/README.SAS14). No longer under active development: (see README files below for instructions on how to rebuild them) fo_prove: A cyclic prover for (for all-exists) first order logic with - inductive definitions (see README.APLAS12). + inductive definitions (see doc/README.APLAS12). goto_prove.native: A cyclic prover for a program logic like while_prove - above, but for a go-to language (see README.APLAS12). + above, but for a go-to language (see doc/README.APLAS12). ================================================================================ RUNNING/COMPILING: Running an executable without arguments will print out instructions for use. -To build from source see README.compiling. +To build from source see doc/README.compiling. ================================================================================ CONTACT: diff --git a/TODO b/TODO index e3ed5cc1..fdcedba7 100644 --- a/TODO +++ b/TODO @@ -1,9 +1,9 @@ -[TODO] Fix conditions on term unification and push most to call sites [TODO] modularise/abstract variables, formulas, definitions for SL [TODO] drop melt as a dependency and re-do the required stuff locally [TODO] consider hash consing for terms formulas etc [TODO] consider patricia trees and maps for most uses [TODO] decide on symheap representation: special data structure or general formula type +[DONE] Fix conditions on term unification and push most to call sites [DONE] rationalise unification interface across all modules [DONE] fix up tagging assumptions [DONE] fix bug wrt tags in weaken tactic in backlinks diff --git a/all.itarget b/all.itarget index 449f39fe..7f13e839 100644 --- a/all.itarget +++ b/all.itarget @@ -9,5 +9,5 @@ src/while/while_prove.native src/while/while_abduce.native src/extended_while/extended_while_prove.native src/temporal/temporal_prove.native -cyclist.docdir/index.html +src/cyclist.docdir/index.html src/seplog/sl.top diff --git a/README.APLAS12 b/doc/README.APLAS12 similarity index 97% rename from README.APLAS12 rename to doc/README.APLAS12 index 2b424c0d..73180d07 100644 --- a/README.APLAS12 +++ b/doc/README.APLAS12 @@ -23,7 +23,7 @@ The theory/design behind Cyclist and the three provers above is described in J. Brotherston, N. Gorogiannis, and R. L. Petersen. A generic cyclic theorem prover. In Proc. APLAS-10, pages 350-367. Springer, 2012. -See papers/APLAS12.{pdf,bib}. +See doc/papers/APLAS12.{pdf,bib}. The grammar for SL sequents is roughly as follows. @@ -61,7 +61,7 @@ relevant to that version. ================================================================================ COMPILING: -See README.compiling. +See doc/README.compiling. ================================================================================ CONTACT: diff --git a/README.CSL-LICS14 b/doc/README.CSL-LICS14 similarity index 96% rename from README.CSL-LICS14 rename to doc/README.CSL-LICS14 index 05e48439..b0167204 100644 --- a/README.CSL-LICS14 +++ b/doc/README.CSL-LICS14 @@ -13,7 +13,7 @@ The algorithm, its soundness and its complexity are described in A decision procedure for satisfiability in separation logic with inductive predicates. To appear at CSL-LICS, 2014. -PDF version and BibTeX are in papers/CSL-LICS14.{bib,pdf} +PDF version and BibTeX are in doc/papers/CSL-LICS14.{bib,pdf} ================================================================================ QUICKSTART: @@ -63,7 +63,7 @@ installed. Then, do ================================================================================ COMPILING: -See README.compiling. +See doc/README.compiling. ================================================================================ CONTACT: diff --git a/README.POPL16 b/doc/README.POPL16 similarity index 98% rename from README.POPL16 rename to doc/README.POPL16 index 81754966..7c7c16b7 100644 --- a/README.POPL16 +++ b/doc/README.POPL16 @@ -33,7 +33,7 @@ README file in the tests/slmc/ subdirectory. ================================================================================ THEORY: -See papers/POPL16.{pdf,bib} +See doc/papers/POPL16.{pdf,bib} ================================================================================ CONTACT: diff --git a/README.SAS14 b/doc/README.SAS14 similarity index 98% rename from README.SAS14 rename to doc/README.SAS14 index 640f5719..243a9b59 100644 --- a/README.SAS14 +++ b/doc/README.SAS14 @@ -42,7 +42,7 @@ altering the search parameters. ================================================================================ THEORY: -See papers/SAS14.{pdf,bib} +See doc/papers/SAS14.{pdf,bib} ================================================================================ CONTACT: diff --git a/README.TABLEAUX15 b/doc/README.TABLEAUX15 similarity index 97% rename from README.TABLEAUX15 rename to doc/README.TABLEAUX15 index eec01fa7..6af93b0b 100644 --- a/README.TABLEAUX15 +++ b/doc/README.TABLEAUX15 @@ -29,7 +29,7 @@ script will execute the LEM benchmark. ================================================================================ THEORY: -See papers/TABLEAUX15.{pdf,bib} +See doc/papers/TABLEAUX15.{pdf,bib} ================================================================================ CONTACT: diff --git a/README.compiling b/doc/README.compiling similarity index 100% rename from README.compiling rename to doc/README.compiling diff --git a/papers/APLAS12.bib b/doc/papers/APLAS12.bib similarity index 100% rename from papers/APLAS12.bib rename to doc/papers/APLAS12.bib diff --git a/papers/CSL-LICS14.bib b/doc/papers/CSL-LICS14.bib similarity index 100% rename from papers/CSL-LICS14.bib rename to doc/papers/CSL-LICS14.bib diff --git a/doc/papers/POPL16.bib b/doc/papers/POPL16.bib new file mode 100644 index 00000000..e6884523 --- /dev/null +++ b/doc/papers/POPL16.bib @@ -0,0 +1,8 @@ +@inproceedings{ Brotherston2016, + author = {James Brotherston and Nikos Gorogiannis and Max Kanovich and Reuben Rowe}, + title = {Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates}, + booktitle = {POPL'16, accepted for publication}, + series = {}, + year = {2016}, + pages = {}, +} \ No newline at end of file diff --git a/papers/SAS14.bib b/doc/papers/SAS14.bib similarity index 100% rename from papers/SAS14.bib rename to doc/papers/SAS14.bib diff --git a/doc/papers/TABLEAUX15.bib b/doc/papers/TABLEAUX15.bib new file mode 100644 index 00000000..b66d5941 --- /dev/null +++ b/doc/papers/TABLEAUX15.bib @@ -0,0 +1,13 @@ +@incollection{Brotherston2015, + year={2015}, + booktitle={Automated Reasoning with Analytic Tableaux and Related Methods}, + volume={9323}, + series={Lecture Notes in Computer Science}, + editor={De Nivelle, Hans}, + doi={10.1007/978-3-319-24312-2_20}, + title={Disproving Inductive Entailments in Separation Logic via Base Pair Approximation}, + publisher={Springer International Publishing}, + author={Brotherston, James and Gorogiannis, Nikos}, + pages={287-303}, + language={English} +} diff --git a/papers/APLAS12.pdf b/papers/APLAS12.pdf deleted file mode 100644 index 221cadf8..00000000 Binary files a/papers/APLAS12.pdf and /dev/null differ diff --git a/papers/CSL-LIC14.pdf b/papers/CSL-LIC14.pdf deleted file mode 100644 index 867c2925..00000000 Binary files a/papers/CSL-LIC14.pdf and /dev/null differ diff --git a/papers/POPL16.bib b/papers/POPL16.bib deleted file mode 100644 index 0f2e4d87..00000000 --- a/papers/POPL16.bib +++ /dev/null @@ -1,358 +0,0 @@ -@Misc{CyclistTool, - title = "{\textsc{Cyclist}}: software distribution", - howpublished = "\\ \url{https://github.com/ngorogiannis/cyclist/}" -} - -@Misc{ArcherGdb, - title = "{P}roject {A}rcher {GDB} development branch", - howpublished = "\\ \url{https://sourceware.org/gdb/wiki/ProjectArcher}" -} - -@InProceedings{Agten-etal:15, - author = "Pieter Agten and Bart Jacobs and Frank Piessens", - title = "Sound Modular Verification of {C} Code Executing in an Unverified Context", - booktitle = "Proc.\ {POPL}-42", - pages = "581--594", - publisher = "ACM", - year = 2015 -} - -@article{Alternation, - author = {Ashok K. Chandra and - Dexter Kozen and - Larry J. Stockmeyer}, - title = {Alternation}, - journal = {J. {ACM}}, - volume = {28}, - number = {1}, - pages = {114--133}, - year = {1981} -} - -@InProceedings{Antonopoulos-etal:14, - author = "Timos Antonopoulos and Nikos Gorogiannis and Christoph Haase and Max Kanovich and Jo{\"e}l Ouaknine", - title = "Foundations for Decision Problems in Separation Logic with General Inductive Predicates", - booktitle = "Proc.\ {FoSSaCS}-17", - year = 2014, - series = "LNCS", - volume = 8412, - pages = "411--425", - publisher = "Springer" -} - -@InProceedings{Berdine-Calcagno-OHearn:04, - author = "Josh Berdine and Cristiano Calcagno and Peter O'Hearn", - title = "A Decidable Fragment of Separation Logic", - booktitle = "Proc.\ {FSTTCS}-24", - series = "LNCS", - volume = 3328, - pages = "97--109", - publisher = "Springer", - year = 2004 -} - -@InProceedings{Berdine-Calcagno-OHearn:APLAS-05, - author = "Josh Berdine and Cristiano Calcagno and Peter W. O'Hearn", - title = "Symbolic Execution with Separation Logic", - booktitle = "Proc.\ {APLAS}-3", - series = "LNCS", - publisher = "Springer", - volume = 3780, - pages = "52--68", - year = 2005 -} - -@InProceedings{Berdine-Cook-Ishtiaq:11, - author = "Josh Berdine and Byron Cook and Samin Ishtiaq", - title = "{SLAyer:} Memory Safety for Systems-Level Code", - booktitle = "Proc.\ {CAV}-23", - year = 2011, - pages = "178--183", - publisher = "Springer" -} - -@InProceedings{Bornat-etal:05, - author = "Richard Bornat and Cristiano Calcagno and Peter O'Hearn and Matthew Parkinson", - title = "Permission accounting in separation logic", - booktitle = "Proc.\ {POPL}-32", - pages = "59--70", - publisher = "ACM", - year = 2005 -} - -@InProceedings{Botincan-etal:11, - author = "Matko Botincan and Dino Distefano and Mike Dodds and Radu Grigore and Daiva Naudziuniene and Matthew J.~Parkinson", - title = "{coreStar}: {T}he core of {jS}tar", - booktitle = "Proc.\ 1st BOOGIE", - pages = "65--77", - year = 2011 -} - -@InProceedings{Brotherston:07, - author = "James Brotherston", - title = "Formalised Inductive Reasoning in the Logic of Bunched Implications", - booktitle = "Proc.\ {SAS}-14", - series = "LNCS", - volume = 4634, - pages = "87--103", - publisher = "Springer", - year = 2007 -} - -@InProceedings{Brotherston-Gorogiannis-Petersen:12, - author = "James Brotherston and Nikos Gorogiannis and Rasmus L.~Petersen", - title = "A Generic Cyclic Theorem Prover", - booktitle = "Proc.\ {APLAS-10}", - year = 2012, - series = "LNCS", - publisher = "Springer", - pages = "350--367" -} - -@InProceedings{Brotherston-etal:14, - author = "James Brotherston and Carsten Fuhs and Nikos Gorogiannis and Juan {Navarro P\'erez}", - title = "A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates", - booktitle = "Proc.\ {CSL-LICS}", - publisher = "ACM", - year = 2014, - pages = "25:1--25:10" -} - -@InProceedings{Brotherston-Gorogiannis:14, - author = "James Brotherston and Nikos Gorogiannis", - title = "Cyclic Abduction of Inductively Defined Safety and Termination Preconditions", - booktitle = "Proc.\ {SAS-21}", - year = 2014, - pages = "68--84", - series = "LNCS", - volume = 8723, - publisher = "Springer" -} - -@InProceedings{Brotherston-Gorogiannis:15, - author = "James Brotherston and Nikos Gorogiannis", - title = "Disproving Inductive Entailments in Separation Logic via Base Pair Approximation", - booktitle = "Proc.\ {TABLEAUX-24}", - year = 2015, - note = "To appear" -} - -@Article{Calcagno-etal:11, - author = "Cristiano Calcagno and Dino Distefano and Peter O'Hearn and Hongseok Yang", - title = "Compositional Shape Analysis by means of Bi-Abduction", - journal = "J.\ {ACM}", - volume = 58, - number = 6, - month = "December", - year = 2011 -} - -@InProceedings{Calcagno-Distefano:11, - author = "Cristiano Calcagno and Dino Distefano", - title = "Infer: {A}n automatic program verifier for memory safety of {C} programs", - booktitle = "Proc. {NFM-3}", - pages = "459--465", - year = 2011, - publisher = "Springer" -} - -@Article{Chin-etal:12, - author = "Wei-Ngan Chin and Cristina David and Huu Hai Nguyen and Shengchao Qin", - title = "Automated verification of shape, size and bag properties via user-defined predicates in separation logic", - journal = "Sci.\ Comp.\ Prog.", - number = 9, - pages = "1006--1036", - volume = 77, - year = 2012 -} - -@InProceedings{Chu-etal:15, - author = "Duc-Hiep Chu and Joxan Jaffar and Minh-Thai Trinh", - title = "Automatic Induction Proofs of Data-structures in Imperative Programs", - booktitle = "Proc.\ {PLDI-36}", - pages = "457--466", - publisher = "ACM", - year = 2015 -} - -@InCollection{Clark:08, - author = "Edmund M. Clarke", - title = "The Birth of Model Checking", - booktitle = "25 Years of Model Checking", - series = "LNCS", - volume = 5000, - pages = "1--26", - publisher = "Springer", - year = 2008 -} - -@InProceedings{Dudka-etal:11, - author = "Kamil Dudka and Petr Peringer and Tom{\'a}{\v{s}} Vojnar", - title = "Predator: A practical tool for checking manipulation of dynamic data structures using separation logic", - booktitle = "Proc.\ {CAV-23}", - pages = "372--378", - series = "LNCS", - volume = 6806, - year = 2011, - publisher = "Springer" -} - -@Article{Frick-Grohe:04, - author = "Markus Frick and Martin Grohe", - title = "The complexity of first-order and monadic second-order logic revisited", - journal = "Annals of Pure and Applied Logic", - volume = 130, - pages = "3--31", - publisher = "Elsevier", - year = 2004 -} - -@Article{Holyer:81, - author = "Ian Holyer", - title = "The {NP}-Completeness of Some Edge-Partition Problems", - journal = "{SIAM J. COMPUT}", - volume = 10, - number = 4, - pages = "713--717", - year = 1981 -} - -@InProceedings{Ishtiaq-OHearn:01, - author = "Samin Ishtiaq and Peter W. O'Hearn", - title = "{BI} as an Assertion Language for Mutable Data Structures", - booktitle = "Proc.\ {POPL}-28", - pages = "14--26", - publisher = "ACM", - year = 2001 -} - -@InProceedings{Iosif-etal:13, - author = "Radu Iosif and Adam Rogalewicz and Jiri Simacek", - title = "The Tree Width of Separation Logic with Recursive Definitions", - booktitle = "Proc.\ {CADE}-24", - series = "LNAI", - volume = 7898, - year = 2013, - pages = "21--38", - publisher = "Springer" -} - -@InProceedings{Le-etal:14, - author = "Quang Loc Le and Cristian Gherghina and Shengchao Qin and Wei-Ngan Chin", - title = "Shape Analysis via Second-Order Bi-Abduction", - booktitle = "Proc.\ {CAV}-26", - series = "LNCS", - volume = 8559, - publisher = "Springer", - pages = "52--68", - year = 2014 -} - -@InProceedings{Magill-etal:10, - author = "Stephen Magill and Ming-Hsien Tsai and Peter Lee and Yih-Kuen Tsay", - title = "Automatic Numeric Abstractions for Heap-Manipulating Programs", - booktitle = "Proc.\ {POPL-37}", - pages = "211-222", - publisher = "ACM", - year = 2010 -} - -@InProceedings{Nguyen-etal:08, - author = "Huu Hai Nguyen and Viktor Kuncak and Wei-Ngan Chin", - title = "Runtime Checking for Separation Logic", - booktitle = "Proc.\ {VMCAI}-9", - series = "LNCS", - volume = 4905, - pages = "203--217", - publisher = "Springer", - year = 2008 -} - -@InProceedings{Pek-etal:14, - author = "Edgar Pek and Xiaokang Qiu and P. Madhusudan", - title = "Natural Proofs for Data Structure Manipulation in {C} Using Separation Logic", - booktitle = "Proc.\ {PLDI-35}", - pages = "440--451", - publisher = "ACM", - year = 2014 -} - -@InProceedings{Reynolds:02, - author = "John C. Reynolds", - title = "Separation Logic: A Logic for Shared Mutable Data Structures", - booktitle = "Proc.\ {LICS-17}", - pages = "55--74", - publisher = "IEEE", - year = 2002 -} - -@Misc{SLCOMP14, - title = "The first {S}eparation {L}ogic {C}ompetition ({SL-COMP14})", - year = {2014}, - howpublished = "\url{http://www.liafa.univ-paris-diderot.fr/~sighirea/slcomp14/}" -} - -@InProceedings{Yang-OHearn:02, - author = "Hongseok Yang and Peter O'Hearn", - title = "A Semantic Basis for Local Reasoning", - booktitle = "Proc.\ {FOSSACS-5}", - pages = "402--416", - publisher = "Springer", - year = 2002 -} - -@InProceedings{Yang-etal:08, - author = "H.~Yang and O.~Lee and J.~Berdine and C.~Calcagno and B.~Cook and D.~Distefano and P.~O'Hearn", - title = "Scalable shape analysis for systems code", - booktitle = "Proc.\ {CAV-20}", - pages = "385--398", - series = "LNCS", - volume = 5123, - publisher = "Springer", - year = 2008 -} - - -@book{GareyJ79, - author = {M. R. Garey and - David S. Johnson}, - title = {Computers and Intractability: {A} Guide to the Theory of NP-Completeness}, - publisher = {W. H. Freeman}, - year = {1979}, - isbn = {0-7167-1044-7}, - timestamp = {Thu, 29 Mar 2007 16:16:40 +0200}, - biburl = {http://dblp.uni-trier.de/rec/bib/books/fm/GareyJ79}, - bibsource = {dblp computer science bibliography, http://dblp.org} -} - -@inproceedings{JacobsSPVPP11, - author = {Bart Jacobs and - Jan Smans and - Pieter Philippaerts and - Fr{\'{e}}d{\'{e}}ric Vogels and - Willem Penninckx and - Frank Piessens}, - title = {VeriFast: {A} Powerful, Sound, Predictable, Fast Verifier for {C} and {J}ava}, - booktitle = {Proc.\ {NFM}-3}, - pages = {41--55}, - publisher = "Springer", - year = {2011} -} - -@InProceedings{JacobsSP08, - author = {Bart Jacobs and Jan Smans and Frank Piessens}, - title = {{V}erifying the {C}omposite {P}attern using {S}eparation {L}ogic}, - booktitle = {SAVCBS Composite Pattern Challenge Track}, - year = {2008} -} - -@inproceedings{OHearnYR04, - author = {O'Hearn, Peter W. and Yang, Hongseok and Reynolds, John C.}, - title = {Separation and Information Hiding}, - booktitle = {Proc.\ {POPL}-31}, - year = {2004}, - pages = {268--280}, - numpages = {13}, - publisher = {ACM}, -} - diff --git a/papers/POPL16.pdf b/papers/POPL16.pdf deleted file mode 100644 index 09bb643d..00000000 Binary files a/papers/POPL16.pdf and /dev/null differ diff --git a/papers/SAS14.pdf b/papers/SAS14.pdf deleted file mode 100644 index 75a50070..00000000 Binary files a/papers/SAS14.pdf and /dev/null differ diff --git a/papers/TABLEAUX15.bib b/papers/TABLEAUX15.bib deleted file mode 100644 index e0323011..00000000 --- a/papers/TABLEAUX15.bib +++ /dev/null @@ -1,8 +0,0 @@ -@inproceedings{Brotherston2015, - author={Brotherston, James and Gorogiannis, Nikos}, - title={Disproving Inductive Entailments in Separation Logic via Base Pair Approximation}, - booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, {TABLEAUX} 2015}, - series = {Lecture Notes in Computer Science}, - year = {2015}, - publisher={Accepted for publication}, -} diff --git a/papers/TABLEAUX15.pdf b/papers/TABLEAUX15.pdf deleted file mode 100644 index 0f01506e..00000000 Binary files a/papers/TABLEAUX15.pdf and /dev/null differ diff --git a/cyclist.odocl b/src/cyclist.odocl similarity index 100% rename from cyclist.odocl rename to src/cyclist.odocl