Post on 22-Oct-2020
transcript
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