Please use this identifier to cite or link to this item:
|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:
|TaQT.pdf||1.09 MB||Adobe PDF|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.