38
S. Chakraborty et al.
Data Availability Statement
The datasets generated and analyzed during the current study are available in
the figshare repository: https://doi.org/10.6084/m9.figshare.11875428.v1
References
1. Alberti, F., Ghilardi, S., Sharygina, N.: Booster: An acceleration-based verification
framework for array programs. In: Proc. of ATVA. pp. 18–23 (2014)
2. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis
for combined theories. In: Proc. of VMCAI. pp. 378–394 (2007)
3. Chakraborty,
S.,
Gupta,
A.,
Unadkat,
D.:
Verifying
array
manipulating
programs
with
full-program
induction,
https://www.cse.iitb.ac.in/ ∼ supratik/publications/papers/FPI longversion.html
4. Chakraborty, S., Gupta, A., Unadkat, D.: Verifying Array Manipulating Programs
by Tiling. In: Proc. of SAS. pp. 428–449 (2017)
5. Chakraborty, S., Gupta, A., Unadkat, D.: Verifying Array Manipulating Programs with Full-program Induction - Artifacts TACAS 2020. Figshare (2020).
https://doi.org/10.6084/m9.figshare.11875428.v1
6. Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. FMSD 19(1), 7–34 (2001)
7. Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully
automatic and scalable array content analysis. In: Proc. of POPL. pp. 105–118
(2011)
8. Darke, P., Prabhu, S., Chimdyalwar, B., Chauhan, A., Kumar, S., Basakchowdhury, A., Venkatesh, R., Datar, A., Medicherla, R.K.: VeriAbs: Verification by
abstraction and test generation. In: TACAS (Competition Contribution). pp. 457–
462 (2018)
9. Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S.,
Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1-3), 35–45 (2007)
10. Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via
syntax-guided-synthesis. In: Proc. of CAV. pp. 259–277 (2019)
11. Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and
its use in optimization. TOPLAS 9(3), 319–349 (1987)
12. Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In:
Proc. of FME. pp. 500–517 (2001)
13. Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array
operations. In: Proc. of POPL. pp. 338–350 (2005)
14. Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified
logical domains. In: Proc. of POPL. pp. 235–246 (2008)
15. Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Proc. of ATVA.
pp. 248–266 (2018)
16. Halbwachs, N., P´ eron, M.: Discovering properties about arrays in simple programs.
In: Proc. of PLDI. pp. 339–348 (2008)
17. Henzinger, T.A., Hottelier, T., Kov´ acs, L., Rybalchenko, A.: Aligators for arrays
(tool paper). In: Proc. of LPAR. pp. 348–356 (2010)
18. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.:
VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Proc. of
NFM. pp. 41–55 (2011)
S. Chakraborty et al.
Data Availability Statement
The datasets generated and analyzed during the current study are available in
the figshare repository: https://doi.org/10.6084/m9.figshare.11875428.v1
References
1. Alberti, F., Ghilardi, S., Sharygina, N.: Booster: An acceleration-based verification
framework for array programs. In: Proc. of ATVA. pp. 18–23 (2014)
2. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis
for combined theories. In: Proc. of VMCAI. pp. 378–394 (2007)
3. Chakraborty,
S.,
Gupta,
A.,
Unadkat,
D.:
Verifying
array
manipulating
programs
with
full-program
induction,
https://www.cse.iitb.ac.in/ ∼ supratik/publications/papers/FPI longversion.html
4. Chakraborty, S., Gupta, A., Unadkat, D.: Verifying Array Manipulating Programs
by Tiling. In: Proc. of SAS. pp. 428–449 (2017)
5. Chakraborty, S., Gupta, A., Unadkat, D.: Verifying Array Manipulating Programs with Full-program Induction - Artifacts TACAS 2020. Figshare (2020).
https://doi.org/10.6084/m9.figshare.11875428.v1
6. Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. FMSD 19(1), 7–34 (2001)
7. Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully
automatic and scalable array content analysis. In: Proc. of POPL. pp. 105–118
(2011)
8. Darke, P., Prabhu, S., Chimdyalwar, B., Chauhan, A., Kumar, S., Basakchowdhury, A., Venkatesh, R., Datar, A., Medicherla, R.K.: VeriAbs: Verification by
abstraction and test generation. In: TACAS (Competition Contribution). pp. 457–
462 (2018)
9. Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S.,
Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1-3), 35–45 (2007)
10. Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via
syntax-guided-synthesis. In: Proc. of CAV. pp. 259–277 (2019)
11. Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and
its use in optimization. TOPLAS 9(3), 319–349 (1987)
12. Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In:
Proc. of FME. pp. 500–517 (2001)
13. Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array
operations. In: Proc. of POPL. pp. 338–350 (2005)
14. Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified
logical domains. In: Proc. of POPL. pp. 235–246 (2008)
15. Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Proc. of ATVA.
pp. 248–266 (2018)
16. Halbwachs, N., P´ eron, M.: Discovering properties about arrays in simple programs.
In: Proc. of PLDI. pp. 339–348 (2008)
17. Henzinger, T.A., Hottelier, T., Kov´ acs, L., Rybalchenko, A.: Aligators for arrays
(tool paper). In: Proc. of LPAR. pp. 348–356 (2010)
18. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.:
VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Proc. of
NFM. pp. 41–55 (2011)