Verige: Verification with invariant generation engine

Nicolas Latorre, Francesco Alberti, Natasha Sharygina

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Program verification systems fail in verifying programs if appropriate loop invariants are not suggested. Generation of loop invariants in general is an art and providing them manually is a highly complex task (if possible at all). In this paper we present verige, a tool that integrates a verifier with an invariant generator engine. verige implements a novel generic algorithm that can alleviate the load on the invariant generator and consequently achieve a general speed-up of program verification.

Original languageEnglish
Title of host publication2014 International SPIN Symposium on Model Checking of Software, SPIN 2014 - Proceedings
PublisherAssociation for Computing Machinery, Inc
Pages121-124
Number of pages4
ISBN (Print)9781450324526
DOIs
Publication statusPublished - Jul 21 2014
Event21st International Symposium on Model Checking of Software, SPIN 2014 - San Jose, United States
Duration: Jul 21 2014Jul 23 2014

Other

Other21st International Symposium on Model Checking of Software, SPIN 2014
CountryUnited States
CitySan Jose
Period7/21/147/23/14

    Fingerprint

Keywords

  • Arrays
  • Quantified invariants
  • Software model checking

ASJC Scopus subject areas

  • Artificial Intelligence
  • Computer Science Applications
  • Software

Cite this

Latorre, N., Alberti, F., & Sharygina, N. (2014). Verige: Verification with invariant generation engine. In 2014 International SPIN Symposium on Model Checking of Software, SPIN 2014 - Proceedings (pp. 121-124). Association for Computing Machinery, Inc. https://doi.org/10.1145/2632362.2632373