Formal verification of a Java component using the RESOLVE framework

DOI10.1007/978-3-030-86205-3_16MaRDI QIDQ831953zbMATH OpenOpenAlexFDO

Authors Laine Rumreich, Paolo A. G. Sivilotti

Publication date 24 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-86205-3_16

zbMATH Keywords

modularitybinary decision diagramformal verificationvalue semantics

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Cites work

• scientific article; zbMATH DE number 993744 (Why is no real title available?)
• scientific article; zbMATH DE number 3353170 (Why is no real title available?)
• BDD-based symbolic model checking
• CONCUR 2004 - Concurrency Theory
• Symbolic model checking: \(10^{20}\) states and beyond
• Why3 -- where programs meet provers

Cited in

(1)

• Rule-based programming in Java for protocol verification

Describes a project that uses

Uses Software

• SableJBDD
• Sylvan
• BDD
• JDD
• GitHub
• Rust
• CacBDD
• WhyML
• VeriFast
• VCC
• ESC/Java
• BuDDy
• Spec#
• CUDD
• Why3
• Dafny

This page was built for publication: Formal verification of a Java component using the RESOLVE framework

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