Model-checking structured context-free languages

DOI10.1007/978-3-030-81688-9_18zbMath1493.68207OpenAlexW3185983707MaRDI QIDQ832277

Dino Mandrioli, Michele Chiari, Matteo Pradella

Publication date: 25 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81688-9_18

zbMATH Keywords

model checkinglinear temporal logicvisibly pushdown languagesinput-driven languagesoperator-precedence languages

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

Verification of programs with exceptions through operator precedence automata ⋮ Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages ⋮ Unnamed Item

Uses Software

• BLAST
• SPIN
• Bebop
• Java-MOP
• GitHub
• VPAlib
• OpenNWA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Stack size analysis for interrupt-driven programs
• Generalizing input-driven languages: theoretical and practical benefits
• Operator precedence and the visibly pushdown property
• 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
• Star-freeness, first-order definability and aperiodicity of structured context-free languages
• Operator precedence temporal logic and model checking
• Operator Precedence Languages: Their Automata-Theoretic and Logic Characterization
• Predicate Abstraction for Program Verification
• Model Checking Procedural Programs
• Visibly Linear Temporal Logic
• Adding nesting structure to words
• Visibly pushdown languages
• First-Order and Temporal Logics for Nested Words
• Handbook of Model Checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Analysis of Boolean Programs
• Syntactic Analysis and Operator Precedence
• Parsing Techniques
• Parenthesis Grammars
• Tools and Algorithms for the Construction and Analysis of 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