Automated verification of recursive programs with pointers
From MaRDI portal
Publication:2908486
DOI10.1007/978-3-642-31365-3_14zbMATH Open1358.68200OpenAlexW1480874032MaRDI QIDQ2908486FDOQ2908486
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
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 (14)
- Abstraction of object graphs in program verification
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Automated Verification of Shape and Size Properties Via Separation Logic
- Verifying pointer and string analyses with region type systems
- Title not available (Why is that?)
- Verifying pointer safety for programs with unknown calls
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
- Programming Languages and Systems
- Programming Languages and Systems
- Dafny: an automatic program verifier for functional correctness
- Title not available (Why is that?)
- Sound and complete verification condition generator for functional recursive programs
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)
