More Web Proxy on the site http://driver.im/

Article

ExpliSAT: Guiding SAT-based software verification with explicit states

Authors:

Daniel Kroening,

Ishai RabinovitzAuthors Info & Claims

HVC'06: Proceedings of the 2nd international Haifa verification conference on Hardware and software, verification and testing

Pages 138 - 154

Published: 23 October 2006 Publication History

Abstract

We present a hybrid method for software model checking that combines explicit-state and symbolic techniques. Our method traverses the control flow graph of the program explicitly, and encodes the data values in a CNF formula, which we solve using a SAT solver. In order to avoid traversing control flow paths that do not correspond to a valid execution of the program we introduce the idea of a representative of a control path. We present favorable experimental results, which show that our method scales well both with regards to the nondeterministic data and the number of threads.

References

[1]

T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: Exploiting program structure for model checking concurrent software. In CONCUR, 2004.

[2]

T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN, pages 113-130, 2000.

Digital Library

[3]

S. Barner, Z. Glazberg, and I. Rabinovitz. Wolf - bug hunter for concurrent software using formal methods. In CAV, pages 153-157, 2005.

Digital Library

[4]

S. Barner and I. Rabinovitz. Effcient symbolic model checking of software using partial disjunctive partitioning. In CHARME, pages 35-50, 2003.

[5]

H. Chockler, E. Farchi, Z. Glazberg, B. Godlin, Y. Nir-Buchbinder, and I. Rabinovitz. Formal verification of concurrent software: two case studies. In Proceedings of 4th International Workshop on Parallel and Distributed Systems: Testing and Debugging (PADTAD), 2006.

Digital Library

[6]

E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

Digital Library

[7]

R. Cytron, J. Ferrante, B. Rosen, M. Wegman, and F. Zadeck. An efficient method of computing static single assignment form. In POPL, pages 25-35. ACM, 1989.

Digital Library

[8]

C. Eisner. Model checking the garbage collection mechanism of SMV. In ENTCS, volume 55. Elsevier Science Publishers, 2001.

[9]

C. Eisner. Formal verification of software source code through semi-automatic modeling. Software and Systems Modeling, 4(1):14-31, February 2005.

Digital Library

[10]

E. Farchi, Y. Nir, and S. Ur. Concurrent bug patterns and how to test them. In IPDPS, page 286b. IEEE, 2003.

Digital Library

[11]

P. Godefroid. VeriSoft: A tool for the automatic analysis of concurrent reactive software. In CAV, pages 476-479. Springer, 1997.

Digital Library

[12]

P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In PLDI, pages 213-223. ACM, 2005.

Digital Library

[13]

G. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279-295, 1997.

Digital Library

[14]

G. Holzmann and D. Peled. An improvement in formal verification. In Proc. Formal Description Techniques, FORTE94, pages 197-211. Chapman & Hall, 1994.

Digital Library

[15]

F. Ivancic, Z. Yang, A. Gupta, M. K. Ganai, and P. Ashar. Efficient SAT-based bounded model checking for software verification, 2004.

[16]

S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In TACAS, pages 553-568, 2003.

Digital Library

[17]

D. Kroening, E. Clarke, and K. Yorav. Behavioral consistency of C and Verilog programs using bounded model checking. In DAC, pages 368-371. ACM, 2003.

Digital Library

[18]

I. Rabinovitz and O. Grumberg. Bounded model checking of concurrent programs. In CAV, volume 3576 of LNCS, pages 82-97. Springer, 2005.

Digital Library

[19]

K. Sen and G. Agha. Cute and jcute : Concolic unit testing and explicit path model-checking tools. In CAV. Tool Paper, 2006.

Digital Library

Cited By

Abadi MKeidar-Barner SPidan DVeksler T(2019)Verifying Parallel Code After Refactoring Using Equivalence CheckingInternational Journal of Parallel Programming10.1007/s10766-017-0548-447:1(59-73)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10766-017-0548-4
Chockler HRuah SWahler MDig D(2012)Verification of software changes with ExpliSATProceedings of the 4th International Workshop on Hot Topics in Software Upgrades10.5555/2664350.2664357(31-35)Online publication date: 3-Jun-2012
https://dl.acm.org/doi/10.5555/2664350.2664357
Siegel SMironova AAvrunin GClarke L(2008)Combining symbolic execution with model checking to verify parallel numerical programsACM Transactions on Software Engineering and Methodology10.1145/1348250.134825617:2(1-34)Online publication date: 5-May-2008
https://dl.acm.org/doi/10.1145/1348250.1348256

ExpliSAT: Guiding SAT-based software verification with explicit states

Recommendations

Verification of software changes with ExpliSAT
HotSWUp '12: Proceedings of the 4th International Workshop on Hot Topics in Software Upgrades

We describe an algorithm for efficient formal verification of changes in software built on top of a model-checking procedure that traverses the control flow graph explicitly while representing the data symbolically. The main idea of our algorithm is to ...
On stateless multihead automata: Hierarchies and the emptiness problem

We look at stateless multihead finite automata in their two-way and one-way, deterministic and nondeterministic variations. The transition of a k-head automaton depends solely on the symbols currently scanned by its k heads, and every such transition ...
Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata
Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures - Volume 5504

The nonemptiness problem for nondeterministic automata on infinite words can be reduced to a sequence of reachability queries. The length of a shortest witness to the nonemptiness is then polynomial in the automaton. Nonemptiness algorithms for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

HVC'06: Proceedings of the 2nd international Haifa verification conference on Hardware and software, verification and testing

October 2006

235 pages

ISBN:9783540708889

Editors:
Eyal Bin
IBM Labs, Haifa University, Haifa, Israel
,
Avi Ziv
IBM Labs, Haifa University, Haifa, Israel
,
Shmuel Ur
IBM Labs, Haifa University, Haifa, Israel

Sponsors

CRI
IBM: IBM

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 23 October 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 12 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Abadi MKeidar-Barner SPidan DVeksler T(2019)Verifying Parallel Code After Refactoring Using Equivalence CheckingInternational Journal of Parallel Programming10.1007/s10766-017-0548-447:1(59-73)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10766-017-0548-4
Chockler HRuah SWahler MDig D(2012)Verification of software changes with ExpliSATProceedings of the 4th International Workshop on Hot Topics in Software Upgrades10.5555/2664350.2664357(31-35)Online publication date: 3-Jun-2012
https://dl.acm.org/doi/10.5555/2664350.2664357
Siegel SMironova AAvrunin GClarke L(2008)Combining symbolic execution with model checking to verify parallel numerical programsACM Transactions on Software Engineering and Methodology10.1145/1348250.134825617:2(1-34)Online publication date: 5-May-2008
https://dl.acm.org/doi/10.1145/1348250.1348256

View Options

View options

Media

Figures

Other

Tables

View Table of Contents