Scaling bounded model checking by transforming programs with arrays

DOI10.1007/978-3-319-63139-4_16MaRDI QIDQ2409744zbMATH OpenOpenAlexFDO

Authors Anushri Jana, Uday P. Khedker, Advaita Datar, R. Venkatesh, Niyas C.

Publication date 13 October 2017

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

zbMATH Keywords

arraybounded model checkingprogram transformationverification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Bounded Model Checking is one the most successful techniques for finding bugs in program. However, model checkers are resource hungry and are often unable to verify programs with loops iterating over large arrays.We present a transformation that enables bounded model checkers to verify a certain class of array properties. Our technique transforms an array-manipulating (ANSI-C) program to an array-free and loop-free (ANSI-C) program thereby reducing the resource requirements of a model checker significantly. Model checking of the transformed program using an off-the-shelf bounded model checker simulates the loop iterations efficiently. Thus, our transformed program is a sound abstraction of the original program and is also precise in a large number of cases - we formally characterize the class of programs for which it is guaranteed to be precise. We demonstrate the applicability and usefulness of our technique on both industry code as well as academic benchmarks.

Recommendations

• Verifying Array Programs by Transforming Verification Conditions
• Towards SMT Model Checking of Array-Based Systems
• Communicating Sequential Processes. The First 25 Years
• Scaling up model-checking. A case-study
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• A compact linear translation for bounded model checking
• Bounded model checking with parametric data structures
• Artificial Intelligence and Symbolic Computation
• Computer Aided Verification

Cited in

(9)

• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• Verification by gambling on program slices
• Property checking array programs using loop shrinking
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• Verifying Array Programs by Transforming Verification Conditions
• scientific article; zbMATH DE number 6687732 (Why is no real title available?)
• Proving safety with trace automata and bounded model checking
• Communicating Sequential Processes. The First 25 Years
• Putting the squeeze on array programs: loop verification via inductive rank reduction

This page was built for publication: Scaling bounded model checking by transforming programs with arrays

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