(Abstraction and Refinement of) Timed Constraint Automata in the ECT

In this talk, I will give a tool demonstration of how Timed Constraint Automata (TCA) have been integrated into the ECT. In particular, I will present the TCA editor, the translation into propositional formulas plus linear arithmetic, and the abstraction-refinement backend used for model checking.  

hosted by