Weakest Preconditions for High-Level Programs

DOI10.1007/11841883_31MaRDI QIDQ3541980zbMATH OpenOpenAlexFDO

Authors Karl-Heinz Pennemann, Arend Rensink, Annegret Habel

Publication date 27 November 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11841883_31

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

• Weakest preconditions for pure Prolog programs
• scientific article; zbMATH DE number 3917681
• scientific article; zbMATH DE number 4047056
• Verifying monadic second-order properties of graph programs
• scientific article; zbMATH DE number 3974258

Cited in

(29)

• Weakest precondition semantics for time and concurrency
• Instrumenting a weakest precondition calculus for counterexample generation
• Weakest pre-condition reasoning for Java programs with JML annotations
• Monadic second-order incorrectness logic for GP 2
• Incorrectness logic for graph programs
• Theorem proving graph grammars with attributes and negative application conditions
• On the inherent weakness of conditional primitives
• Weakest preconditioned goto axiom
• Weakest relative precondition semantics. Balancing approved theory and realistic translation verification
• Weakest preconditions for pure Prolog programs
• Verifying monadic second-order properties of graph programs
• High-Level Programs and Program Conditions
• Resolution-Like Theorem Proving for High-Level Conditions
• Development of Correct Graph Transformation Systems
• Application of Graph Transformation in Verification of Dynamic Systems
• Correctness of high-level transformation systems relative to nested conditions
• scientific article; zbMATH DE number 3917681 (Why is no real title available?)
• Some Variants of the Weakest Precondition in Nondeterminism
• scientific article; zbMATH DE number 4022610 (Why is no real title available?)
• scientific article; zbMATH DE number 4047056 (Why is no real title available?)
• scientific article; zbMATH DE number 1949610 (Why is no real title available?)
• scientific article; zbMATH DE number 1927431 (Why is no real title available?)
• scientific article; zbMATH DE number 1531358 (Why is no real title available?)
• Interactive and automated proofs for graph transformations
• scientific article; zbMATH DE number 7456049 (Why is no real title available?)
• An algorithm for approximating the satisfiability problem of high-level conditions
• -adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation
• Reasoning formally about database queries and updates
• Efficient weakest preconditions

Describes a project that uses

Uses Software

• PLUMP

This page was built for publication: Weakest Preconditions for High-Level Programs

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