Benchmark for work "Temporal Verification of Mixed Sync-Async Execution Models"

<p>This benchmark is for validation and evaluation purpose for&nbsp;<br> the work &quot;Temporal Verification of Mixed Sync-Async Execution&nbsp;<br> Models&quot;. It is constructed by manually annotating ASyncEffs<br> specifications, including both succeeded and failed cases.&nbsp;</p> <p>This benchmark consists two folders:<br> 1. validation_tests:&nbsp;<br> The validation tests are synthetic examples to test&nbsp;<br> the main contributions, including the preemption interleaving computation and&nbsp;<br> the inclusion checking for the parallel composition and the waiting operator.&nbsp;</p> <p>2. evaluation_tests:<br> We select 16 programs, varying from 15 lines to 300 lines, and &nbsp;annotate&nbsp;<br> ASyncEffs specifications<br> with a 1:1 ratio for succeeded/failed cases.&nbsp;</p>