Verifying relative safety, accuracy, and termination for program approximations

DOI10.1007/s10817-017-9421-9zbMath1425.68256OpenAlexW2738309652MaRDI QIDQ682353

Shaobo He, Shuvendu K. Lahiri, Zvonimir Rakamarić

Publication date: 2 February 2018

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

Full work available at URL: https://doi.org/10.1007/s10817-017-9421-9

zbMATH Keywords

approximate computingdifferential verificationSymDiff

Mathematics Subject Classification ID

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

Uses Software

• Coq
• PVS
• Boogie
• SymDiff
• Houdini
• FlexJava
• Chisel
• ACCEPT
• EnerJ
• Green
• Rely

Cites Work

• Unnamed Item
• Proving mutual termination
• Randomized accuracy-aware program transformations for efficient approximate computations
• Structural Analysis of Narratives with the Coq Proof Assistant
• Simple relational correctness proofs for static analyses and program transformations
• Towards Modularly Comparing Programs Using Automated Theorem Provers

This page was built for publication: Verifying relative safety, accuracy, and termination for program approximations