Incremental bounded model checking for embedded software

DOI10.1007/S00165-017-0419-1MaRDI QIDQ1682291zbMATH OpenOpenAlexWikidataFDO

Authors Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmüller

Publication date 29 November 2017

Published in Formal Aspects of Computing (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1409.5872

zbMATH Keywords

embedded systemsbounded model checking\(k\)-inductionincremental SAT solving

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Program analysis is on the brink of mainstream in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and automated test case generation are some of the most common applications of automated verification tools based on Bounded Model Checking. Existing industrial tools for embedded software use an off-the-shelf Bounded Model Checker and apply it iteratively to verify the program with an increasing number of unwindings. This approach unnecessarily wastes time repeating work that has already been done and fails to exploit the power of incremental SAT solving. This paper reports on the extension of the software model checker CBMC to support incremental Bounded Model Checking and its successful integration with the industrial embedded software verification tool BTC EmbeddedTester. We present an extensive evaluation over large industrial embedded programs, which shows that incremental Bounded Model Checking cuts runtimes by one order of magnitude in comparison to the standard non-incremental approach, enabling the application of formal verification to large and complex embedded software.

Recommendations

• Efficient SAT-based bounded model checking for software verification
• An incremental algorithm to check satisfiability for bounded model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1979554
• Computer Aided Verification
• Computer Aided Verification
• Improving saturation-based bounded model checking

Cites work

• scientific article; zbMATH DE number 5613976 (Why is no real title available?)
• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 526071 (Why is no real title available?)
• scientific article; zbMATH DE number 1953038 (Why is no real title available?)
• scientific article; zbMATH DE number 1852147 (Why is no real title available?)
• An incremental algorithm to check satisfiability for bounded model checking
• Bounded model checking using satisfiability solving
• Deciding Bit-Vector Arithmetic with Abstraction
• Linear completeness thresholds for bounded model checking
• Query-Driven Program Testing
• Random time evolution and direct integrals: Constants of the motion and the mass operator
• Reduced functional consistency of uninterpreted functions
• Solving the incremental satisfiability problem
• Temporal induction by incremental SAT solving
• Theory and Applications of Satisfiability Testing
• Tools and Algorithms for the Construction and Analysis of Systems
• Under-approximating loops in C programs for fast counterexample detection

Cited in

(4)

• Incremental design-space model checking via reusable reachable state approximations
• eVolCheck: incremental upgrade checker for C
• A compositional behavioral modeling framework for embedded system design and conformance checking
• From bounded checking to verification of equivalence via symbolic up-to techniques

Describes a project that uses

Uses Software

• NModel
• CBMC
• StarExec
• SystemC
• PicoSAT
• KLEE
• SATIRE
• MiniSat
• Boolector

This page was built for publication: Incremental bounded model checking for embedded software

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1682291)