A novel approach to verifying context free properties of programs

DOI10.1016/j.tcs.2020.01.005zbMath1436.68200OpenAlexW2998933178WikidataQ126384761 ScholiaQ126384761MaRDI QIDQ2290651

Zhenhua Duan, Nan Zhang, Cong Tian, Hongwei David Du

Publication date: 29 January 2020

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2020.01.005

zbMATH Keywords

algorithmautomatamodel checkingtemporal logicruntime verification

Mathematics Subject Classification ID

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

Uses Software

• z3
• CPAchecker
• CESAR
• Murphi
• MSVL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A mechanism of function calls in MSVL
• A cylinder computation model for many-core parallel computing
• Results on the propositional \(\mu\)-calculus
• An experience in proving regular networks of processes by modular model checking
• A compiler for MSVL and its applications
• A structural induction theorem for processes
• Decision procedures and expressiveness in the temporal logic of branching time
• Counterexample-guided abstraction refinement for symbolic model checking
• Complexity of propositional projection temporal logic with star
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• The complexity of propositional linear temporal logics
• Reasoning about systems with many processes
• Complete Proof System for QPTL
• Symbolic model checking with rich assertional languages

This page was built for publication: A novel approach to verifying context free properties of programs