Show simple item record

dc.contributor.authorAlhawi, Omar M.; email: omar.alhawi@manchester.ac.uk
dc.contributor.authorRocha, Herbert
dc.contributor.authorGadelha, Mikhail R.
dc.contributor.authorCordeiro, Lucas C.
dc.contributor.authorBatista, Eddie
dc.date.accessioned2021-06-17T15:50:28Z
dc.date.available2021-06-17T15:50:28Z
dc.date.issued2020-05-18
dc.identifierhttps://chesterrep.openrepository.com/bitstream/handle/10034/624972/10009_2020_Article_564.pdf?sequence=2
dc.identifierhttps://chesterrep.openrepository.com/bitstream/handle/10034/624972/10009_2020_Article_564_nlm.xml?sequence=3
dc.identifier.citationInternational Journal on Software Tools for Technology Transfer, volume 23, issue 2, page 115-135
dc.identifier.urihttp://hdl.handle.net/10034/624972
dc.descriptionFrom Springer Nature via Jisc Publications Router
dc.descriptionHistory: registration 2020-04-23, online 2020-05-18, pub-electronic 2020-05-18, pub-print 2021-04
dc.descriptionPublication status: Published
dc.descriptionFunder: University of Manchester
dc.description.abstractAbstract: 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.
dc.languageen
dc.publisherSpringer Berlin Heidelberg
dc.rightsLicence for this article: http://creativecommons.org/licenses/by/4.0/
dc.sourcepissn: 1433-2779
dc.sourceeissn: 1433-2787
dc.subjectGeneral
dc.subjectSoftware engineering
dc.subjectFormal methods
dc.subjectBounded model checking
dc.subjectk-Induction
dc.subjectInvariant inference
dc.titleVerification and refutation of C programs based on k -induction and invariant inference
dc.typearticle
dc.date.updated2021-06-17T15:50:28Z


Files in this item

Thumbnail
Name:
10009_2020_Article_564.pdf
Size:
1.100Mb
Format:
PDF
Thumbnail
Name:
10009_2020_Article_564_nlm.xml
Size:
219.8Kb
Format:
XML

This item appears in the following Collection(s)

Show simple item record