Please use this identifier to cite or link to this item: https://scholarbank.nus.edu.sg/handle/10635/142982
Title: AUTOMATED ENTAILMENT PROVING IN SEPARATION LOGIC
Authors: TA QUANG TRUNG
Keywords: Software Verification, Separation Logic, Entailment Proving, Mutual Induction, Lemma Synthesis, Learning from Failure
Issue Date: 23-Jan-2018
Citation: TA QUANG TRUNG (2018-01-23). AUTOMATED ENTAILMENT PROVING IN SEPARATION LOGIC. ScholarBank@NUS Repository.
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.
URI: http://scholarbank.nus.edu.sg/handle/10635/142982
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
TaQT.pdf1.09 MBAdobe PDF

OPEN

NoneView/Download

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.