Zing: A model checker for concurrent software

DOI10.1007/978-3-540-27813-9_42MaRDI QIDQ5312934zbMATH OpenOpenAlexFDO

Authors Jakob Rehof, Yichen Xie, Shaz Qadeer, Sriram K. Rajamani, Tony Andrews

Publication date 25 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b98490

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Zing: Exploiting program structure for model checking concurrent software
• Model checking of concurrent algorithms: from Java to C
• Model checking concurrent programs
• A model checking project at Philips Research
• A modular checker for multithreaded programs

Cited in

(12)

• System-level state equality detection for the formal dynamic verification of legacy distributed applications
• Model checking of concurrent algorithms: from Java to C
• Model checking concurrent programs
• Verification of STM on relaxed memory models
• Zing: Exploiting program structure for model checking concurrent software
• Extracting Zing Models from C Source Code
• FocusCheck: A tool for model checking and debugging sequential C programs
• Model checking Z specifications using SAL
• Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving
• A rewriting logic semantics for the analysis of \textsf{P} programs
• Question-guided stubborn set methods for state properties
• CSP is a retract of CCS

Describes a project that uses

Uses Software

• Zing
• Bogor
• SLAM
• dSPIN
• SPIN

This page was built for publication: Zing: A model checker for concurrent software

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5312934)