Verige: Verification with invariant generation engine

Nicolas Latorre, Francesco Alberti, Natasha Sharygina

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


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
Number of pages4
ISBN (Print)9781450324526
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


Other21st International Symposium on Model Checking of Software, SPIN 2014
Country/TerritoryUnited States
CitySan Jose


  • Arrays
  • Quantified invariants
  • Software model checking

ASJC Scopus subject areas

  • Artificial Intelligence
  • Computer Science Applications
  • Software


Dive into the research topics of 'Verige: Verification with invariant generation engine'. Together they form a unique fingerprint.

Cite this