Home
Separation Logic
Specs
Tools
Thanks
References
Competition report:
- M. Sighireanu and D. R. Cok.
Report on SLCOMP 2014.
[PDF]
Research articles describing the techniques underlying the tools and the benchmarks:
- J. Brotherston, N. Gorogiannis, and R.L. Petersen.
A Generic Cyclic Theorem Prover, APLAS'10.
[TR PDF]
- J. Brotherston, C. Fuhs, N. Gorogiannis, and J.N. Perez.
A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates,
CSL-LICS'14.
[TR PDF]
- Wei-Ngan Chin, Cristian Gherghina, Razvan Voicu, Quang Loc Le, Florin Craciun, Shengchao Qin : A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification. CAV 2011. [pdf]
- C. Enea, O. Lengal, M. Sighireanu, and T. Vojnar.
Compositional Entailment Checking for a Fragment of Separation Logic,
APLAS'14.
[TR PDF]
- R. Iosif, A. Rogalewicz, and T. Vojnar.
Deciding Entailments in Inductive Separation Logic with Tree Automata.
ATVA'2014.
[TR PDF]
- J.A. Navarro Perez and A. Rybalchenko.
Separation Logic Modulo Theories.
APLAS'13.
Web site for some tools:
Other references:
Last modified: Thu Dec 18 00:38:44 CET 2014