Reducing behavioural to structural properties of programs with procedures
From MaRDI portal
Publication:385023
DOI10.1016/j.tcs.2013.02.006zbMath1291.68259MaRDI QIDQ385023
Publication date: 29 November 2013
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2013.02.006
safety properties; modal \(\mu\)-calculus; program verification; compositional reasoning; control-flow behaviour; control-flow structure
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Graphical versus logical specifications
- Results on the propositional \(\mu\)-calculus
- Compositional verification of sequential programs with procedures
- An automata theoretic decision procedure for the propositional mu- calculus
- Weighted pushdown systems and their application to interprocedural dataflow analysis
- CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties
- ProMoVer: Modular Verification of Temporal Safety Properties
- On the power of abstract interpretation
- Model Checking Recursive Programs with Exact Predicate Abstraction
- Reducing Behavioural to Structural Properties of Programs with Procedures
- Temporal Reasoning for Procedural Programs
- -Calculus with Explicit Points and Approximations
- Tools and Algorithms for the Construction and Analysis of Systems
- A fixpoint calculus for local and global program flows
- Fundamental Approaches to Software Engineering
- Tools and Algorithms for the Construction and Analysis of Systems
- Languages of Nested Trees
- MAVEN: Modular Aspect Verification
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Decidability of DPDA equivalence
- Modular specification and verification of object-oriented programs
