Towards Modularly Comparing Programs Using Automated Theorem Provers
From MaRDI portal
Publication:4928447
DOI10.1007/978-3-642-38574-2_20zbMath1381.68054OpenAlexW26752331MaRDI QIDQ4928447
Henrique Rebêlo, Ming Kawaguchi, Shuvendu K. Lahiri, C. Hawblitzel
Publication date: 14 June 2013
Published in: Automated Deduction – CADE-24 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-38574-2_20
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (11)
Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Product programs in the wild: retrofitting program verifiers to check information flow security ⋮ Constraint-based relational verification ⋮ Automating regression verification of pointer programs by predicate abstraction ⋮ Certified verification of relational properties ⋮ Relational program reasoning using compiler IR ⋮ Unnamed Item ⋮ Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ A language-independent proof system for full program equivalence ⋮ Verifying relative safety, accuracy, and termination for program approximations ⋮ Proving mutual termination
Uses Software
This page was built for publication: Towards Modularly Comparing Programs Using Automated Theorem Provers
