Schematic program proofs with abstract execution. Theory and applications

DOI10.1007/S10817-023-09692-0MaRDI QIDQ6552501zbMATH OpenFDO

Authors Dominic Steinhöfel, Reiner Hähnle

Publication date 10 June 2024

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

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-023-09692-0

zbMATH Keywords

deductive verificationprogram transformationschematic programssecond-order program propertiessymbolic execution

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Abstract execution
• Certified abstract cost analysis
• Towards a Generic Framework for Trustworthy Program Refactoring
• Systematic design of program transformation frameworks by abstract interpretation
• scientific article; zbMATH DE number 4024753

Cites work

• A complete uniform substitution calculus for differential dynamic logic
• A program logic for dependence analysis
• Abstract execution
• An axiomatic basis for computer programming
• Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
• Certified abstract cost analysis
• Deductive software verification: from pen-and-paper proofs to industrial tools
• Dynamic frames in Java dynamic logic
• Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
• Formal Program Verification Using Symbolic Execution
• From program verification to program synthesis
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 3798996 (Why is no real title available?)
• scientific article; zbMATH DE number 3322506 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Modeling in Event B. System and software engineering.
• Parallel programming with a pattern language
• Program development by stepwise refinement
• Reuse in Software Verification by Abstract Method Calls
• Software Product Line Engineering
• Static semantics, types, and binding time analysis
• Symbolic execution and program testing
• The B-Book
• The correctness-by-construction approach to programming
• The dynamic frames theory
• The Lean 4 theorem prover and programming language
• The trace modality

Cited in

(1)

• Abstract execution

This page was built for publication: Schematic program proofs with abstract execution. Theory and applications

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