Automating regression verification of pointer programs by predicate abstraction

DOI10.1007/s10703-017-0293-8zbMath1392.68146OpenAlexW2751641401MaRDI QIDQ1650864

Philipp Rümmer, Vladimir Klebanov, 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

regression verificationprogram equivalenceHorn constraint solvingrelational program verification

Mathematics Subject Classification ID

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

Uses Software

• SIMPLIFY
• Boogie
• AProVE
• SymDiff

Cites Work

• Unnamed Item
• Unnamed Item
• Guiding Craig interpolation with domain-specific abstractions
• Inference rules for proving the equivalence of recursive procedures
• Generalized Property Directed Reachability
• Computer-Aided Cryptographic Proofs
• Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
• Information Flow in Object-Oriented Software
• Introduction to Software Testing
• Ownership confinement ensures representation independence for object-oriented programs
• Simplify: a theorem prover for program checking
• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• Guarded commands, nondeterminacy and formal derivation of programs
• Towards Modularly Comparing Programs Using Automated Theorem Provers
• A logic for information flow in object-oriented programs

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