Please use this identifier to cite or link to this item:
https://scholarbank.nus.edu.sg/handle/10635/142982
DC Field | Value | |
---|---|---|
dc.title | AUTOMATED ENTAILMENT PROVING IN SEPARATION LOGIC | |
dc.contributor.author | TA QUANG TRUNG | |
dc.date.accessioned | 2018-06-07T18:00:32Z | |
dc.date.available | 2018-06-07T18:00:32Z | |
dc.date.issued | 2018-01-23 | |
dc.identifier.citation | TA QUANG TRUNG (2018-01-23). AUTOMATED ENTAILMENT PROVING IN SEPARATION LOGIC. ScholarBank@NUS Repository. | |
dc.identifier.uri | http://scholarbank.nus.edu.sg/handle/10635/142982 | |
dc.description.abstract | We consider the problem of proving entailments, which are conditions generated in the formal verification of computer programs using separation logic. We propose comprehensive solutions to automatically prove entailments using proof techniques based on mathematical induction. More specifically, our first solution is a mutual induction proof system which allows entailments derived in an on-going proof to be used as hypotheses to prove future entailments which will be derived in the same proof. The second solution is a lemma synthesis framework which can automatically synthesize lemmas to assist in proving sophisticated entailments. The final solution is a failure learning framework which can systematically learn from the failure of the induction hypothesis applications to repair unsuccessful proof attempts. We have implemented these techniques in a prover named Songbird and have experimented with it on various entailment benchmarks. To date, Songbird can prove most of the entailments and outperforms all state-of-the-art separation logic provers. Our proposed solutions have opened up more opportunities to utilize separation logic to verify real-world programs. | |
dc.language.iso | en | |
dc.subject | Software Verification, Separation Logic, Entailment Proving, Mutual Induction, Lemma Synthesis, Learning from Failure | |
dc.type | Thesis | |
dc.contributor.department | COMPUTER SCIENCE | |
dc.contributor.supervisor | Khoo Siau Cheng | |
dc.contributor.supervisor | Chin Wei Ngan | |
dc.description.degree | Ph.D | |
dc.description.degreeconferred | DOCTOR OF PHILOSOPHY (SOC) | |
Appears in Collections: | Ph.D Theses (Open) |
Show simple item record
Files in This Item:
File | Description | Size | Format | Access Settings | Version | |
---|---|---|---|---|---|---|
TaQT.pdf | 1.09 MB | Adobe PDF | OPEN | None | View/Download |
Google ScholarTM
Check
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.