research-article

Over-approximating loops to prove properties using bounded model checking

Authors:

Ravindra MettaAuthors Info & Claims

DATE '15: Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition

Pages 1407 - 1412

Published: 09 March 2015 Publication History

Get Access

Abstract

Bounded Model Checkers (BMCs) are widely used to detect violations of program properties up to a bounded execution length of the program. However when it comes to proving the properties, BMCs are unable to provide a sound result for programs with loops of large or unknown bounds. To address this limitation, we developed a new loop over-approximation technique LA. LA replaces a given loop in a program with an abstract loop having a smaller known bound by combining the techniques of output abstraction and a novel abstract acceleration, suitably augmented with a new application of induction. The resulting transformed program can then be fed to any bounded model checker to provide a sound proof of the desired properties. We call this approach, of LA followed by BMC, as LABMC.

We evaluated the effectiveness of LABMC on some of the SV-COMP14 loop benchmarks, each with a property encoded into it. Well known BMCs failed to prove most of these properties due to loops of large, infinite or unknown bounds while LABMC obtained promising results. We also performed experiments on a real world automotive application on which the well known BMCs were able to prove only one of the 186 array accesses to be within array bounds. LABMC was able to successfully prove 131 of those array accesses to be within array bounds.

References

[1]

ESBMC 1.22. http://users.ecs.soton.ac.uk/lcc08r/esbmc/papers/TACAS13.pdf.

Google Scholar

[2]

LLBMC: Improved Bounded Model Checking of C Programs Using LLVM. http://llbmc.org/files/papers/TACAS13.pdf.

Google Scholar

[3]

SV-COMP 2014 Benchmark. http://sv-comp.sosy-lab.org/2014/benchmarks.php.

Google Scholar

[4]

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The software model checker blast. STTT, 9(5--6): 505--525, 2007.

Digital Library

Google Scholar

[5]

Edmund Clarke, Daniel Kroening, and Flavio Lerda. A Tool for Checking ANSI-C Programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), volume 2988 of Lecture Notes in Computer Science, pages 168--176. Springer, 2004.

Crossref

Google Scholar

[6]

Edmund Clarke, Daniel Kroening, Natasha Sharygina, and Karen Yorav. SATABS: SAT-based predicate abstraction for ANSI-C. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), volume 3440 of Lecture Notes in Computer Science, pages 570--574. Springer Verlag, 2005.

Digital Library

Google Scholar

[7]

P. Darke, M. Khanzode, A. Nair, U. Shrotri, and R. Venkatesh. Precise analysis of large industry code. In Asia Pacific Software Engineering Conferece, pages 306--309, 2012.

Digital Library

Google Scholar

[8]

