Relational program reasoning using compiler IR
DOI10.1007/S10817-017-9433-5zbMATH Open1426.68052OpenAlexW2760670085WikidataQ121592888 ScholiaQ121592888MaRDI QIDQ1703014FDOQ1703014
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
Recommendations
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)
Cites Work
- The Daikon system for dynamic detection of likely invariants
- From invariant checking to invariant inference using randomized search
- An \(O(ND)\) difference algorithm and its variations
- Generalized property directed reachability
- Towards modularly comparing programs using automated theorem provers
- A data driven approach for algebraic loop invariants
- Relational decomposition
- Beyond 2-safety: asymmetric product programs for relational program verification
- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
- Relational verification through Horn clause transformation
- Relational logic with framing and hypotheses
Cited In (9)
- Understanding counterexamples for relational properties with \textit{DIbugger}
- Title not available (Why is that?)
- 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
Uses Software
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)
