Verified certification of reachability checking for timed automata

DOI10.1007/978-3-030-45190-5_24MaRDI QIDQ5039522zbMATH OpenOpenAlexFDO

Authors Simon Wimmer, Joshua von Mutius

Publication date 13 October 2022

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

certificationinteractive theorem provingIsabelle/HOLmodel checkingtimed automata

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)

Recommendations

• Verified model checking of timed automata
• Formalized timed automata
• scientific article; zbMATH DE number 1798181
• Verification of timed automata via satisfiability checking
• scientific article; zbMATH DE number 1507209

Cites work

• A mechanized semantic framework for real-time systems
• A theory of timed automata
• Better abstractions for timed automata
• Certifying proofs for SAT-based model checking
• Formal verification of an executable LTL model checker with partial order reduction
• Formalized timed automata
• scientific article; zbMATH DE number 1956585 (Why is no real title available?)
• scientific article; zbMATH DE number 2081113 (Why is no real title available?)
• scientific article; zbMATH DE number 1798181 (Why is no real title available?)
• scientific article; zbMATH DE number 2242593 (Why is no real title available?)
• Imperative Functional Programming with Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Lectures on Concurrency and Petri Nets
• Refinement to Imperative/HOL
• Tools and Algorithms for the Construction and Analysis of Systems
• Verified model checking of timed automata
• Why liveness for timed automata is hard, and what we can do about it

Cited in

(12)

• Decidable verification for reducible timed automata specified in a first order logic with time
• Certifying emptiness of timed Büchi automata
• Verified model checking of timed automata
• Verification for Timed Automata extended with Unbounded Discrete Data Structures
• scientific article; zbMATH DE number 1954132 (Why is no real title available?)
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 5024617 (Why is no real title available?)
• Perspectives of System Informatics
• Certificates for probabilistic pushdown automata via optimistic value iteration
• Explainable online monitoring of metric temporal logic
• Verification of continuous dynamical systems by timed automata
• Progress in certifying hardware model checking results

Describes a project that uses

Uses Software

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

This page was built for publication: Verified certification of reachability checking for timed automata

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