Formalized Timed Automata

DOI10.1007/978-3-319-43144-4_26zbMath1478.68183OpenAlexW2499128759MaRDI QIDQ2829277

Simon Wimmer

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_26

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Verified Certification of Reachability Checking for Timed Automata

Uses Software

• Isabelle
• Kronos
• Isabelle/HOL
• PVS
• HyTech
• Uppaal
• HOL
• Timed Automata
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theory of timed automata
• HyTech: A model checker for hybrid systems
• Kronos: A verification tool for real-time systems
• Uppaal in a nutshell
• Forward analysis of updatable timed automata
• A Mechanized Semantic Framework for Real-Time Systems
• Parametric real-time reasoning
• Lectures on Concurrency and Petri Nets

This page was built for publication: Formalized Timed Automata