Verified Certification of Reachability Checking for Timed Automata

DOI10.1007/978-3-030-45190-5_24OpenAlexW3016645482MaRDI QIDQ5039522

Joshua von Mutius, Simon Wimmer

Publication date: 13 October 2022

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-45190-5_24

zbMATH Keywords

timed automatamodel checkingIsabelle/HOLinteractive theorem provingcertification

Mathematics Subject Classification ID

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)

Related Items (1)

Certifying emptiness of timed Büchi automata

Uses Software

• Coq
• Isabelle/HOL
• GitHub
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Better abstractions for timed automata
• Formal verification of an executable LTL model checker with partial order reduction
• A theory of timed automata
• Isabelle/HOL. A proof assistant for higher-order logic
• Certifying proofs for SAT-based model checking
• Verified model checking of timed automata
• Formalized Timed Automata
• A Mechanized Semantic Framework for Real-Time Systems
• Refinement to Imperative/HOL
• Imperative Functional Programming with Isabelle/HOL
• Why Liveness for Timed Automata Is Hard, and What We Can Do About It
• Tools and Algorithms for the Construction and Analysis of Systems
• Lectures on Concurrency and Petri Nets

This page was built for publication: Verified Certification of Reachability Checking for Timed Automata