Main directory cleanup. READMEs updated.

README

@@ -8,47 +8,50 @@ 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.
 
 ================================================================================
 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:

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

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

README.APLAS12 → 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:

README.CSL-LICS14 → 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:

README.POPL16 → 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:

README.SAS14 → doc/README.SAS14

@@ -42,7 +42,7 @@ altering the search parameters.
 
 ================================================================================
 THEORY:
-See papers/SAS14.{pdf,bib}
+See doc/papers/SAS14.{pdf,bib}
 
 ================================================================================
 CONTACT:

README.TABLEAUX15 → 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:

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 = {},
+}

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}
+}