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

DOI10.1007/S10703-005-1491-3MaRDI QIDQ816196zbMATH OpenOpenAlexFDO

Authors Radu Iosif, Matthew B. Dwyer, John Hatcliff

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

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

Recommendations

• scientific article; zbMATH DE number 1860613
• scientific article; zbMATH DE number 1863159
• ZB 2005: Formal Specification and Development in Z and B
• scientific article; zbMATH DE number 1953278
• Model checking JAVA programs using JAVA PathFinder

Cites work

• A partial order approach to branching time logic model checking.
• Branching time and abstraction in bisimulation semantics
• scientific article; zbMATH DE number 1617328 (Why is no real title available?)
• scientific article; zbMATH DE number 1670550 (Why is no real title available?)
• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1670561 (Why is no real title available?)
• scientific article; zbMATH DE number 1670562 (Why is no real title available?)
• scientific article; zbMATH DE number 1670783 (Why is no real title available?)
• scientific article; zbMATH DE number 1701765 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3936469 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 1953278 (Why is no real title available?)
• scientific article; zbMATH DE number 1746648 (Why is no real title available?)
• scientific article; zbMATH DE number 2087625 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 1905116 (Why is no real title available?)
• scientific article; zbMATH DE number 3415379 (Why is no real title available?)
• Lazy abstraction
• 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
• Slicing software for model construction
• Three logics for branching bisimulation
• Tools and Algorithms for the Construction and Analysis of Systems
• Verifying safety properties of concurrent Java programs using 3-valued logic

Cited in

(5)

• scientific article; zbMATH DE number 1953278 (Why is no real title available?)
• scientific article; zbMATH DE number 1744966 (Why is no real title available?)
• scientific article; zbMATH DE number 1860613 (Why is no real title available?)
• scientific article; zbMATH DE number 1863159 (Why is no real title available?)
• A translator of Java programs to TADDs

Describes a project that uses

Uses Software

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

This page was built for publication: Translating Java for multiple model checkers: The Bandera back-end

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