I/O automata in Isabelle/HOL

DOI10.1007/3-540-60579-7_6MaRDI QIDQ6061876zbMATH OpenOpenAlexFDO

Authors Tobias Nipkow, Konrad Slind

Publication date 8 December 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-60579-7_6

zbMATH Keywords

parallel compositionproof obligationreachable statetheorem provertransition relation

Mathematics Subject Classification ID

Network protocols (68M12) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1301859
• scientific article; zbMATH DE number 1277257
• scientific article; zbMATH DE number 1424022
• scientific article; zbMATH DE number 1973995
• Proving invariants of I/O automata with TAME

Cites work

• A fixedpoint approach to implementing (co)inductive definitions
• scientific article; zbMATH DE number 4084989 (Why is no real title available?)
• scientific article; zbMATH DE number 4110131 (Why is no real title available?)
• Isabelle. A generic theorem prover
• Symbolic model checking: \(10^{20}\) states and beyond
• The existence of refinement mappings

Cited in

(4)

• scientific article; zbMATH DE number 1670757 (Why is no real title available?)
• scientific article; zbMATH DE number 4213439 (Why is no real title available?)
• scientific article; zbMATH DE number 139804 (Why is no real title available?)
• Modal I/O Automata for Interface and Product Line Theories

This page was built for publication: I/O automata in Isabelle/HOL

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