Compositional verification of sequential programs with procedures

DOI10.1016/j.ic.2008.03.003zbMath1153.68036OpenAlexW2034063260MaRDI QIDQ937300

Marieke Huisman, Christoph Sprenger, Dilian Gurov

Publication date: 14 August 2008

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2008.03.003

zbMATH Keywords

safety propertiesprogram verificationcompositional reasoningcontrol-flow behaviourmodal \(\mu \)-calculusmaximal modelprivate procedures

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Reducing behavioural to structural properties of programs with procedures ⋮ Conditions of contracts for separating responsibilities in heterogeneous systems ⋮ CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties ⋮ ProMoVer: Modular Verification of Temporal Safety Properties

Uses Software

• MAVEN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Graphical versus logical specifications
• Results on the propositional \(\mu\)-calculus
• Automatic verification methods for finite state systems. International workshop, Grenoble, France, June 12-14, 1989. Proceedings
• Formal methods for smart cards: an experience report
• A lattice-theoretical fixpoint theorem and its applications
• A generic approach to the static analysis of concurrent programs with procedures
• State Space Representation for Verification of Open Systems
• Algebraic laws for nondeterminism and concurrency
• Tools and Algorithms for the Construction and Analysis of Systems
• Mathematical Foundations of Computer Science 2004
• Fundamental Approaches to Software Engineering
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Improving Pushdown System Model Checking
• MAVEN: Modular Aspect Verification
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Rudiments of \(\mu\)-calculus
• Decidability of DPDA equivalence
• Reachability analysis of pushdown automata: Application to model-checking

This page was built for publication: Compositional verification of sequential programs with procedures