Enhancing Program Verification with Lemmas

DOI10.1007/978-3-540-70545-1_34zbMath1155.68443OpenAlexW2166989203MaRDI QIDQ3512504

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

Program VerificationEntailmentLemma ApplicationLemma ProvingSeparation Logic

Mathematics Subject Classification ID

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

Related Items (7)

Completeness for recursive procedures in separation logic ⋮ Automated mutual induction proof in separation logic ⋮ Completeness and expressiveness of pointer program verification by separation logic ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ Automated repair of heap-manipulating programs using deductive synthesis ⋮ Automated Cyclic Entailment Proofs in Separation Logic ⋮ Separation Logic Tutorial

Uses Software

• Isabelle/HOL
• PVS
• CVC

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