scientific article; zbMATH DE number 2185692

MaRDI QIDQ3024875zbMATH OpenFDO

Authors Sara Kalvala

Publication date 4 July 2005

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 910717
• scientific article; zbMATH DE number 1476493
• An embedding of timed transition systems in \(HOL\)
• scientific article; zbMATH DE number 1301859
• scientific article; zbMATH DE number 1405446

Cited in

(13)

• An embedding of timed transition systems in \(HOL\)
• Formal proof of a machine closed theorem in Coq
• Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
• An Axiomatic Value Model for Isabelle/UTP
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• scientific article; zbMATH DE number 1301859 (Why is no real title available?)
• TLA +  Proofs
• scientific article; zbMATH DE number 2172804 (Why is no real title available?)
• scientific article; zbMATH DE number 910717 (Why is no real title available?)
• scientific article; zbMATH DE number 1390253 (Why is no real title available?)
• scientific article; zbMATH DE number 1405446 (Why is no real title available?)
• Proving linearizability with temporal logic
• Inference rules for programming languages with side effects in expressions

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication:

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