Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs

DOI10.1023/B:FORM.0000040028.49845.67zbMath1090.68020MaRDI QIDQ1888204

John Hatcliff, Matthew B. Dwyer, Robby, Venkatesh-Prasad Ranganath

Publication date: 22 November 2004

Published in: Formal Methods in System Design (Search for Journal in Brave)

zbMATH Keywords

software verificationpartial order reductionescape analysislocking disciplineSoftware model checking

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Dynamic Reductions for Model Checking Concurrent Software, Transparent partial order reduction, Memory model sensitive bytecode verification, Partial Order Reduction for Rewriting Semantics of Programming Languages

Uses Software

• veriSoft
• SPIN
• Bogor
• SymmSpin
• Bandera
• Eraser