Alastair F. Donaldson, Leopold Haller, Daniel Kroening, and Philipp Ruemmer. Software verification using k-induction. In Proceedings of the 18th International Static Analysis Symposium (SAS'11), volume 6887 of Lecture Notes in Computer Science, pages 351--368. Springer, 2011.

Digital Library

Google Scholar

[9]

Daniel Kroening, Matt Lewis, and Georg Weissenbacher. Under-approximating loops in C programs for fast counterexample detection. In Computer Aided Verification (CAV), volume 8044 of LNCS. Springer, 2013.

Digital Library

Google Scholar

[10]

Nicolas Halbwachs Laure Gonnord. Combining widening and acceleration in linear relation analysis. In Static Analysis, pages 144--160. Springer, 2006.

Digital Library

Google Scholar

[11]

Thibaud Hottelier Regis Blanc, Thomas Henzinger and Laura Kovacs. Abc: Algebraic bound computation for loops. In Lecture Notes in Computer Science Volume 6355, pages 103--118. Springer, 2010.

Digital Library

Google Scholar

[12]

Peter Schrammel and Bertrand Jeannet. Applying abstract acceleration to (co-)reachability analysis of reactive programs. J. Symb. Comput., pages 1512--1532, 2012.

Digital Library

Google Scholar

[13]

Milena Vujosevic-Janicic and Viktor Kuncak. Development and evaluation of lav: An smt-based error finding platform - system description. In VSTTE, pages 98--113, 2012.

Digital Library

Google Scholar

[14]

Björn Wachter, Daniel Kroening, and Joel Ouaknine. Verifying multi-threaded software with Impact. In Formal Methods in Computer-Aided Design (FMCAD), pages 210--217, 2013.

Crossref

Google Scholar

Cited By

View all

Chimdyalwar BDarke PChauhan AShah PKumar SVenkatesh R(2017)VeriAbsProceedings, Part II, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020610.1007/978-3-662-54580-5_32(404-408)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54580-5_32
Metta RBecker MBokil PChakraborty SVenkatesh R(2016)TIC: a scalable model checking based approach to WCET estimationACM SIGPLAN Notices10.1145/2980930.290796151:5(72-81)Online publication date: 13-Jun-2016
https://dl.acm.org/doi/10.1145/2980930.2907961
Metta RBecker MBokil PChakraborty SVenkatesh RKuo TWhalley D(2016)TIC: a scalable model checking based approach to WCET estimationProceedings of the 17th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools, and Theory for Embedded Systems10.1145/2907950.2907961(72-81)Online publication date: 13-Jun-2016
https://dl.acm.org/doi/10.1145/2907950.2907961
Show More Cited By

Index Terms

Over-approximating loops to prove properties using bounded model checking

Recommendations

Handling loops in bounded model checking of C programs via k-induction

The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative ...
Evaluation of SAT-based Bounded Model Checking of ACTL Properties
TASE '07: Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering

Bounded model checking (BMC) based on SAT has been introduced as a complementary method to BDDbased symbolic model checking of LTL and ACTL properties in recent years. For general LTL and ACTL properties, BMC has traditionally aimed mainly at error ...
Verification of ACTL properties by bounded model checking
EUROCAST'07: Proceedings of the 11th international conference on Computer aided systems theory

SAT-based bounded model checking has been introduced as a complementary technique to BDD-based symbolic model checking in recent years and a lot of successful work has been done with this approach. The success is mostly due to the efficiency of error-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DATE '15: Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition

March 2015

1827 pages

ISBN:9783981537048

General Chair:
Wolfgang Nebel
OFFIS & University of Oldenburg, DE
,
Program Chair:
David Atienza
EPFL, CH

Publisher

EDA Consortium

San Jose, CA, United States

Publication History

Published: 09 March 2015

Check for updates

Qualifiers

Research-article

Conference

DATE '15

Sponsor:

EDAA
EDAC
SIGDA
Russian Acadamy of Sciences

DATE '15: Design, Automation and Test in Europe

March 9 - 13, 2015

Grenoble, France

Acceptance Rates

DATE '15 Paper Acceptance Rate 206 of 915 submissions, 23%;

Overall Acceptance Rate 518 of 1,794 submissions, 29%

Upcoming Conference

DATE '25

Sponsor:
sigda

Design, Automation and Test in Europe

March 31 - April 2, 2025

Lyon , France

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
135
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Chimdyalwar BDarke PChauhan AShah PKumar SVenkatesh R(2017)VeriAbsProceedings, Part II, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020610.1007/978-3-662-54580-5_32(404-408)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54580-5_32
Metta RBecker MBokil PChakraborty SVenkatesh R(2016)TIC: a scalable model checking based approach to WCET estimationACM SIGPLAN Notices10.1145/2980930.290796151:5(72-81)Online publication date: 13-Jun-2016
https://dl.acm.org/doi/10.1145/2980930.2907961
Metta RBecker MBokil PChakraborty SVenkatesh RKuo TWhalley D(2016)TIC: a scalable model checking based approach to WCET estimationProceedings of the 17th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools, and Theory for Embedded Systems10.1145/2907950.2907961(72-81)Online publication date: 13-Jun-2016
https://dl.acm.org/doi/10.1145/2907950.2907961
Madhukar KWachter BKroening DLewis MSrivas MKaivola RWahl T(2015)Accelerating invariant generationProceedings of the 15th Conference on Formal Methods in Computer-Aided Design10.5555/2893529.2893550(105-111)Online publication date: 27-Sep-2015
https://dl.acm.org/doi/10.5555/2893529.2893550

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Handling loops in bounded model checking of C programs via k-induction

Evaluation of SAT-based Bounded Model Checking of ACTL Properties

Verification of ACTL properties by bounded model checking