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

<p>This is the artifact for paper</p> <p>&quot;Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm&quot;</p> <p>The latest code can be found in&nbsp;https://github.com/songyahui/Timed_Verification</p> <p>Our benchmark contains three folders:</p> <p>- 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&nbsp;waiting operator and shared global variables.</p> <p>- Experiment1: For 16 C^t programs, 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.</p> <p>- Experiment12: comparison with the PAT [16] model checker using real-life Fischer&rsquo;s mutual exclusion algorithm.</p>