Model Checking Procedural Programs

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

Mathematics Subject Classification ID

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

• jMoped
• SLAM
• SPIN
• Bebop
• WALi

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