scientific article; zbMATH DE number 1301859

zbMath0927.03024MaRDI QIDQ4247083

Olaf Mueller

Publication date: 16 June 1999

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

model checkingtemporal logicabstraction theoryverification framework for I/O automata in Isabelle

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Related Items (5)

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory ⋮ Mechanized proofs of opacity: a comparison of two techniques ⋮ A Formalized Theory for Verifying Stability and Convergence of Automata in PVS ⋮ Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations ⋮ Unnamed Item

Uses Software

• Isabelle

This page was built for publication: