Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 5/2022

29-09-2022 | General

Full-program induction: verifying array programs sans loop invariants

Authors: Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat

Published in: International Journal on Software Tools for Technology Transfer | Issue 5/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Arrays are commonly used in a variety of software to store and process data in loops. Automatically proving safety properties of such programs that manipulate arrays is challenging. We present a novel verification technique, called full-program induction, for proving (a sub-class of) quantified as well as quantifier-free properties of programs manipulating arrays of parametric size N. Instead of inducting over individual loops, our technique inducts over the entire program (possibly containing multiple loops) directly via the program parameter N. The technique performs non-trivial transformations of the given program and pre-conditions during the inductive step. The transformations assist in effectively reducing the assertion checking problem by transforming a program with multiple loops to a program which has fewer and simpler loops or is loop free. Significantly, full-program induction does not require generation or use of loop-specific invariants. To assess the efficacy of our technique, we have developed a prototype tool called Vajra. We demonstrate the performance of Vajra vis-a-vis several state-of-the-art tools on a large set of array manipulating benchmarks from the international software verification competition (SV-COMP) and on several programs inspired by algebraic functions that perform polynomial computations.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
By indirect dependence, we mean the dependence via another value computed in a peeled or non-peeled statements in the program.
 
Literature
1.
go back to reference Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Proceedings of FMCAD, pp. 127–144 (2000) Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Proceedings of FMCAD, pp. 127–144 (2000)
2.
go back to reference Komuravelli, A., Bjorner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: Proceedings of FMCAD, pp. 89–96 (2015) Komuravelli, A., Bjorner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: Proceedings of FMCAD, pp. 89–96 (2015)
3.
go back to reference Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Proceedings of ATVA, pp. 248–266 (2018) Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Proceedings of ATVA, pp. 248–266 (2018)
4.
go back to reference Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided-synthesis. In: Proceedings of CAV, pp. 259–277 (2019) Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided-synthesis. In: Proceedings of CAV, pp. 259–277 (2019)
5.
go back to reference Rajkhowa, P., Lin, F.: Extending VIAP to handle array programs. In: Proceedings of VSTTE, pp. 38–49 (2018) Rajkhowa, P., Lin, F.: Extending VIAP to handle array programs. In: Proceedings of VSTTE, pp. 38–49 (2018)
6.
go back to reference Henzinger, T.A., Hottelier, T., Kovács, L., Rybalchenko, A.: Aligators for arrays (tool paper). In: Proceedings of LPAR, pp. 348–356 (2010) Henzinger, T.A., Hottelier, T., Kovács, L., Rybalchenko, A.: Aligators for arrays (tool paper). In: Proceedings of LPAR, pp. 348–356 (2010)
7.
go back to reference Afzal, M., Chakraborty, S., Chauhan, A., Chimdyalwar, B., Darke, P., Gupta, A., Kumar, S., Babu M, C., Unadkat, D., Venkatesh, R.: Veriabs: verification by abstraction and test generation (competition contribution). In: Proceedings of TACAS, pp. 383–387 (2020) Afzal, M., Chakraborty, S., Chauhan, A., Chimdyalwar, B., Darke, P., Gupta, A., Kumar, S., Babu M, C., Unadkat, D., Venkatesh, R.: Veriabs: verification by abstraction and test generation (competition contribution). In: Proceedings of TACAS, pp. 383–387 (2020)
8.
go back to reference Chakraborty, S., Gupta, A., Unadkat, D.: Verifying Array Manipulating Programs by Tiling. In: Proceedings of SAS, pp. 428–449 (2017) Chakraborty, S., Gupta, A., Unadkat, D.: Verifying Array Manipulating Programs by Tiling. In: Proceedings of SAS, pp. 428–449 (2017)
9.
go back to reference Monniaux, D., Gonnord, L.: Cell morphing: from array programs to array-free horn clauses. In: Proceedings of SAS, pp. 361–382 (2016) Monniaux, D., Gonnord, L.: Cell morphing: from array programs to array-free horn clauses. In: Proceedings of SAS, pp. 361–382 (2016)
10.
go back to reference Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an acceleration-based verification framework for array programs. In: Proceedings of ATVA, pp. 18–23 (2014) Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an acceleration-based verification framework for array programs. In: Proceedings of ATVA, pp. 18–23 (2014)
11.
go back to reference Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. FMSD 19(1), 7–34 (2001)MATH Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. FMSD 19(1), 7–34 (2001)MATH
12.
go back to reference de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of TACAS, pp. 337–340 (2008) de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of TACAS, pp. 337–340 (2008)
13.
go back to reference Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: Proceedings of POPL, pp. 338–350 (2005) Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: Proceedings of POPL, pp. 338–350 (2005)
14.
go back to reference Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: Proceedings of PLDI, pp. 339–348 (2008) Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: Proceedings of PLDI, pp. 339–348 (2008)
15.
go back to reference Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In: Proceedings of VMCAI, pp. 282–299 (2015) Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In: Proceedings of VMCAI, pp. 282–299 (2015)
16.
go back to reference Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of POPL, pp. 105–118 (2011) Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of POPL, pp. 105–118 (2011)
17.
go back to reference Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Proceedings of POPL, pp. 235–246 (2008) Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Proceedings of POPL, pp. 235–246 (2008)
18.
go back to reference Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. ACM Sigplan Notices 44(6), 223–234 (2009)CrossRef Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. ACM Sigplan Notices 44(6), 223–234 (2009)CrossRef
19.
go back to reference Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Proceedings of VMCAI, pp. 378–394 (2007) Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Proceedings of VMCAI, pp. 378–394 (2007)
20.
go back to reference Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Proceedings of CAV, pp. 193–206 (2007) Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Proceedings of CAV, pp. 193–206 (2007)
21.
go back to reference Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Proceedings of FME, pp. 500–517 (2001) Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Proceedings of FME, pp. 500–517 (2001)
22.
go back to reference 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)MathSciNetCrossRefMATH 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)MathSciNetCrossRefMATH
23.
go back to reference Lattner, C., Adve, V.: Llvm: a compilation framework for lifelong program analysis and transformation. In: Proceedings of CGO, pp. 75–86 (2004) Lattner, C., Adve, V.: Llvm: a compilation framework for lifelong program analysis and transformation. In: Proceedings of CGO, pp. 75–86 (2004)
24.
go back to reference Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs with full-program induction. In: Proceedings of TACAS, pp. 22–39 (2020) Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs with full-program induction. In: Proceedings of TACAS, pp. 22–39 (2020)
25.
go back to reference Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Proceedings of POPL, pp. 12–27 (1988) Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Proceedings of POPL, pp. 12–27 (1988)
26.
go back to reference Knobe, K., Sarkar, V.: Array SSA form and its use in parallelization. In: Proceedings of POPL, pp. 107–120 (1998) Knobe, K., Sarkar, V.: Array SSA form and its use in parallelization. In: Proceedings of POPL, pp. 107–120 (1998)
27.
go back to reference Unadkat, D.P.: Techniques for Precise and Scalable Verification of Array Programs. Ph.D. Thesis, Indian Institute of Technology Bombay (2022) Unadkat, D.P.: Techniques for Precise and Scalable Verification of Array Programs. Ph.D. Thesis, Indian Institute of Technology Bombay (2022)
28.
go back to reference Towle, R.A.: Control and Data Dependence for Program Transformations. Ph.D. Dissertation, University of Illinois at Urbana-Champaign, USA (1976) Towle, R.A.: Control and Data Dependence for Program Transformations. Ph.D. Dissertation, University of Illinois at Urbana-Champaign, USA (1976)
29.
go back to reference Kuck, D.L.: Structure of Computers and Computations. Wiley, Hoboken (1978) Kuck, D.L.: Structure of Computers and Computations. Wiley, Hoboken (1978)
30.
go back to reference Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. TOPLAS 9(3), 319–349 (1987)CrossRefMATH Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. TOPLAS 9(3), 319–349 (1987)CrossRefMATH
31.
go back to reference Horwitz, S., Reps, T.: The use of program dependence graphs in software engineering. In: ICSE, pp. 392–411 (1992) Horwitz, S., Reps, T.: The use of program dependence graphs in software engineering. In: ICSE, pp. 392–411 (1992)
32.
go back to reference Kennedy, K., Allen, J.R.: Optimizing Compilers for Modern Architectures: A Dependence-Based Approach (2001) Kennedy, K., Allen, J.R.: Optimizing Compilers for Modern Architectures: A Dependence-Based Approach (2001)
33.
go back to reference Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions. In: Workshop on Advances in Verification, pp. 1–8 (2000) Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions. In: Workshop on Advances in Verification, pp. 1–8 (2000)
34.
go back to reference Colón, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Proceedings of TACAS, pp. 67–81 (2001) Colón, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Proceedings of TACAS, pp. 67–81 (2001)
35.
go back to reference Colón, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Proceedings of CAV, pp. 442–454 (2002) Colón, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Proceedings of CAV, pp. 442–454 (2002)
36.
go back to reference Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Proceedings of VMCAI, pp. 239–251 (2004) Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Proceedings of VMCAI, pp. 239–251 (2004)
38.
go back to reference Lescanne, P.: Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems. RAIRO. Informatique théorique 16(4), 331–347 (1982)MathSciNetCrossRefMATH Lescanne, P.: Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems. RAIRO. Informatique théorique 16(4), 331–347 (1982)MathSciNetCrossRefMATH
39.
go back to reference Chakraborty, S., Gupta, A., Unadkat, D.: Diffy: inductive reasoning of array programs using difference invariants. In: Proceedings of CAV, pp. 911–935 (2021) Chakraborty, S., Gupta, A., Unadkat, D.: Diffy: inductive reasoning of array programs using difference invariants. In: Proceedings of CAV, pp. 911–935 (2021)
41.
go back to reference Georgiou, P., Gleiss, B., Kovács, L.: Trace logic for inductive loop reasoning. In: Proceedings of FMCAD, pp. 255–263 (2020) Georgiou, P., Gleiss, B., Kovács, L.: Trace logic for inductive loop reasoning. In: Proceedings of FMCAD, pp. 255–263 (2020)
42.
go back to reference Bozga, M., Iosif, R., Konecný, F.: Fast acceleration of ultimately periodic relations. In: Proceedings of CAV, pp. 227–242 (2010) Bozga, M., Iosif, R., Konecný, F.: Fast acceleration of ultimately periodic relations. In: Proceedings of CAV, pp. 227–242 (2010)
43.
go back to reference Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: Proceedings of POPL, pp. 529–540 (2014) Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: Proceedings of POPL, pp. 529–540 (2014)
44.
go back to reference Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Proceedings of LPAR, pp. 46–61 (2012) Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Proceedings of LPAR, pp. 46–61 (2012)
45.
go back to reference Monniaux, D., Alberti, F.: A simple abstraction of arrays and maps by program translation. In: Proceedings of SAS, pp. 217–234 (2015) Monniaux, D., Alberti, F.: A simple abstraction of arrays and maps by program translation. In: Proceedings of SAS, pp. 217–234 (2015)
46.
47.
go back to reference Déharbe, D., Moreira, A.M.: Using induction and BDDs to model check invariants. In: Advances in Hardware Design and Verification, pp. 203–213 (1997) Déharbe, D., Moreira, A.M.: Using induction and BDDs to model check invariants. In: Advances in Hardware Design and Verification, pp. 203–213 (1997)
48.
go back to reference Bjesse, P., Claessen, K.: Sat-based verification without state space traversal. In: FMCAD, pp. 409–426 (2000) Bjesse, P., Claessen, K.: Sat-based verification without state space traversal. In: FMCAD, pp. 409–426 (2000)
49.
go back to reference Eén, N., Sörensson, N.: Temporal induction by incremental sat solving. Electron. Notes Theor. Comput. Sci. 89(4), 543–560 (2003)CrossRefMATH Eén, N., Sörensson, N.: Temporal induction by incremental sat solving. Electron. Notes Theor. Comput. Sci. 89(4), 543–560 (2003)CrossRefMATH
50.
go back to reference Große, D., Le, H.M., Drechsler, R.: Induction-based formal verification of SystemC TLM designs. In: Workshop on Microprocessor Test and Verification, pp. 101–106 (2009) Große, D., Le, H.M., Drechsler, R.: Induction-based formal verification of SystemC TLM designs. In: Workshop on Microprocessor Test and Verification, pp. 101–106 (2009)
51.
go back to reference Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: CADE, pp. 392–406 (2013) Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: CADE, pp. 392–406 (2013)
52.
go back to reference Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: VMCAI, pp. 80–98 (2015) Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: VMCAI, pp. 80–98 (2015)
53.
go back to reference Unno, H., Torii, S., Sakamoto, H.: Automating induction for solving horn clauses. In: CAV, pp. 571–591 (2017) Unno, H., Torii, S., Sakamoto, H.: Automating induction for solving horn clauses. In: CAV, pp. 571–591 (2017)
54.
go back to reference De Moura, L., Rueß, H., Sorea, M.: Bounded model checking and induction: from refutation to verification. In: CAV, pp. 14–26 (2003) De Moura, L., Rueß, H., Sorea, M.: Bounded model checking and induction: from refutation to verification. In: CAV, pp. 14–26 (2003)
55.
go back to reference Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: FMCAD, pp. 1–9 (2008) Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: FMCAD, pp. 1–9 (2008)
56.
go back to reference Donaldson, A.F., Kroening, D., Rümmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Proceedings of TACAS, pp. 280–295 (2010) Donaldson, A.F., Kroening, D., Rümmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Proceedings of TACAS, pp. 280–295 (2010)
57.
go back to reference Kahsai, T., Tinelli, C.: Pkind: A parallel k-induction based model checker. In: PDMC, pp. 55–62 (2011) Kahsai, T., Tinelli, C.: Pkind: A parallel k-induction based model checker. In: PDMC, pp. 55–62 (2011)
58.
go back to reference Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software verification using k-induction. In: Proceedings of SAS, pp. 351–368 (2011) Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software verification using k-induction. In: Proceedings of SAS, pp. 351–368 (2011)
59.
go back to reference Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proceedings of CAV, pp. 622–640 (2015) Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proceedings of CAV, pp. 622–640 (2015)
60.
go back to reference Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Proceedings of SAS, pp. 145–161 (2015) Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Proceedings of SAS, pp. 145–161 (2015)
61.
go back to reference Gadelha, M.Y., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of c programs via k-induction. STTT 19(1), 97–114 (2017)CrossRef Gadelha, M.Y., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of c programs via k-induction. STTT 19(1), 97–114 (2017)CrossRef
62.
go back to reference Krishnan, H.G.V., Vizel, Y., Ganesh, V., Gurfinkel, A.: Interpolating strong induction. In: International Conference on Computer Aided Verification, pp. 367–385 (2019) Krishnan, H.G.V., Vizel, Y., Ganesh, V., Gurfinkel, A.: Interpolating strong induction. In: International Conference on Computer Aided Verification, pp. 367–385 (2019)
63.
go back to reference Alhawi, O.M., Rocha, H., Gadelha, M.R., Cordeiro, L.C., Batista, E.: Verification and refutation of c programs based on k-induction and invariant inference. STTT 23(2), 115–135 (2021)CrossRef Alhawi, O.M., Rocha, H., Gadelha, M.R., Cordeiro, L.C., Batista, E.: Verification and refutation of c programs based on k-induction and invariant inference. STTT 23(2), 115–135 (2021)CrossRef
64.
go back to reference Yu, E., Biere, A., Heljanko, K.: Progress in certifying hardware model checking results. In: Proceedings of CAV, pp. 363–386 (2021) Yu, E., Biere, A., Heljanko, K.: Progress in certifying hardware model checking results. In: Proceedings of CAV, pp. 363–386 (2021)
65.
go back to reference Seghir, M.N., Brain, M.: Simplifying the verification of quantified array assertions via code transformation. In: Proceedings of LOPSTR, pp. 194–212 (2012) Seghir, M.N., Brain, M.: Simplifying the verification of quantified array assertions via code transformation. In: Proceedings of LOPSTR, pp. 194–212 (2012)
66.
go back to reference Ish-Shalom, O., Itzhaky, S., Rinetzky, N., Shoham, S.: Putting the squeeze on array programs: Loop verification via inductive rank reduction. In: Proceedings of VMCAI, pp. 112–135 (2020) Ish-Shalom, O., Itzhaky, S., Rinetzky, N., Shoham, S.: Putting the squeeze on array programs: Loop verification via inductive rank reduction. In: Proceedings of VMCAI, pp. 112–135 (2020)
68.
go back to reference Mann, M., Irfan, A., Griggio, A., Padon, O., Barrett, C.: Counterexample-guided prophecy for model checking modulo the theory of arrays. In: Proceedings of TACAS (2021) Mann, M., Irfan, A., Griggio, A., Padon, O., Barrett, C.: Counterexample-guided prophecy for model checking modulo the theory of arrays. In: Proceedings of TACAS (2021)
69.
go back to reference Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. weak updates. In: Proceedings of ESOP, pp. 246–266 (2010) Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. weak updates. In: Proceedings of ESOP, pp. 246–266 (2010)
70.
go back to reference Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Proceedings of NFM, pp. 41–55 (2011) Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Proceedings of NFM, pp. 41–55 (2011)
71.
go back to reference Paige, R., Koenig, S.: Finite differencing of computable expressions. TOPLAS 4(3), 402–454 (1982)CrossRefMATH Paige, R., Koenig, S.: Finite differencing of computable expressions. TOPLAS 4(3), 402–454 (1982)CrossRefMATH
72.
go back to reference Horwitz, S., Prins, J., Reps, T.: Integrating noninterfering versions of programs. TOPLAS 11(3), 345–387 (1989)CrossRef Horwitz, S., Prins, J., Reps, T.: Integrating noninterfering versions of programs. TOPLAS 11(3), 345–387 (1989)CrossRef
73.
go back to reference Lahiri, S.K., Vaswani, K., Hoare, C.A.: Differential static analysis: opportunities, applications, and challenges. In: Workshop on Future of Software Engineering Research, pp. 201–204 (2010) Lahiri, S.K., Vaswani, K., Hoare, C.A.: Differential static analysis: opportunities, applications, and challenges. In: Workshop on Future of Software Engineering Research, pp. 201–204 (2010)
74.
go back to reference Liu, Y.A., Stoller, S.D., Teitelbaum, T.: Static caching for incremental computation. TOPLAS 20(3), 546–585 (1998)CrossRef Liu, Y.A., Stoller, S.D., Teitelbaum, T.: Static caching for incremental computation. TOPLAS 20(3), 546–585 (1998)CrossRef
75.
go back to reference Liu, Y.A., Stoller, S.D., Li, N., Rothamel, T.: Optimizing aggregate array computations in loops. TOPLAS 27(1), 91–125 (2005)CrossRef Liu, Y.A., Stoller, S.D., Li, N., Rothamel, T.: Optimizing aggregate array computations in loops. TOPLAS 27(1), 91–125 (2005)CrossRef
76.
go back to reference Binkley, D.W.: Using semantic differencing to reduce the cost of regression testing. In: Proceedings of ICSM, pp. 41–50 (1992) Binkley, D.W.: Using semantic differencing to reduce the cost of regression testing. In: Proceedings of ICSM, pp. 41–50 (1992)
77.
go back to reference Shankar, A., Bodik, R.: DITTO: automatic incrementalization of data structure invariant checks (in Java). ACM SIGPLAN Notices 42(6), 310–319 (2007) Shankar, A., Bodik, R.: DITTO: automatic incrementalization of data structure invariant checks (in Java). ACM SIGPLAN Notices 42(6), 310–319 (2007)
78.
go back to reference Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: Symdiff: a language-agnostic semantic diff tool for imperative programs. In: Proceedings of CAV, pp. 712–717 (2012) Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: Symdiff: a language-agnostic semantic diff tool for imperative programs. In: Proceedings of CAV, pp. 712–717 (2012)
Metadata
Title
Full-program induction: verifying array programs sans loop invariants
Authors
Supratik Chakraborty
Ashutosh Gupta
Divyesh Unadkat
Publication date
29-09-2022
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 5/2022
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00676-w

Other articles of this Issue 5/2022

International Journal on Software Tools for Technology Transfer 5/2022 Go to the issue

Premium Partner