Separation Logic + Superposition Calculus = Heap Theorem ...Heap Theorem Prover •split the...
Transcript of Separation Logic + Superposition Calculus = Heap Theorem ...Heap Theorem Prover •split the...
-
Separation Logic + Superposition Calculus =
Heap Theorem ProverJuan A. Navarro Pérez and Andrey Rybalchenko
Fakultat für InformatikTechnische Universität München
-
Separation Logic + Superposition Calculus =
Heap Theorem Prover
-
Separation Logic + Superposition Calculus =
Heap Theorem Prover
1
-
Separation Logic + Superposition Calculus =
Heap Theorem Prover
1
2
-
Separation Logic + Superposition Calculus =
Heap Theorem Prover
1
2
3
-
Separation Logicnext(x, y)
x :HeapMemory
y
-
Separation Logicnext(x, y)
x :
lseg(y, z)
zHeapMemory
y :
-
Separation Logicnext(x, y)
x :
lseg(y, z)
z
∗
HeapMemory
y :
-
Separation Logicnext(x, y)
x :
lseg(y, z)
z
∗
HeapMemory
y :
Symbolic Execution with Separation Logic (Berdine et al. 2005)
• Reasoning about heap structure and aliasing• Calculus for entailments of the form:• Search for a sequence of inferences that yields a proof
Π ∧ Σ → Π� ∧ Σ�
-
Superposition Calculus
L1 ∨ · · · ∨ Ln ∨R1 ∨ · · · ∨Rm ∨ y � z
L1 ∨ · · · ∨ Ln ∨ x� y R1 ∨ · · · ∨Rm ∨ x� z
-
Superposition Calculus
L1 ∨ · · · ∨ Ln ∨R1 ∨ · · · ∨Rm ∨ y � z
L1 ∨ · · · ∨ Ln ∨ x� y R1 ∨ · · · ∨Rm ∨ x� z
-
Superposition Calculus
L1 ∨ · · · ∨ Ln ∨R1 ∨ · · · ∨Rm ∨ y � z
L1 ∨ · · · ∨ Ln ∨ x� y R1 ∨ · · · ∨Rm ∨ x� z
• Equality reasoning with paramodulation (Robinson & Wos 1969)• Superpostion inference rules (Knuth & Bendix 1970)• Handbook of Automated Reasoning (Nieuwenhuis & Rubio 2001)
-
Superposition Calculus
L1 ∨ · · · ∨ Ln ∨R1 ∨ · · · ∨Rm ∨ y � z
L1 ∨ · · · ∨ Ln ∨ x� y R1 ∨ · · · ∨Rm ∨ x� z
• Equality reasoning with paramodulation (Robinson & Wos 1969)• Superpostion inference rules (Knuth & Bendix 1970)• Handbook of Automated Reasoning (Nieuwenhuis & Rubio 2001)
reasoning about aliasing = reasoning about equality
-
Separation Logic + Superposition Calculus =
Heap Theorem Prover
-
Separation Logic + Superposition Calculus =
Heap Theorem Prover
reasoning aboutaliasing/equality
reasoning aboutheap structure
-
Heap Theorem Proverc �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� e¬lseg(b, c) ∗ lseg(c, e)lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� e¬lseg(b, c) ∗ lseg(c, e)lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� e¬lseg(b, c) ∗ lseg(c, e)lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c¬lseg(b, c) ∗ lseg(c, e)
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c¬lseg(b, c) ∗ lseg(c, e)
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c¬lseg(b, c) ∗ lseg(c, e)
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c¬lseg(b, c) ∗ lseg(c, e)
∗ lseg(a, a)a� b ∨ lseg(a, b)∗ next(a, d) ∗ lseg(d, e)
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c¬lseg(b, c) ∗ lseg(c, e)
∗ lseg(a, a)a� b ∨ lseg(a, b)∗ next(a, d) ∗ lseg(d, e)
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c¬lseg(b, c) ∗ lseg(c, e)
a� b ∨ lseg(a, b) ∗ next(a, d) ∗ lseg(d, e)
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c¬lseg(b, c) ∗ lseg(c, e)a� ba� b ∨ lseg(a, b) ∗ next(a, d) ∗ lseg(d, e)
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c¬lseg(b, c) ∗ lseg(c, e)a� b
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� blseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
¬lseg(b, c) ∗ lseg(c, e)
lseg(a, a) ∗
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� blseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
¬lseg(b, c) ∗ lseg(c, e)
lseg(a, a) ∗
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
¬lseg(a, c) ∗ lseg(c, e)lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
¬lseg(a, c) ∗ lseg(c, e)lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
¬lseg(a, c) ∗ lseg(c, e)lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
c� e ∨ ¬lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
c� e ∨ ¬lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
c� elseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
c� e ∨ ¬lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
-
Heap Theorem Prover
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
c� e
c �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)→ lseg(b, c) ∗ lseg(c, e)
-
Heap Theorem Proverc �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
→ lseg(b, c) ∗ lseg(c, e)
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
c� e
-
Heap Theorem Proverc �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
→ lseg(b, c) ∗ lseg(c, e)
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
c� e
-
Heap Theorem Proverc �� e ∧ lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
→ lseg(b, c) ∗ lseg(c, e)
PureSpatial
c �� ea� b ∨ a� c
lseg(a, b) ∗ lseg(a, c) ∗ next(c, d) ∗ lseg(d, e)
a� b¬lseg(b, c) ∗ lseg(c, e)
c� e
Theorem
-
Heap Theorem Prover•split the entailment into:•pure clauses, a positive spatial clause, and a negative spatial clause
•repeat•repeat•search for a model of the pure clauses•return “Theorem” if no model is found•normalize the positive spatial clause w.r.t. the model•derive more pure clauses by well-formed inferences
•until the pure clauses reach a fixpoint•return “Invalid” if the model is a counterexample•normalize the negative spatial clause w.r.t. the model•apply unfolding inferences and resolve away the spatial clauses•return “Invalid” if the spatial clauses donʼt match
•forever
-
Heap Theorem Prover•split the entailment into:•pure clauses, a positive spatial clause, and a negative spatial clause
•repeat•repeat•search for a model of the pure clauses•return “Theorem” if no model is found•normalize the positive spatial clause w.r.t. the model•derive more pure clauses by well-formed inferences
•until the pure clauses reach a fixpoint•return “Invalid” if the model is a counterexample•normalize the negative spatial clause w.r.t. the model•apply unfolding inferences and resolve away the spatial clauses•return “Invalid” if the spatial clauses donʼt match
•forever
no search
-
Heap Theorem Prover•split the entailment into:•pure clauses, a positive spatial clause, and a negative spatial clause
•repeat•repeat•search for a model of the pure clauses•return “Theorem” if no model is found•normalize the positive spatial clause w.r.t. the model•derive more pure clauses by well-formed inferences
•until the pure clauses reach a fixpoint•return “Invalid” if the model is a counterexample•normalize the negative spatial clause w.r.t. the model•apply unfolding inferences and resolve away the spatial clauses•return “Invalid” if the spatial clauses donʼt match
•forever
no searchno search
-
Heap Theorem Prover•split the entailment into:•pure clauses, a positive spatial clause, and a negative spatial clause
•repeat•repeat•search for a model of the pure clauses•return “Theorem” if no model is found•normalize the positive spatial clause w.r.t. the model•derive more pure clauses by well-formed inferences
•until the pure clauses reach a fixpoint•return “Invalid” if the model is a counterexample•normalize the negative spatial clause w.r.t. the model•apply unfolding inferences and resolve away the spatial clauses•return “Invalid” if the spatial clauses donʼt match
•forever
no searchno search
no search
-
Heap Theorem Prover•split the entailment into:•pure clauses, a positive spatial clause, and a negative spatial clause
•repeat•repeat•search for a model of the pure clauses•return “Theorem” if no model is found•normalize the positive spatial clause w.r.t. the model•derive more pure clauses by well-formed inferences
•until the pure clauses reach a fixpoint•return “Invalid” if the model is a counterexample•normalize the negative spatial clause w.r.t. the model•apply unfolding inferences and resolve away the spatial clauses•return “Invalid” if the spatial clauses donʼt match
•forever
no searchno search
no searchno search
-
Heap Theorem Prover•split the entailment into:•pure clauses, a positive spatial clause, and a negative spatial clause
•repeat•repeat•search for a model of the pure clauses•return “Theorem” if no model is found•normalize the positive spatial clause w.r.t. the model•derive more pure clauses by well-formed inferences
•until the pure clauses reach a fixpoint•return “Invalid” if the model is a counterexample•normalize the negative spatial clause w.r.t. the model•apply unfolding inferences and resolve away the spatial clauses•return “Invalid” if the spatial clauses donʼt match
•forever
no searchno search
no searchno search
search
-
Separation Logic + Superposition Calculus =
Heap Theorem Prover
reasoning aboutaliasing/equality
reasoning aboutheap structure
-
Separation Logic + Superposition Calculus =
Heap Theorem Prover
reasoning aboutaliasing/equality
search
reasoning aboutheap structure
no search
-
Heap Theorem Prover
0 secs.
20 secs.
40 secs.
60 secs.
80 secs.
jStar Smallfoot SLP
Time to solve 1 000 synthetic “unfolding” entailments
> 10 min (10%)
-
Heap Theorem Prover
0 secs.
20 secs.
40 secs.
60 secs.
80 secs.
jStar Smallfoot SLP
Time to solve 1 000 synthetic “unfolding” entailments
> 10 min (10%)
• Prolog implementation
• Direct encoding of the rules from the calculus
-
What’s next?
• Extension with other data structures (e.g. trees)• Combination with other theories• Linear Arithmetic (Korovin & Voronkov 2007)• SMT (Baumgartner & Waldmann 2009; de Moura & Bjørner 2009)• Verified Software Toolchain (Appel 2011)• Ongoing implementation of a model checker
-
Separation Logic + Superposition Calculus =
Heap Theorem Prover
reasoning aboutaliasing/equality
search
reasoning aboutheap structure
no search