Automated verification of recursive programs with pointers

DOI10.1007/978-3-642-31365-3_14zbMATH Open1358.68200OpenAlexW1480874032MaRDI QIDQ2908486FDOQ2908486

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

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

Mathematics Subject Classification ID

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

Cited In (10)

• 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?)
• 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
• Title not available (Why is that?)

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)