Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm

This is the artifact for paper "Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm" Our benchmark contains three folders: - Validation: We manually annotate TimEffs specifications for a set of synthetic examples (for about 54 programs), to test the main contributions, including: computing effects from symbolic timed programs written in C t ; and the inclusion checking for TimEffs with the parallel composition, block waiting operator and shared global variables. - Experiment1: For 16 C^t programs8, and the annotated temporal specifications are in a 1:1 ratio for succeeded/failed cases. We record the evaluation results in Table 3 in the paper. - Experiment12: comparison with the PAT [16] model checker using real-life Fischer’s mutual exclusion algorithm.