Verifying quantitative temporal properties of procedural programs

DOI10.4230/LIPIcs.CONCUR.2018.15OpenAlexW2889247958MaRDI QIDQ5009429

Mohamed Faouzi Atig, Ahmed Bouajjani, Prakash Saivasan, K. K. Narayan

Publication date: 4 August 2021

Full work available at URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.15

zbMATH Keywords

verificationformal methodspushdown systemsquantitative temporal propertiesvisibly pushdown

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Parikh's theorem: a simple and direct automaton construction
• Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
• Quantitative Interprocedural Analysis
• BOUNDED PARIKH AUTOMATA
• Well-Structured Pushdown Systems
• The Minimal Cost Reachability Problem in Priced Timed Pushdown Systems
• Model Checking Languages of Data Words
• Push-Down Automata with Gap-Order Constraints
• Dense-Timed Pushdown Automata
• Visibly pushdown languages
• First-Order and Temporal Logics for Nested Words
• Visibly Pushdown Automata and Transducers with Counters
• Analyzing Timed Systems Using Tree Automata
• Timed Pushdown Automata Revisited
• The complexity of regular abstractions of one-counter languages
• Automata, Languages and Programming
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Verifying quantitative temporal properties of procedural programs