Automated verification of recursive programs with pointers

DOI10.1007/978-3-642-31365-3_14MaRDI QIDQ2908486zbMATH OpenOpenAlexFDO

Authors Marcello M. Bonsangue, Jurriaan Rot, Frank S. de Boer

Publication date 5 September 2012

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-31365-3_14

Mathematics Subject Classification ID

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

Recommendations

• Programming Languages and Systems
• Automated Verification of Shape and Size Properties Via Separation Logic
• Automated program verification
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Automatically verifying temporal properties of pointer programs with cyclic proof

Cited in

(21)

• Automating regression verification of pointer programs by predicate abstraction
• Verifying pointer and string analyses with region type systems
• Automatically proving termination and memory safety for programs with pointer arithmetic
• scientific article; zbMATH DE number 1629942 (Why is no real title available?)
• Automated program verification
• Sound and complete verification condition generator for functional recursive programs
• Dafny: an automatic program verifier for functional correctness
• Abstraction of object graphs in program verification
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• scientific article; zbMATH DE number 1848282 (Why is no real title available?)
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Programming Languages and Systems
• Generating specifications for recursive methods by abstracting program states
• Automated verification of relational while-programs
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• Automated Verification of Shape and Size Properties Via Separation Logic
• Proof automation for functional correctness in separation logic
• Programming Languages and Systems
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Verifying pointer safety for programs with unknown calls

This page was built for publication: Automated verification of recursive programs with pointers

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