#5 #6 #7 #8 #15 #16 #18 #19 #22
10
2
10
3
10
4
time (ms)
aggress.
approx.
exact
#5 #6 #7 #8 #15 #16 #18 #19 #22
10
0
10
1
10
2
10
3
repair and assumption sizes
repair size
assumption size
Fig. 6: Comparing repair methods: time and repair size (logarithmic scale).
Example #22 models a simple structure in which, due to a loop in M 2 , the same alphabet sequence can
generate infinitely many error traces. The exact repair method timed out, since it attempted removing one
error trace at a time. On the other hand, the aggressive method removed all accepting states, creating an
empty program – a trivial (yet valid) repair. However, the approximate method created a valid, non-trivial
repair.
Conclusion AGR offers a new take on the learning-based approach to assume-guarantee verification, and
manages coping with complex properties and repairing infinite-state programs. Our experimental results
show that using existing semantic tools, AGR produces very succinct proofs, and quickly and efficiently
repairs flawed communicating programs.
References
1. http://hfrenkel.cswp.cs.technion.ac.il/agr-full-version/.
2. https://www.dropbox.com/sh/oi1joxvjuv5p3ag/AACOMDB6wGevkFogilQUyfXqa?dl=0.
3. A. Albarghouthi, I. Dillig, and A. Gurfinkel. Maximal specification synthesis. In POPL, 2016.
4. B. Alpern, M. N. Wegman, and F. K. Zadeck. Detecting equality of variables in programs. In POPL, 1988.
5. D. Angluin. Learning regular sets from queries and counterexamples. Inf. Comput., 75(2):87–106, 1987.
6. S. Chaki and O. Strichman. Optimized l*-based assume-guarantee reasoning. In TACAS, 2007.
7. Y.-F. Chen, E. M. Clarke, A. Farzan, M.-H. Tsai, Y.-K. Tsay, and B.-Y. Wang. Automated assume-guarantee
reasoning through implicit learning. In CAV, 2010.
8. Y.-F. Chen, A. Farzan, E. M. Clarke, Y.-K. Tsay, and B.-Y. Wang. Learning minimal separating DFA’s for compositional verification. In TACAS, 2009.
9. J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu. Learning assumptions for compositional verification. In
TACAS, 2003.
10. L. De Moura and N. Bjørner. Z3: An efficient smt solver. In TACAS, 2008.
11. I. Dillig and T. Dillig. Explain: A tool for performing abductive inference. In CAV, 2013.
12. K. A. Elkader, O. Grumberg, C. S. Pasareanu, and S. Shoham. Automated circular assume-guarantee reasoning. In
FM, 2015.
13. K. A. Elkader, O. Grumberg, C. S. Pasareanu, and S. Shoham. Automated circular assume-guarantee reasoning
with n-way decomposition and alphabet refinement. In CAV, 2016.
14. M. Gheorghiu, D. Giannakopoulou, and C. S. Pasareanu. Refining interface alphabets for compositional verification. In TACAS, 2007.
15. D. Giannakopoulou, C. S. Pasareanu, and H. Barringer. Assumption generation for software component verification. In ASE. IEEE Computer Society, 2002.
226
H. Frenkel et al.
10
2
10
3
10
4
time (ms)
aggress.
approx.
exact
#5 #6 #7 #8 #15 #16 #18 #19 #22
10
0
10
1
10
2
10
3
repair and assumption sizes
repair size
assumption size
Fig. 6: Comparing repair methods: time and repair size (logarithmic scale).
Example #22 models a simple structure in which, due to a loop in M 2 , the same alphabet sequence can
generate infinitely many error traces. The exact repair method timed out, since it attempted removing one
error trace at a time. On the other hand, the aggressive method removed all accepting states, creating an
empty program – a trivial (yet valid) repair. However, the approximate method created a valid, non-trivial
repair.
Conclusion AGR offers a new take on the learning-based approach to assume-guarantee verification, and
manages coping with complex properties and repairing infinite-state programs. Our experimental results
show that using existing semantic tools, AGR produces very succinct proofs, and quickly and efficiently
repairs flawed communicating programs.
References
1. http://hfrenkel.cswp.cs.technion.ac.il/agr-full-version/.
2. https://www.dropbox.com/sh/oi1joxvjuv5p3ag/AACOMDB6wGevkFogilQUyfXqa?dl=0.
3. A. Albarghouthi, I. Dillig, and A. Gurfinkel. Maximal specification synthesis. In POPL, 2016.
4. B. Alpern, M. N. Wegman, and F. K. Zadeck. Detecting equality of variables in programs. In POPL, 1988.
5. D. Angluin. Learning regular sets from queries and counterexamples. Inf. Comput., 75(2):87–106, 1987.
6. S. Chaki and O. Strichman. Optimized l*-based assume-guarantee reasoning. In TACAS, 2007.
7. Y.-F. Chen, E. M. Clarke, A. Farzan, M.-H. Tsai, Y.-K. Tsay, and B.-Y. Wang. Automated assume-guarantee
reasoning through implicit learning. In CAV, 2010.
8. Y.-F. Chen, A. Farzan, E. M. Clarke, Y.-K. Tsay, and B.-Y. Wang. Learning minimal separating DFA’s for compositional verification. In TACAS, 2009.
9. J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu. Learning assumptions for compositional verification. In
TACAS, 2003.
10. L. De Moura and N. Bjørner. Z3: An efficient smt solver. In TACAS, 2008.
11. I. Dillig and T. Dillig. Explain: A tool for performing abductive inference. In CAV, 2013.
12. K. A. Elkader, O. Grumberg, C. S. Pasareanu, and S. Shoham. Automated circular assume-guarantee reasoning. In
FM, 2015.
13. K. A. Elkader, O. Grumberg, C. S. Pasareanu, and S. Shoham. Automated circular assume-guarantee reasoning
with n-way decomposition and alphabet refinement. In CAV, 2016.
14. M. Gheorghiu, D. Giannakopoulou, and C. S. Pasareanu. Refining interface alphabets for compositional verification. In TACAS, 2007.
15. D. Giannakopoulou, C. S. Pasareanu, and H. Barringer. Assumption generation for software component verification. In ASE. IEEE Computer Society, 2002.
226
H. Frenkel et al.