Synthia: Verification and synthesis for timed automata. Synthia is the first certifying model checker for open real-time systems modeled as networks of timed automata. The key innovation of Synthia is its ability to justify why a given system is correct by providing a correctness certificate to the user. Such certificates are easy-to-validate deductive proofs that only reflect the specification-critical properties of the system. Synthia can also handle partially implemented systems, in which case it certifies their realizability by synthesizing reference implementations for the unimplemented parts. In the analysis of timed automata, the main technical challenge is to efficiently represent the arising infinite state space. Synthia’s analysis algorithm is based on a novel abstraction refinement technique that enables a clean combination of binary decision diagrams with difference bound matrices for a symbolic representation of both the discrete control-related and the continuous part of the state space.