Reuse in Software Verification by Abstract Method Calls

DOI10.1007/978-3-642-38574-2_21MaRDI QIDQ4928448zbMATH OpenOpenAlexFDO

Authors Reiner Hähnle, Ina Schaefer, Richard Bubel

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_21

Mathematics Subject Classification ID

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

Recommendations

• Reuse of proofs in software verification
• scientific article; zbMATH DE number 1903343
• scientific article; zbMATH DE number 860045
• Algebraic Methodology and Software Technology
• scientific article; zbMATH DE number 1701753
• Verification by abstract interpretation
• Abstraction as the key for invariant verification
• Structural Abstraction of Software Verification Conditions
• Predicate abstraction for software verification

Cited in

(7)

• Schematic program proofs with abstract execution. Theory and applications
• Reuse of proofs in software verification
• An abstract contract theory for programs with procedures
• Hoare-style reasoning from multiple contracts
• Reusing predicate precision in value analysis
• Reusable contracts for safe integration of reinforcement learning in hybrid systems
• Abstract execution

This page was built for publication: Reuse in Software Verification by Abstract Method Calls

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