SAT-based unbounded model checking of timed automata

MaRDI QIDQ5506384zbMATH OpenFDO

Authors Wojciech Penczek, MacIej Szreter

Publication date 28 January 2009

zbMATH Keywords

Fischer's mutual exclusion protocolUMC

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• SAT based bounded model checking with partial order semantics for timed automata
• Towards Bounded Model Checking for the Universal Fragment of TCTL
• Unbounded, fully symbolic model checking of timed automata using Boolean methods.
• Bounded model checking for timed automata
• scientific article; zbMATH DE number 1973987

Cited in

(10)

• Fault localization of timed automata using maximum satisfiability
• Bounded model checking for timed automata
• SAT-based verification for timed component connectors
• SAT-Based Model Checking without Unrolling
• Verification for Timed Automata extended with Unbounded Discrete Data Structures
• SAT based bounded model checking with partial order semantics for timed automata
• Automated Technology for Verification and Analysis
• scientific article; zbMATH DE number 5033900 (Why is no real title available?)
• SAT-BASED MODEL CHECKING FOR REGION AUTOMATA
• Unbounded, fully symbolic model checking of timed automata using Boolean methods.

Describes a project that uses

Uses Software

• Uppaal2k
• VerICS

This page was built for publication: SAT-based unbounded model checking of timed automata

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