Model-checking structured context-free languages

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

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

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

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)

Cites Work

• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• Visibly pushdown languages
• Adding nesting structure to words
• Parenthesis Grammars
• Pushdown processes: Games and model-checking
• Title not available (Why is that?)
• Reachability analysis of pushdown automata: Application to model-checking
• Title not available (Why is that?)
• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• Model checking LTL with regular valuations for pushdown systems
• Title not available (Why is that?)
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• First-Order and Temporal Logics for Nested Words
• Parsing Techniques
• Model checking the full modal mu-calculus for infinite sequential processes
• Title not available (Why is that?)
• Syntactic Analysis and Operator Precedence
• Constrained properties, semilinear systems, and Petri nets
• Stack size analysis for interrupt-driven programs
• Operator precedence and the visibly pushdown property
• Operator Precedence Languages: Their Automata-Theoretic and Logic Characterization
• Analysis of Boolean Programs
• Handbook of Model Checking
• Generalizing input-driven languages: theoretical and practical benefits
• Star-freeness, first-order definability and aperiodicity of structured context-free languages
• Operator precedence temporal logic and model checking
• Predicate Abstraction for Program Verification
• Model Checking Procedural Programs
• Visibly Linear Temporal Logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (4)

• Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages
• Title not available (Why is that?)
• Model Checking for String Problems
• Verification of programs with exceptions through operator precedence automata

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)