CVPP: a tool set for compositional verification of control-flow safety properties

DOI10.1007/978-3-642-18070-5_8MaRDI QIDQ3067539zbMATH OpenOpenAlexFDO

Authors Marieke Huisman, Dilian Gurov

Publication date 21 January 2011

Published in Formal Verification of Object-Oriented Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-18070-5_8

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

• Compositional verification of sequential programs with procedures
• The code validation tool (CVT). Automatic verification of a compilation process
• ProMoVer: modular verification of temporal safety properties
• Compositional analysis of C/C++ programs with veriSoft
• VCS: a verifier for component-based systems

Cites work

• Compositional verification of sequential programs with procedures
• First-Order and Temporal Logics for Nested Words
• Fundamental Approaches to Software Engineering
• Graphical versus logical specifications
• MAVEN: Modular Aspect Verification
• Modular specification and verification of object-oriented programs
• ProMoVer: modular verification of temporal safety properties
• Reducing Behavioural to Structural Properties of Programs with Procedures
• Reducing behavioural to structural properties of programs with procedures
• Results on the propositional \(\mu\)-calculus
• Temporal reasoning for procedural programs
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(5)

• Compositional verification of sequential programs with procedures
• CVPP
• From safety critical Java programs to timed process models
• ProMoVer: modular verification of temporal safety properties
• Reducing behavioural to structural properties of programs with procedures

Describes a project that uses

Uses Software

• MAVEN
• Spec#

This page was built for publication: CVPP: a tool set for compositional verification of control-flow safety properties

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