Relational program reasoning using compiler IR

DOI10.1007/s10817-017-9433-5zbMath1426.68052OpenAlexW2760670085WikidataQ121592888 ScholiaQ121592888MaRDI QIDQ1703014

Vladimir Klebanov, Mattias Ulbrich, Moritz Kiefer

Publication date: 1 March 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-017-9433-5

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Certified verification of relational properties ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Daikon
• LLVM
• Boogie
• AProVE
• LLBMC
• SymDiff
• SeaHorn
• c2i
• CoVaC
• SMACK

Cites Work

• Unnamed Item
• From invariant checking to invariant inference using randomized search
• An \(O(ND)\) difference algorithm and its variations
• Relational verification through Horn clause transformation
• The Daikon system for dynamic detection of likely invariants
• Generalized Property Directed Reachability
• Relational Decomposition
• Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• Towards Modularly Comparing Programs Using Automated Theorem Provers
• A Data Driven Approach for Algebraic Loop Invariants