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

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?)
• 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?)
• Title not available (Why is that?)
• 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)

• 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
• Operator precedence temporal logic and model checking

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)