Effective generation of verification conditions for non-deterministic unstructured programs

MaRDI QIDQ2882984zbMATH OpenFDO

Authors Igor S. Anureev, Evgeny V. Bodin, Nikolay V. Shilov

Publication date 11 May 2012

Published in Joint Bulletin of the Novosibirsk Computing Center (NCC) and A. P. Ershov Institute of Informatics Systems (IIS). Series: Computer Science (Search for Journal in Brave)

zbMATH Keywords

assertion languageFloyd methodHoare tripleverification conditions

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

• Generation of correctness conditions for imperative programs
• Verification conditions for source-level imperative programs
• Avoiding exponential explosion: generating compact verification conditions
• Verification Condition Generation Via Theorem Proving
• Building verification condition generators by compositional extension

Cited in

(5)

• Refinement-Based Verification of Communicating Unstructured Code
• Verification conditions for source-level imperative programs
• Avoiding exponential explosion: generating compact verification conditions
• Semi-automated reasoning about non-determinism in C expressions
• Generation of correctness conditions for imperative programs

This page was built for publication: Effective generation of verification conditions for non-deterministic unstructured programs

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