Java PathFinder: going to Mars without bugs and deadlocks
summary
Java PathFinder runs model checking on Java bytecode and exhaustively explores thread interleavings to produce deadlock and data-race counterexamples with full execution traces. It finds null pointer and invariant violations, catches misuse of an MPSC queue, and even found a reader‑writer bug in seven minutes that earlier verification missed for decades. Limits include sequential‑consistency only (no weak‑memory guarantees), state‑space explosion, trouble with unbounded spin loops, single‑threaded analysis and the need to extract small, assertion‑rich reproductions.
AI-written summary · about
chapters (5)
- 0:00Start
- 13:01ware model checking
- 22:59line implementation
- 29:48integrity problem
- 30:33cLinkedQueue bug
related talks
52mFinding Bugs Using Path-Sensitive Static Analysis
40mCatching More Bugs with Fewer False Alarms
58mPractical Java Problem Solving: A Hands-On Guide to Debugging
18mPreview: Verification (Correctness & Debugging)
39mLincheck: Testing concurrency on the JVM
31mLincheck: Testing Concurrent Algorithms on JVM
01h 04mDebugging data races
38mStatic Code Analysis - A Behind-the-scenes Look