Formal verification of a Java component using the RESOLVE framework

DOI10.1007/978-3-030-86205-3_16OpenAlexW3198714731MaRDI QIDQ831953

Paolo A. G. Sivilotti, Laine Rumreich

Publication date: 24 March 2022

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

zbMATH Keywords

formal verificationmodularitybinary decision diagramvalue semantics

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Uses Software

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

Cites Work

• Symbolic model checking: \(10^{20}\) states and beyond
• BDD-Based Symbolic Model Checking
• CONCUR 2004 - Concurrency Theory
• Why3 — Where Programs Meet Provers
• Unnamed Item
• Unnamed Item

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