Model checking procedural programs
DOI10.1007/978-3-319-10575-8_17zbMATH Open1392.68226OpenAlexW2804951778MaRDI QIDQ3176375FDOQ3176375
Authors: Ahmed Bouajjani, Javier Esparza, 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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Tools and Algorithms for the Construction and Analysis of Systems
- Visibly pushdown languages
- On Context-Free Languages
- Adding nesting structure to words
- Title not available (Why is that?)
- Precise interprocedural analysis through linear algebra
- Pushdown processes: Games and model-checking
- Efficient CTL model-checking for pushdown systems
- Reachability analysis of pushdown automata: Application to model-checking
- Weighted pushdown systems and their application to interprocedural dataflow analysis
- Title not available (Why is that?)
- Title not available (Why is that?)
- Tools and Algorithms for the Construction and Analysis of Systems
- A fixpoint calculus for local and global program flows
- The theory of ends, pushdown automata, and second-order logic
- Model checking LTL with regular valuations for pushdown systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Model checking the full modal mu-calculus for infinite sequential processes
- Title not available (Why is that?)
- Computer Aided Verification
- A saturation method for the modal \(\mu \)-calculus over pushdown systems
- First-Order and Temporal Logics for Nested Words
- Model checking the full modal mu-calculus for infinite sequential processes
- Winning Regions of Pushdown Parity Games: A Saturation Method
- Title not available (Why is that?)
- On the regular structure of prefix rewriting
- Precise interprocedural dataflow analysis with applications to constant propagation
- Title not available (Why is that?)
- Constrained properties, semilinear systems, and Petri nets
- Stack size analysis for interrupt-driven programs
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems
- Automata Theory and Model Checking
- BDD-Based Symbolic Model Checking
- Program Analysis Using Weighted Pushdown Systems
- Title not available (Why is that?)
- Computing Procedure Summaries for Interprocedural Analysis
- Temporal Logic and Fair Discrete Systems
- AN ALTERNATIVE CONSTRUCTION IN SYMBOLIC REACHABILITY ANALYSIS OF SECOND ORDER PUSHDOWN SYSTEMS
- Tools and Algorithms for the Construction and Analysis of Systems
Cited In (16)
- Model Checking Temporal Properties of Recursive Probabilistic Programs
- Model-checking structured context-free languages
- Compositional verification of sequential programs with procedures
- Title not available (Why is that?)
- Be lazy and don't care: faster CTL model checking for recursive state machines
- Verification of programs with exceptions through operator precedence automata
- Minimization of Visibly Pushdown Automata Using Partial Max-SAT
- Colored nested words
- Procedure extraction to improve scalability of software model checking
- Tools and Algorithms for the Construction and Analysis of Systems
- LTL model checking for recursive programs
- Parameterized verification under TSO with data types
- Faster Algorithms for Weighted Recursive State Machines
- Tools and Algorithms for the Construction and Analysis of Systems
- Temporal Logic and Fair Discrete Systems
- Maximally-Polyvariant Partial Evaluation in Polynomial Time
Uses Software
This page was built for publication: Model checking procedural programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176375)
