2 papers
cs.FL2026
TARZAN: A Region-Based Library for Forward and Backward Reachability of Timed Automata (Extended Version)
Andrea Manini, Matteo Rossi, Pierluigi San Pietro
The zone abstraction, widely adopted for its notable practical efficiency, is the de facto standard in the verification of Timed Automata (TA). Nonetheless, region-based abstractio…
cs.FL2025
Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation
Andrea Manini, Matteo Rossi, Pierluigi San Pietro
A key challenge in formal verification, particularly in Model Checking, is ensuring the correctness of the verification tools. Erroneous results on complex models can be difficult…