Syntax-directed model checking of sequential programs

DOI10.1016/S1567-8326(02)00035-8zbMath1008.68075OpenAlexW2000953224MaRDI QIDQ1858441

Karen Yorav, Orna Grumberg

Publication date: 13 February 2003

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s1567-8326(02)00035-8

zbMATH Keywords

temporal logic model checking of sequential programs

Mathematics Subject Classification ID

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

Uses Software

• veriSoft
• SPIN
• Java PathFinder
• Bandera
• CESAR
• Bebop
• dSPIN

Cites Work

• Precise interprocedural dataflow analysis with applications to constant propagation
• The temporal semantics of concurrent programs
• Symbolic model checking: \(10^{20}\) states and beyond
• Model checking JAVA programs using JAVA PathFinder
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• “Sometimes” and “not never” revisited
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Syntax-directed model checking of sequential programs