Model Checking Procedural Programs
From MaRDI portal
Publication:3176375
DOI10.1007/978-3-319-10575-8_17zbMath1392.68226OpenAlexW2804951778MaRDI QIDQ3176375
Javier Esparza, Ahmed Bouajjani, Rajeev Alur
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.644.4883
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (10)
Model-checking structured context-free languages ⋮ Temporal Logic and Fair Discrete Systems ⋮ Maximally-Polyvariant Partial Evaluation in Polynomial Time ⋮ Colored nested words ⋮ Verification of programs with exceptions through operator precedence automata ⋮ Be lazy and don't care: faster CTL model checking for recursive state machines ⋮ Model Checking Temporal Properties of Recursive Probabilistic Programs ⋮ Faster Algorithms for Weighted Recursive State Machines ⋮ Minimization of Visibly Pushdown Automata Using Partial Max-SAT ⋮ Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A saturation method for the modal \(\mu \)-calculus over pushdown systems
- Precise interprocedural dataflow analysis with applications to constant propagation
- On the regular structure of prefix rewriting
- Stack size analysis for interrupt-driven programs
- The theory of ends, pushdown automata, and second-order logic
- Pushdown processes: Games and model-checking
- Model checking LTL with regular valuations for pushdown systems
- Model checking the full modal mu-calculus for infinite sequential processes
- Weighted pushdown systems and their application to interprocedural dataflow analysis
- Efficient CTL Model-Checking for Pushdown Systems
- Temporal Logic and Fair Discrete Systems
- Automata Theory and Model Checking
- BDD-Based Symbolic Model Checking
- Winning Regions of Pushdown Parity Games: A Saturation Method
- Adding nesting structure to words
- Precise interprocedural analysis through linear algebra
- AN ALTERNATIVE CONSTRUCTION IN SYMBOLIC REACHABILITY ANALYSIS OF SECOND ORDER PUSHDOWN SYSTEMS
- Visibly pushdown languages
- First-Order and Temporal Logics for Nested Words
- Model checking the full modal mu-calculus for infinite sequential processes
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- A fixpoint calculus for local and global program flows
- Program Analysis Using Weighted Pushdown Systems
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- On Context-Free Languages
- Tools and Algorithms for the Construction and Analysis of Systems
- Computing Procedure Summaries for Interprocedural Analysis
- Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Reachability analysis of pushdown automata: Application to model-checking
- Constrained properties, semilinear systems, and Petri nets
This page was built for publication: Model Checking Procedural Programs
