In large real life programs, loops and arrays are the main challenges to scaling up verification. Overcoming this challenge requires a portfolio of specialised techniques. Accordingly, we at TCS Research have developed a portfolio of loop and array abstraction techniques to scale up verification in practice. Naturally, a collection of such techniques can verify programs from a wider variety of classes than each individual technique. This collection of techniques in addition to well known verification techniques like bounded model checking form the portfolio used in the VeriAbs framework. In order to improve the likelihood that a suitable technique from the portfolio is applied to the input program, the techniques are often prioritized into a sequence, also called a verification strategy, to verify each input program. VeriAbs uses four such strategies, each defined manually using domain expertise and experimentation. One of the suitable strategies is selected for verification based on the class of the input program. This approach to program verification has shown success and won several gold medals in the Competition on Software Verification (sv-comp) 2019–23. In practice, defining verification strategies manually is time consuming and not extensible. Towards this, machine learning methods have been proposed recently to predict strategies automatically for each input program. It is a challenge to define useful program features that can describe a program well enough to the learner to predict a useful strategy from the given portfolio of techniques. We present a novel approach to alleviate this challenge as implemented in VeriAbsL, a tool that uses machine learning methods to predict strategies for an input program using VeriAbs’s portfolio. VeriAbsL was developed in 2023, and since then has won a silver and a gold medal at sv-comp 2023–24. To summarise, in this paper we present (1) a few proprietary loops and array abstraction techniques in VeriAbs’s portfolio, (2) the manually defined method of strategy selection as implemented in VeriAbs, (3) the machine learning method of strategy prediction as implemented in VeriAbsL, (4) a comparison of VeriAbs’s portfolio with another state-of-art portfolio-based verifier, and (5) a comparison of strategy selection implemented in VeriAbs with a novel strategy prediction implemented in VeriAbsL.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

The VeriAbs Tool Suite for Code Verification

  • Priyanka Darke,
  • Bharti Chimdyalwar,
  • R. Venkatesh,
  • Supratik Chakraborty

摘要

In large real life programs, loops and arrays are the main challenges to scaling up verification. Overcoming this challenge requires a portfolio of specialised techniques. Accordingly, we at TCS Research have developed a portfolio of loop and array abstraction techniques to scale up verification in practice. Naturally, a collection of such techniques can verify programs from a wider variety of classes than each individual technique. This collection of techniques in addition to well known verification techniques like bounded model checking form the portfolio used in the VeriAbs framework. In order to improve the likelihood that a suitable technique from the portfolio is applied to the input program, the techniques are often prioritized into a sequence, also called a verification strategy, to verify each input program. VeriAbs uses four such strategies, each defined manually using domain expertise and experimentation. One of the suitable strategies is selected for verification based on the class of the input program. This approach to program verification has shown success and won several gold medals in the Competition on Software Verification (sv-comp) 2019–23. In practice, defining verification strategies manually is time consuming and not extensible. Towards this, machine learning methods have been proposed recently to predict strategies automatically for each input program. It is a challenge to define useful program features that can describe a program well enough to the learner to predict a useful strategy from the given portfolio of techniques. We present a novel approach to alleviate this challenge as implemented in VeriAbsL, a tool that uses machine learning methods to predict strategies for an input program using VeriAbs’s portfolio. VeriAbsL was developed in 2023, and since then has won a silver and a gold medal at sv-comp 2023–24. To summarise, in this paper we present (1) a few proprietary loops and array abstraction techniques in VeriAbs’s portfolio, (2) the manually defined method of strategy selection as implemented in VeriAbs, (3) the machine learning method of strategy prediction as implemented in VeriAbsL, (4) a comparison of VeriAbs’s portfolio with another state-of-art portfolio-based verifier, and (5) a comparison of strategy selection implemented in VeriAbs with a novel strategy prediction implemented in VeriAbsL.