Loading...
Verification and refutation of C programs based on k -induction and invariant inference
Alhawi, Omar M.; email: omar.alhawi@manchester.ac.uk Rocha, Herbert Gadelha, Mikhail R. Cordeiro, Lucas C. Batista, Eddie
Alhawi, Omar M.; email: omar.alhawi@manchester.ac.uk
Rocha, Herbert
Gadelha, Mikhail R.
Cordeiro, Lucas C.
Batista, Eddie
Advisors
Editors
Other Contributors
Affiliation
EPub Date
Publication Date
2020-05-18
Submitted Date
Collections
Other Titles
Abstract
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 k-induction 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.
Citation
International Journal on Software Tools for Technology Transfer, volume 23, issue 2, page 115-135
Publisher
Springer Berlin Heidelberg
Journal
Research Unit
DOI
PubMed ID
PubMed Central ID
Type
article
Language
Description
From Springer Nature via Jisc Publications Router
History: registration 2020-04-23, online 2020-05-18, pub-electronic 2020-05-18, pub-print 2021-04
Publication status: Published
Funder: University of Manchester
History: registration 2020-04-23, online 2020-05-18, pub-electronic 2020-05-18, pub-print 2021-04
Publication status: Published
Funder: University of Manchester