Relational program reasoning using compiler IR

DOI10.1007/s10817-017-9433-5zbMath1426.68052WikidataQ121592888 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

68N20: Theory of compilers and interpreters

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Uses Software

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