ProMoVer: modular verification of temporal safety properties

DOI10.1007/978-3-642-24690-6_25MaRDI QIDQ3095249zbMATH OpenOpenAlexFDO

Authors Siavash Soleimanifard, Dilian Gurov, Marieke Huisman

Publication date 28 October 2011

Published in Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24690-6_25

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• scientific article; zbMATH DE number 177256
• Verification of Java programs with interacting analysis plugins
• Compositional verification of sequential programs with procedures
• scientific article; zbMATH DE number 177517
• scientific article; zbMATH DE number 1361119

Cites work

• CVPP: a tool set for compositional verification of control-flow safety properties
• Compositional verification of sequential programs with procedures
• First-Order and Temporal Logics for Nested Words
• 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
• Results on the propositional \(\mu\)-calculus
• Sawja: static analysis workshop for Java
• Temporal reasoning for procedural programs
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(7)

• Compositional verification of sequential programs with procedures
• Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints
• ProMoVer
• scientific article; zbMATH DE number 1744961 (Why is no real title available?)
• CVPP: a tool set for compositional verification of control-flow safety properties
• ProMoVer: modular verification of temporal safety properties
• Reducing behavioural to structural properties of programs with procedures

Describes a project that uses

Uses Software

• Moped
• MAVEN
• Sawja
• CVPP

This page was built for publication: ProMoVer: modular verification of temporal safety properties

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