Verification and refutation of C programs based on k -induction and invariant inference
- PDF / 1,274,452 Bytes
- 21 Pages / 595.276 x 790.866 pts Page_size
- 101 Downloads / 148 Views
STTT Regular Paper
Verification and refutation of C programs based on k-induction and invariant inference Omar M. Alhawi1 · Herbert Rocha2 · Mikhail R. Gadelha3 · Lucas C. Cordeiro1 · Eddie Batista4
© The Author(s) 2020
Abstract DepthK is a source-to-source transformation tool that employs bounded model checking (BMC) to verify and falsify safety properties in single- and multi-threaded C programs, without manual annotation of loop invariants. Here, we describe and evaluate a proof-by-induction algorithm that combines k-induction with invariant inference to prove and refute safety properties. We apply two invariant generators to produce program invariants and feed these into a k-induction-based verification algorithm implemented in DepthK, which uses the efficient SMT-based context-bounded model checker (ESBMC) as sequential verification back-end. A set of C benchmarks from the International Competition on Software Verification (SV-COMP) and embedded-system applications extracted from the available literature are used to evaluate the effectiveness of the proposed approach. Experimental results show that k-induction with invariants can handle a wide variety of safety properties, in typical programs with loops and embedded software applications from the telecommunications, control systems, and medical domains. The results of our comparative evaluation extend the knowledge about approaches that rely on both BMC and kinduction for software verification, in the following ways. (1) The proposed method outperforms the existing implementations that use k-induction with an interval-invariant generator (e.g., 2LS and ESBMC), in the category ConcurrencySafety, and overcame, in others categories, such as SoftwareSystems, other software verifiers that use plain BMC (e.g., CBMC). Also, (2) it is more precise than other verifiers based on the property-directed reachability (PDR) algorithm (i.e., SeaHorn, Vvt and CPAchecker-CTIGAR). This way, our methodology demonstrated improvement over existing BMC and k-induction-based approaches. Keywords Software engineering · Formal methods · Bounded model checking · k-Induction · Invariant inference
1 Introduction Computer-based systems have been applied to different domains (e.g., industrial, military, education, and wearable), which generally demand high-quality software, in order to meet a target system’s requirements. In particular, (critical) embedded systems, such as those in the avionics and medical domains, impose several restrictions (e.g., response time and data accuracy) that must be met and measured, according to users’ requirements; otherwise, failures may lead to
B
Omar M. Alhawi [email protected]
1
University of Manchester, Manchester, UK
2
Federal University of Roraima, Boa Vista, Brazil
3
SIDIA Instituto de Ciência e Tecnologia, Manaus, Brazil
4
TP Vision, Manaus, Brazil
catastrophic situations. As a result, software testing and verification techniques are essential ingredients for developing systems with high dependability and reliability requirem
Data Loading...
