Building verification condition generators by compositional extension

DOI10.1016/J.ENTCS.2006.08.052MaRDI QIDQ2864396zbMATH OpenOpenAlexFDO

Authors A. J. van Leeuwen

Publication date 6 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.08.052

zbMATH Keywords

Hoare logicprogramming language semanticsmonadic logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Recommendations

• A generic intermediate representation for verification condition generation
• Verification Condition Generation Via Theorem Proving
• Compositional Verification for Component-Based Systems and Application
• Automated Assumption Generation for Compositional Verification
• Automated assumption generation for compositional verification
• Verifying generative Casl architectural specifications.

Cites work

• scientific article; zbMATH DE number 1696886 (Why is no real title available?)
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• Composing monads using coproducts
• First-class attribute grammars
• Monad-independent Dynamic Logic in HasCasl

Cited in

(5)

• Verification Condition Generation Via Theorem Proving
• Verification conditions for source-level imperative programs
• Effective generation of verification conditions for non-deterministic unstructured programs
• A generic intermediate representation for verification condition generation
• Avoiding exponential explosion: generating compact verification conditions

Describes a project that uses

Uses Software

• HasCasl

This page was built for publication: Building verification condition generators by compositional extension

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