Model-checking structured context-free languages

DOI10.1007/978-3-030-81688-9_18zbMATH Open1493.68207OpenAlexW3185983707MaRDI QIDQ832277FDOQ832277

Authors Michele Chiari, Dino Mandrioli, 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)

Recommendations

• Operator precedence temporal logic and model checking
• Verification of programs with exceptions through operator precedence automata
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 5245252
• Model Checking: From Tools to Theory

Cites work

• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1670780 (Why is no real title available?)
• scientific article; zbMATH DE number 7447741 (Why is no real title available?)
• scientific article; zbMATH DE number 7447746 (Why is no real title available?)
• scientific article; zbMATH DE number 3696500 (Why is no real title available?)
• scientific article; zbMATH DE number 3639163 (Why is no real title available?)
• scientific article; zbMATH DE number 1232241 (Why is no real title available?)
• scientific article; zbMATH DE number 1982210 (Why is no real title available?)
• scientific article; zbMATH DE number 1980931 (Why is no real title available?)
• scientific article; zbMATH DE number 1903366 (Why is no real title available?)
• scientific article; zbMATH DE number 5245252 (Why is no real title available?)
• Adding nesting structure to words
• Analysis of Boolean Programs
• Computer Aided Verification
• Constrained properties, semilinear systems, and Petri nets
• First-Order and Temporal Logics for Nested Words
• Generalizing input-driven languages: theoretical and practical benefits
• Handbook of model checking
• Model checking LTL with regular valuations for pushdown systems
• Model checking procedural programs
• Model checking the full modal mu-calculus for infinite sequential processes
• Operator Precedence Languages: Their Automata-Theoretic and Logic Characterization
• Operator precedence and the visibly pushdown property
• Operator precedence temporal logic and model checking
• Parenthesis Grammars
• Parsing Techniques
• Predicate abstraction for program verification
• Pushdown processes: Games and model-checking
• Reachability analysis of pushdown automata: Application to model-checking
• Stack size analysis for interrupt-driven programs
• Star-freeness, first-order definability and aperiodicity of structured context-free languages
• Syntactic Analysis and Operator Precedence
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Visibly linear temporal logic
• Visibly pushdown languages

Cited in

(5)

• Verification of programs with exceptions through operator precedence automata
• Model Checking for String Problems
• Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages
• Operator precedence temporal logic and model checking
• scientific article; zbMATH DE number 7577575 (Why is no real title available?)

Describes a project that uses

Uses Software

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

This page was built for publication: Model-checking structured context-free languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832277)