How verified is my code? Falsification-driven verification

Alex Groce, Iftekhar Ahmed, Carlos Jensen, Paul E. McKenney

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

11 Scopus citations

Abstract

Formal verification has advanced to the point that developers can verify the correctness of small, critical modules. Unfortunately, despite considerable efforts, determining if a "verification" verifies what the author intends is still difficult. Previous approaches are difficult to understand and often limited in applicability. Developers need verification coverage in terms of the software they are verifying, not model checking diagnostics. We propose a methodology to allow developers to determine (and correct) what it is that they have verified, and tools to support that methodology. Our basic approach is based on a novel variation of mutation analysis and the idea of verification driven by falsification. We use the CBMC model checker to show that this approach is applicable not only to simple data structures and sorting routines, and verification of a routine in Mozilla's JavaScript engine, but to understanding an ongoing effort to verify the Linux kernel Read-Copy-Update (RCU) mechanism.

Original languageEnglish (US)
Title of host publicationProceedings - 2015 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages737-748
Number of pages12
ISBN (Electronic)9781509000241
DOIs
StatePublished - Jan 4 2016
Externally publishedYes
Event30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015 - Lincoln, United States
Duration: Nov 9 2015Nov 13 2015

Publication series

NameProceedings - 2015 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015

Conference

Conference30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015
Country/TerritoryUnited States
CityLincoln
Period11/9/1511/13/15

Keywords

  • Falsification
  • Model checking
  • Mutation
  • Oracles
  • Test harnesses
  • Verification

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'How verified is my code? Falsification-driven verification'. Together they form a unique fingerprint.

Cite this