Building verification condition generators by compositional extension

DOI10.1016/J.ENTCS.2006.08.052zbMATH Open1277.68062OpenAlexW2155833178MaRDI QIDQ2864396FDOQ2864396

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

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.

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Monad-independent Dynamic Logic in HasCasl
• Composing monads using coproducts
• Title not available (Why is that?)
• First-class attribute grammars

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
• Avoiding exponential explosion: generating compact verification conditions
• A generic intermediate representation for verification condition generation

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)