Generation of correctness conditions for imperative programs

DOI10.1134/S0361768808060029MaRDI QIDQ840060zbMATH OpenOpenAlexFDO

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

Publication date 4 September 2009

Published in Programming and Computer Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1134/s0361768808060029

zbMATH Keywords

Floyd-Hoare

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99)

Recommendations

• Effective generation of verification conditions for non-deterministic unstructured programs
• Verification conditions for source-level imperative programs
• Generating algebraic laws from imperative programs
• Verification conditions are code
• scientific article; zbMATH DE number 3936484

Cites work

• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1956470 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• An axiomatic definition of the programming language Pascal
• Avoiding exponential explosion: generating compact verification conditions
• Effective generation of verification conditions for non-deterministic unstructured programs

Cited in

(5)

• scientific article; zbMATH DE number 1949610 (Why is no real title available?)
• A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences
• Verification conditions for source-level imperative programs
• Effective generation of verification conditions for non-deterministic unstructured programs
• The correctness of a code generator for a functional language

Describes a project that uses

Uses Software

• F@BOOL@

This page was built for publication: Generation of correctness conditions for imperative programs

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