Reducing behavioural to structural properties of programs with procedures
DOI10.1016/j.tcs.2013.02.006zbMath1291.68259OpenAlexW2164285951MaRDI 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 propertiesmodal \(\mu\)-calculusprogram verificationcompositional reasoningcontrol-flow behaviourcontrol-flow structure
Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (1)
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
This page was built for publication: Reducing behavioural to structural properties of programs with procedures
