Relational program reasoning using compiler IR

DOI10.1007/S10817-017-9433-5MaRDI QIDQ1703014zbMATH OpenOpenAlexWikidataFDO

Authors Moritz Kiefer, Vladimir Klebanov, Mattias Ulbrich

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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Relational logic with framing and hypotheses
• Product programs and relational program logics
• Beyond 2-safety: asymmetric product programs for relational program verification
• Relational verification through Horn clause transformation
• Relational verification via invariant-guided synchronization

Cites work

• A data driven approach for algebraic loop invariants
• An \(O(ND)\) difference algorithm and its variations
• Beyond 2-safety: asymmetric product programs for relational program verification
• Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
• From invariant checking to invariant inference using randomized search
• Generalized property directed reachability
• Relational decomposition
• Relational logic with framing and hypotheses
• Relational verification through Horn clause transformation
• The Daikon system for dynamic detection of likely invariants
• Towards modularly comparing programs using automated theorem provers

Cited in

(9)

• Understanding counterexamples for relational properties with \textit{DIbugger}
• scientific article; zbMATH DE number 7589540 (Why is no real title available?)
• Product programs and relational program logics
• Relational verification via invariant-guided synchronization
• Verifying equivalence of Spark programs
• Certified verification of relational properties
• Using Relational Verification for Program Slicing
• Leveraging compiler intermediate representation for multi- and cross-language verification
• Abstract execution

Describes a project that uses

Uses Software

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

This page was built for publication: Relational program reasoning using compiler IR

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