E_2+?, hQQH 7Q` _2+?#BHBiv BM S2i`B L2ib
H2t .BtQM M/ _MFQ GxBÉ
.2T`iK2Mi Q7 *QKTmi2` a+B2M+2- lMBp2`bBiv Q7 q`rB+F
*Qp2Mi`v- lMBi2/ EBM;/QK
&H2tM/2`X/BtQM-`XbXHxB+'!r`rB+FX+XmF
#bi`+iX q2 T`2b2Mi E_2+?- iQQH 7Q` /2+B/BM; `2+?#BHBiv BM ;2M@
2`H S2i`B M2ibX h?2 iQQH Bb 7mHH BKTH2K2MiiBQM Q7 EQb`DmǶb Q`B;BMH
RN3k /2+BbBQM T`Q+2/m`2 7Q` `2+?#BHBiv BM oaaX q2 #2HB2p2 i?Bb iQ #2
i?2 }`bi BKTH2K2MiiBQM Q7 Bib FBM/X q2 BM+Hm/2 +QKT`2?2MbBp2 bmBi2 Q7
HB#``B2b 7Q` /2p2HQTK2Mi rBi? o2+iQ` //BiBQM avbi2Kb UrBi? aii2bV BM
i?2 >bF2HH T`Q;`KKBM; HM;m;2X E_2+? b2`p2b b T`+iB+H iQQHM/ +ib b M 2z2+iBp2 i2+?BM; B/ 7Q` i?2 i?2Q`v #2?BM/ i?2 H;Q`Bi?KX
S`2HBKBM`v i2bib bm;;2bi i?i i?2`2 `2 bQK2 +Hbb2b Q7 S2i`B M2ib 7Q`
r?B+? r2 +M [mB+FHv b?Qr mM`2+?#BHBivX AM T`iB+mH`- mbBM; E_2+?
7Q` +Qp2`#BHBiv T`Q#H2Kb- #v `2/m+iBQM iQ `2+?#BHBiv- Bb +QKT2iBiBp2
2p2M ;BMbi bii2@Q7@i?2@`i +Qp2`#BHBiv +?2+F2`bX
E2vrQ`/b, S2i`B L2ib Ǧ EQb`DmǶb H;Q`Bi?K Ǧ _2+?#BHBiv Ǧ o2+iQ`
//BiBQM avbi2Kb Ǧ *Qp2`#BHBiv
R AMi`Q/m+iBQM
S2i`B M2ib (ke) U2[mBpH2MiHv- o2+iQ` //BiBQM avbi2Kb rBi? aii2b (Rk-R9)V `2
QM2 Q7 i?2 #2bi@FMQrM 7Q`KHBbKb BM +QM+m``2M+v i?2Q`vX h?2v 7Q`K ?B;?Hv
2tT`2bbBp2 KQ/2H r?B+? Bb TTHB+#H2 BM #`Q/ `M;2 Q7 /QKBMb BM+Hm/BM;
bQ7ir`2 M/ ?`/r`2 p2`B}+iBQM (8-e)- +?2KB+H KQ/2HHBM; (j)- M/ #mbBM2bb
T`Q+2bb2b (kk)X hrQ Q7 i?2 KQbi bim/B2/ /2+BbBQM T`Q#H2Kb QM S2i`B M2ib `2
i?Qb2 Q7 +Qp2`#BHBiv M/ `2+?#BHBivX
*Qp2`#BHBiv Bb i?2 +2Mi`H /2+BbBQM T`Q#H2K 7Q` p2`B7vBM; b72iv T`QT2`iB2b
QM S2i`B M2ibX h?2 +Qp2`#BHBiv T`Q#H2K bFb- ;Bp2M bi`iBM; +QM};m`iBQM m 0
M/ i`;2i m- r?2i?2` r2 +M `2+?- #v bQK2 b2[m2M+2 Q7 pHB/ i`MbBiBQMb
UBX2X #v `mMV- Mv +QM};m`iBQM m
≥ mX h?2 T`Q#H2K Bb FMQrM iQ #2 1s@
SaS*1@+QKTH2i2 (kj-kd)X *Qp2`#BHBiv ?b b22M +QMbB/2`#H2 bim/v BM `2+2Mi
v2`b- BM T`iB+mH` rBi? pB2r iQr`/b KBMBKBbBM; i?2 `mMMBM; iBK2 Q7 +Qp2`@
#BHBiv /2+BbBQM T`Q+2/m`2b (k-RR)X
h?2 `2+?#BHBiv T`Q#H2K- iQ r?B+? +Qp2`#BHBiv Bb 2bBHv `2/m+B#H2- +M +T@
im`2 #Qi? b72iv M/ HBp2M2bb T`QT2`iB2b Q7 bvbi2Kb (Rj)X 6Q`KHHv- i?2 `2+?#BH@
Biv T`Q#H2K bFb B7 r2 +M- #v bQK2 `mM- ;2i 7`QK bi`iBM; +QM};m`iBQM m 0
iQ i?2 i`;2i +QM};m`iBQM m 2t+iHvX >BbiQ`B+HHv- i?2`2 ?b #22M rB/2 ;T
amTTQ`i2/ #v i?2 *2Mi`2 7Q` .Q+iQ`H h`BMBM; BM l`#M a+B2M+2 M/ S`Q;`2bb U1S@
a_* :`Mi 1SfGyRe9yyfRVX
Ü h?2 mi?Q`UbV kyky
X "B2`2 M/ .X S`F2` U1/bXV, h*a kyky- GL*a Rkyd3- TTX 9y8Ĝ9Rk- kykyX
?iiTb,ff/QBXQ`;fRyXRyydfNd3@j@yjy@98RNy@8nkk
TACAS
Evaluation
Artifact
2020
Accepted
H2t .BtQM M/ _MFQ GxBÉ
.2T`iK2Mi Q7 *QKTmi2` a+B2M+2- lMBp2`bBiv Q7 q`rB+F
*Qp2Mi`v- lMBi2/ EBM;/QK
&H2tM/2`X/BtQM-`XbXHxB+'!r`rB+FX+XmF
#bi`+iX q2 T`2b2Mi E_2+?- iQQH 7Q` /2+B/BM; `2+?#BHBiv BM ;2M@
2`H S2i`B M2ibX h?2 iQQH Bb 7mHH BKTH2K2MiiBQM Q7 EQb`DmǶb Q`B;BMH
RN3k /2+BbBQM T`Q+2/m`2 7Q` `2+?#BHBiv BM oaaX q2 #2HB2p2 i?Bb iQ #2
i?2 }`bi BKTH2K2MiiBQM Q7 Bib FBM/X q2 BM+Hm/2 +QKT`2?2MbBp2 bmBi2 Q7
HB#``B2b 7Q` /2p2HQTK2Mi rBi? o2+iQ` //BiBQM avbi2Kb UrBi? aii2bV BM
i?2 >bF2HH T`Q;`KKBM; HM;m;2X E_2+? b2`p2b b T`+iB+H iQQHM/ +ib b M 2z2+iBp2 i2+?BM; B/ 7Q` i?2 i?2Q`v #2?BM/ i?2 H;Q`Bi?KX
S`2HBKBM`v i2bib bm;;2bi i?i i?2`2 `2 bQK2 +Hbb2b Q7 S2i`B M2ib 7Q`
r?B+? r2 +M [mB+FHv b?Qr mM`2+?#BHBivX AM T`iB+mH`- mbBM; E_2+?
7Q` +Qp2`#BHBiv T`Q#H2Kb- #v `2/m+iBQM iQ `2+?#BHBiv- Bb +QKT2iBiBp2
2p2M ;BMbi bii2@Q7@i?2@`i +Qp2`#BHBiv +?2+F2`bX
E2vrQ`/b, S2i`B L2ib Ǧ EQb`DmǶb H;Q`Bi?K Ǧ _2+?#BHBiv Ǧ o2+iQ`
//BiBQM avbi2Kb Ǧ *Qp2`#BHBiv
R AMi`Q/m+iBQM
S2i`B M2ib (ke) U2[mBpH2MiHv- o2+iQ` //BiBQM avbi2Kb rBi? aii2b (Rk-R9)V `2
QM2 Q7 i?2 #2bi@FMQrM 7Q`KHBbKb BM +QM+m``2M+v i?2Q`vX h?2v 7Q`K ?B;?Hv
2tT`2bbBp2 KQ/2H r?B+? Bb TTHB+#H2 BM #`Q/ `M;2 Q7 /QKBMb BM+Hm/BM;
bQ7ir`2 M/ ?`/r`2 p2`B}+iBQM (8-e)- +?2KB+H KQ/2HHBM; (j)- M/ #mbBM2bb
T`Q+2bb2b (kk)X hrQ Q7 i?2 KQbi bim/B2/ /2+BbBQM T`Q#H2Kb QM S2i`B M2ib `2
i?Qb2 Q7 +Qp2`#BHBiv M/ `2+?#BHBivX
*Qp2`#BHBiv Bb i?2 +2Mi`H /2+BbBQM T`Q#H2K 7Q` p2`B7vBM; b72iv T`QT2`iB2b
QM S2i`B M2ibX h?2 +Qp2`#BHBiv T`Q#H2K bFb- ;Bp2M bi`iBM; +QM};m`iBQM m 0
M/ i`;2i m- r?2i?2` r2 +M `2+?- #v bQK2 b2[m2M+2 Q7 pHB/ i`MbBiBQMb
UBX2X #v `mMV- Mv +QM};m`iBQM m
≥ mX h?2 T`Q#H2K Bb FMQrM iQ #2 1s@
SaS*1@+QKTH2i2 (kj-kd)X *Qp2`#BHBiv ?b b22M +QMbB/2`#H2 bim/v BM `2+2Mi
v2`b- BM T`iB+mH` rBi? pB2r iQr`/b KBMBKBbBM; i?2 `mMMBM; iBK2 Q7 +Qp2`@
#BHBiv /2+BbBQM T`Q+2/m`2b (k-RR)X
h?2 `2+?#BHBiv T`Q#H2K- iQ r?B+? +Qp2`#BHBiv Bb 2bBHv `2/m+B#H2- +M +T@
im`2 #Qi? b72iv M/ HBp2M2bb T`QT2`iB2b Q7 bvbi2Kb (Rj)X 6Q`KHHv- i?2 `2+?#BH@
Biv T`Q#H2K bFb B7 r2 +M- #v bQK2 `mM- ;2i 7`QK bi`iBM; +QM};m`iBQM m 0
iQ i?2 i`;2i +QM};m`iBQM m 2t+iHvX >BbiQ`B+HHv- i?2`2 ?b #22M rB/2 ;T
amTTQ`i2/ #v i?2 *2Mi`2 7Q` .Q+iQ`H h`BMBM; BM l`#M a+B2M+2 M/ S`Q;`2bb U1S@
a_* :`Mi 1SfGyRe9yyfRVX
Ü h?2 mi?Q`UbV kyky
X "B2`2 M/ .X S`F2` U1/bXV, h*a kyky- GL*a Rkyd3- TTX 9y8Ĝ9Rk- kykyX
?iiTb,ff/QBXQ`;fRyXRyydfNd3@j@yjy@98RNy@8nkk
TACAS
Evaluation
Artifact
2020
Accepted