I/O automata in Isabelle/HOL

DOI10.1007/3-540-60579-7_6zbMath1530.68156OpenAlexW1498539321MaRDI QIDQ6061876

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

theorem proverproof obligationparallel compositiontransition relationreachable state

Mathematics Subject Classification ID

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

Cites Work

• The existence of refinement mappings
• Symbolic model checking: \(10^{20}\) states and beyond
• Isabelle. A generic theorem prover
• A fixedpoint approach to implementing (Co)inductive definitions
• Unnamed Item
• Unnamed Item

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