Scalable and scope-bounded software verification in Varvel

Franjo Ivančić, Gogul Balakrishnan, Aarti Gupta, Sriram Sankaranarayanan, Naoto Maeda, Takashi Imoto, Rakesh Pothengil, Mustafa Hussain

Research output: Contribution to journalArticle

8 Scopus citations

Abstract

Software model checking and static analysis have matured over the last decade, enabling their use in automated software verification. However, lack of scalability makes these tools hard to apply in industry practice. Furthermore, approximations in the models of program and environment lead to a profusion of false alarms. This paper proposes DC2, a verification framework using scope-bounding to address the issue of scalability, while retaining enough precision to avoid false alarms in practice. DC2 splits the analysis problem into manageable parts, relying on a combination of three automated techniques: (a) techniques to infer useful specifications for functions in the form of pre- and post-conditions; (b) stub inference techniques that infer abstractions to replace function calls beyond the verification scope; and (c) automatic refinement of pre- and post-conditions using counterexamples that are deemed to be false alarms by a user. The techniques enable DC2 to perform iterative reasoning over the calling environment of functions, to find non-trivial bugs and fewer false alarms. Based on the DC2 framework, we have developed a software model checking tool for C/C++ programs called Varvel, which has been in industrial use at NEC for a number of years. In addition to DC2, we describe other scalability and usability improvements in Varvel that have enabled its successful application on numerous large software projects. These include model simplifications, support for witness understanding to improve debugging assistance, and handling of C++ programs. We present experimental evaluations that demonstrate the effectiveness of DC2 and report on the usage of Varvel in NEC.

Original languageEnglish (US)
Pages (from-to)517-559
Number of pages43
JournalAutomated Software Engineering
Volume22
Issue number4
DOIs
StatePublished - Dec 26 2015
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Abstract interpretation
  • Bug detection
  • Program analysis
  • Scope bounding
  • Software model checking
  • Witness presentation

Fingerprint Dive into the research topics of 'Scalable and scope-bounded software verification in Varvel'. Together they form a unique fingerprint.

  • Cite this

    Ivančić, F., Balakrishnan, G., Gupta, A., Sankaranarayanan, S., Maeda, N., Imoto, T., Pothengil, R., & Hussain, M. (2015). Scalable and scope-bounded software verification in Varvel. Automated Software Engineering, 22(4), 517-559. https://doi.org/10.1007/s10515-014-0164-0