Verification of Equivalent-Results Methods

DOI10.1007/978-3-540-78739-6_24MaRDI QIDQ5458406zbMATH OpenOpenAlexFDO

Authors K. Rustan M. Leino, Peter Müller

Publication date 11 April 2008

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78739-6_24

Mathematics Subject Classification ID

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

Recommendations

• On comparison of solutions at verification
• Equivalence checking using structural methods
• Verification and validation
• Numerical validation methods
• Accuracy verification methods. Theory and algorithms
• Empirical justification of the uncertain equivalence method
• Verification methods: rigorous results using floating-point arithmetic
• scientific article; zbMATH DE number 556057
• scientific article; zbMATH DE number 45257

Cites work

• A Reachability Predicate for Analyzing Low-Level Software
• A verifying compiler for a multi-threaded object-oriented language
• How the design of JML accommodates both runtime assertion checking and formal verification
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• Separation and information hiding
• Separation logic and abstraction

Cited in

(6)

• Modular verification of procedure equivalence in the presence of memory allocation
• scientific article; zbMATH DE number 1886428 (Why is no real title available?)
• A Technique for Verifying Measurements
• Integrating ADTs in KeY and their application to history-based reasoning about collection
• Integrating ADTs in KeY and Their Application to History-Based Reasoning
• Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)

This page was built for publication: Verification of Equivalent-Results Methods

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