Automating regression verification of pointer programs by predicate abstraction

DOI10.1007/S10703-017-0293-8MaRDI QIDQ1650864zbMATH OpenOpenAlexFDO

Authors Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich

Publication date 16 July 2018

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-356860

zbMATH Keywords

program equivalenceHorn constraint solvingregression verificationrelational program verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Regression verification for multi-threaded programs
• Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)
• Automated verification of recursive programs with pointers
• scientific article; zbMATH DE number 1953018
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic

Cites work

• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 1191738 (Why is no real title available?)
• A logic for information flow in object-oriented programs
• Computer-aided cryptographic proofs
• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• Generalized property directed reachability
• Guarded commands, nondeterminacy and formal derivation of programs
• Guiding Craig interpolation with domain-specific abstractions
• Inference rules for proving the equivalence of recursive procedures
• Information flow in object-oriented software
• Introduction to Software Testing
• Modular verification of procedure equivalence in the presence of memory allocation
• Ownership confinement ensures representation independence for object-oriented programs
• Simplify: a theorem prover for program checking
• Towards modularly comparing programs using automated theorem provers

Cited in

(7)

• Regression verification for multi-threaded programs
• Regression verification for unbalanced recursive functions
• Verifying pointer and string analyses with region type systems
• Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)
• Using Relational Verification for Program Slicing
• Programming Languages and Systems
• Lockstep composition for unbalanced loops

Describes a project that uses

Uses Software

• SymDiff
• AProVE
• Boogie
• SIMPLIFY

This page was built for publication: Automating regression verification of pointer programs by predicate abstraction

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