Enhancing Program Verification with Lemmas

DOI10.1007/978-3-540-70545-1_34MaRDI QIDQ3512504zbMATH OpenOpenAlexFDO

Authors Huu Hai Nguyen, Wei-Ngan Chin

Publication date 15 July 2008

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70545-1_34

zbMATH Keywords

EntailmentLemma ApplicationLemma ProvingProgram VerificationSeparation Logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On automated lemma generation for separation logic with inductive definitions
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Computer Science Logic
• Separation logic modulo theories
• Automated Verification of Shape and Size Properties Via Separation Logic

Cited in

(9)

• Automated repair of heap-manipulating programs using deductive synthesis
• Automated mutual induction proof in separation logic
• Completeness and expressiveness of pointer program verification by separation logic
• Completeness for recursive procedures in separation logic
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• On automated lemma generation for separation logic with inductive definitions
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Automated cyclic entailment proofs in separation logic
• Separation Logic Tutorial

Describes a project that uses

Uses Software

• PVS
• Isabelle/HOL
• CVC

This page was built for publication: Enhancing Program Verification with Lemmas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3512504)