Model Checking Procedural Programs
DOI10.1007/978-3-319-10575-8_17zbMATH Open1392.68226OpenAlexW2804951778MaRDI QIDQ3176375FDOQ3176375
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
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Tools and Algorithms for the Construction and Analysis of Systems
- Visibly pushdown languages
- On Context-Free Languages
- Adding nesting structure to words
- 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
- 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
- Model checking the full modal mu-calculus for infinite sequential processes
- 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
- On the regular structure of prefix rewriting
- Precise interprocedural dataflow analysis with applications to constant propagation
- 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
- 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 (11)
- Model Checking Temporal Properties of Recursive Probabilistic Programs
- Model-checking structured context-free languages
- 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
- Parameterized verification under TSO with data types
- Faster Algorithms for Weighted Recursive State Machines
- 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)
