A lightweight technique for distributed and incremental program verification

Martin Brain, Florian Schanda

Research output: Chapter in Book/Report/Conference proceedingChapter

3 Citations (Scopus)

Abstract

Applying automated verification to industrial code bases creates a significant computational task even when the individual conditions to be checked are trivial. This affects the wall clock time taken to verify the program and has knock-on effects on how the tools are used and on project management. In this paper a simple and lightweight technique for adding incremental and distributed capabilities to a program verification system is given. Experiments with an implementation of the technique for the SPARK tool set show that it can yield an average 29 fold speed increase in incremental use and near optimal speedup in distributed use. Critically, this gives a qualitative change in how automated verification is used in a large commercial project.
Original languageEnglish
Title of host publicationVerified Software: Theories, Tools, Experiments
Place of PublicationHeidelberg
PublisherSpringer
Pages114-129
Number of pages16
Edition7152
DOIs
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer

Fingerprint

Dive into the research topics of 'A lightweight technique for distributed and incremental program verification'. Together they form a unique fingerprint.

Cite this