Name
Abstract | ||
|---|---|---|
We present a sequent-based deductive system for automatically proving entailments in separation logic by using mathematical induction. Our technique, called mutual explicit induction proof, is an instance of Noetherian induction. Specifically, we propose a novel induction principle on a well-founded relation of separation logic model, and follow the explicit induction methods to implement this principle as inference rules, so that it can be easily integrated into a deductive system. We also support mutual induction, a natural feature of implicit induction, where the goal entailment and other entailments derived during the proof search can be used as hypotheses to prove each other. We have implemented a prototype prover and evaluated it on a benchmark of handcrafted entailments as well as benchmarks from a separation logic competition. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-48989-6_40 | Lecture Notes in Computer Science |
DocType | Volume | ISSN |
Conference | 9995 | 0302-9743 |
Citations | PageRank | References |
4 | 0.40 | 21 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Quang-Trung Ta | 1 | 8 | 3.83 |
| Ton Chanh Le | 2 | 23 | 2.69 |
| Siau-cheng Khoo | 3 | 1016 | 50.74 |
| weingan chin | 4 | 77 | 7.94 |