Translating Java for multiple model checkers: The Bandera back-end

DOI10.1007/s10703-005-1491-3zbMath1086.68557MaRDI QIDQ816196

John Hatcliff, Radu Iosif, Matthew B. Dwyer

Publication date: 20 February 2006

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

Full work available at URL: https://doi.org/10.1007/s10703-005-1491-3

zbMATH Keywords

Bandera intermediate representation

Mathematics Subject Classification ID

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

Uses Software

• veriSoft
• SyncGen
• IF-2.0
• SPIN
• PVS
• NuSMV
• Java PathFinder
• Bandera
• Bebop
• TVLA
• dSPIN

Cites Work

• Slicing software for model construction
• A partial order approach to branching time logic model checking.
• Model checking JAVA programs using JAVA PathFinder
• NuSMV: A new symbolic model checker
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Three logics for branching bisimulation
• Branching time and abstraction in bisimulation semantics
• Verifying safety properties of concurrent Java programs using 3-valued logic
• Lazy abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item