|
⇤ ← Revision 1 as of 2011-02-07 14:23:25
Size: 36
Comment:
|
← Revision 2 as of 2011-02-07 14:25:35 ⇥
Size: 1142
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 1: | Line 1: |
| Describe SLInProofAssistants here. | == Separation logic & proof assistants == As is incredibly difficult for fully automatic techniques to prove full functional correctness, a number of projects use separation logic within a proof assistant (in the sense of the LCF/HOL/Isabelle/Coq tradition). Often these interactive proofs are assisted by advanced tactics that carry out many mundane proof steps. * [[http://flint.cs.yale.edu/flint/software.html|CAP/SCAP/XCAP]] (Yale) * [[http://www.cs.princeton.edu/~appel/cminor/|Concurrent C Minor]] (Princeton) * [[http://holfoot.heap-of-problems.org/|Holfoot]] (Cambridge) * [[http://ertos.nicta.com.au/research/l4.verified/|L4.verified]] (Sydney) * [[http://staff.aist.go.jp/reynald.affeldt/seplog/|SepLog in Coq]] (Tokyo) * [[http://ynot.cs.harvard.edu/|Ynot]] (Harvard) === Medium-scale and large-scale case studies === * [[http://ynot.cs.harvard.edu/papers/popl10.pdf|Lightweight RDBMS]] (Ynot) * [[http://software.imdea.org/~aleks/papers/reflect/reflect.pdf|Fast congrunce closure algorithm of Nieuwenhuis and Oliveras]] (HTT/Ynot) * [[http://ertos.nicta.com.au/research/l4.verified/|L4 microkernel]] |
Separation logic & proof assistants
As is incredibly difficult for fully automatic techniques to prove full functional correctness, a number of projects use separation logic within a proof assistant (in the sense of the LCF/HOL/Isabelle/Coq tradition). Often these interactive proofs are assisted by advanced tactics that carry out many mundane proof steps.
CAP/SCAP/XCAP (Yale)
Concurrent C Minor (Princeton)
Holfoot (Cambridge)
L4.verified (Sydney)
SepLog in Coq (Tokyo)
Ynot (Harvard)