Article

Symbolic Reachability Analysis Based on SAT-Solvers

Authors:

Parosh Aziz Abdulla,

Niklas EénAuthors Info & Claims

TACAS '00: Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000

Pages 411 - 425

Published: 25 March 2000 Publication History

Abstract

The introduction of symbolic model checking using Binary Decision Diagrams (BDDs) has led to a substantial extension of the class of systems that can be algorithmically verified. Although BDDs have played a crucial role in this success, they have some well-known drawbacks, such as requiring an externally supplied variable ordering and causing space blowups in certain applications. In a parallel development, SAT-solving procedures, such as Stålmarck's method or the Davis-Putnam procedure, have been used successfully in verifying very large industrial systems. These efforts have recently attracted the attention of the model checking community resulting in the notion of bounded model checking. In this paper, we show how to adapt standard algorithms for symbolic reachability analysis to work with SAT-solvers. The key element of our contribution is the combination of an algorithm that removes quantifiers over propositional variables and a simple representation that allows reuse of subformulas. The result will in principle allow many existing BDD-based algorithms to work with SAT-solvers. We show that even with our relatively simple techniques it is possible to verify systems that are known to be hard for BDD-based model checkers.

References

[1]

H. R. Andersen and H. Hulgaard. Boolean expression diagrams. In Proc. 12th IEEE Int. Symp. on Logic in Computer Science, pages 88-98, 1997.

[2]

A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Design Automation Conference (DAC'99), 1999.

[3]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS '98, 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 1999.

[4]

J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142- 170, 1992.

[5]

A. Biere, E. M. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC{tm} microprocessor using symbolic model checking without BDDs. In Proc. 11th Int. Conf. on Computer Aided Verification, 1999.

[6]

P. Bjesse. Symbolic model checking with sets of states represented as formulas. Technical Report CS-1999-100, Department of Computer Science, Chalmers technical university, March 1999.

[7]

A. Borälv. The industrial success of verification tools based on Stålmarck's method. In Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 7-10, 1997.

[8]

A. Borälv. Case study: Formal verification of a computerized railway interlocking. Formal Aspects of Computing, 10(4):338-360, 1998.

[9]

R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8):677-691, Aug. 1986.

[10]

E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems, 8(2):244-263, April 1986.

[11]

N. EÉn. Symbolic reachability analysis based on SAT-solvers. Master's thesis, Dept. of Computer Systems, Uppsala university, 1999.

[12]

J.F. Groote, S.F.M. van Vlijmen, and J.W.C. Koorn. The safety guaranteeing system at station Hoorn-Kersenboogerd. In COMPASS'95, 1995.

[13]

H. Hulgaard, P.F. Williams, and H.R. Andersen. Combinational logic-level verification using boolean expression diagrams. In 3rd International Workshop on Applications of the Reed-Muller Expansion in Circuit Design, 1997.

[14]

K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

[15]

C. Papadimitriou. Computational complexity. Addison-Wesley, 1994.

[16]

J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In 5th International Symposium on Programming, Turin, volume 137 of Lecture Notes in Computer Science, pages 337-352. Springer Verlag, 1982.

[17]

G. Stälmarck and M. Säflund. Modelling and verifying systems and software in propositional logic. In SAFECOMP'90, pages 31-36. Pergamon Press, 1990.

[18]

M. Sheeran and G. Stålmarck. A tutorial on Stålmarck's method of propositional proof. Formal Methods In System Design, 16(1), 2000.

[19]

G. Stålmarck. A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula. Swedish Patent No. 467 076 (approved 1992), US patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995).

[20]

H. Zhang. SATO: an efficient propositional prover. In Proc. Int. Conference om Automated Deduction (CADE'97), volume 1249 of LNAI, pages 272- 275. Springer Verlag, 1997.

Cited By

Torlak EBodik RHosking AEugster PHirschfeld R(2013)Growing solver-aided languages with rosetteProceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software10.1145/2509578.2509586(135-152)Online publication date: 29-Oct-2013
https://dl.acm.org/doi/10.1145/2509578.2509586
Lomuscio APenczek W(2012)Symbolic model checking for temporal-epistemic logicLogic Programs, Norms and Action10.5555/2340883.2340896(172-195)Online publication date: 1-Jan-2012
https://dl.acm.org/doi/10.5555/2340883.2340896
Hassan ZBradley ASomenzi F(2012)Incremental, inductive CTL model checkingProceedings of the 24th international conference on Computer Aided Verification10.1007/978-3-642-31424-7_38(532-547)Online publication date: 7-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31424-7_38
Show More Cited By

Symbolic Reachability Analysis Based on SAT-Solvers
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation

Recommendations

SAT-based unbounded symbolic model checking
DAC '03: Proceedings of the 40th annual Design Automation Conference

This paper describes a SAT-based unbounded symbolic model checking algorithm. BDDs have been widely used for symbolic model checking, but the approach suffers from memory overflow. The SAT procedure was exploited to overcome the problem, but it verified ...
Improvements in SAT-based Reachability Analysis for Timed Automata
Concurrency Specification and Programming (CS&P 2003)

The paper deals with the problem of checking reachability for timed automata. In order to check reachability of a~state satisfying some property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a ...
Tightening BDD-based approximate reachability with SAT-based clause generalization
DATE '14: Proceedings of the conference on Design, Automation & Test in Europe

In the framework of symbolic model checking, BDD-based approximate reachability is potentially much more scalable than its exact counterpart. However, its practical applicability is highly limited by its static approach to abstraction, and the intrinsic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

TACAS '00: Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000

March 2000

549 pages

ISBN:3540672826

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 25 March 2000

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Torlak EBodik RHosking AEugster PHirschfeld R(2013)Growing solver-aided languages with rosetteProceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software10.1145/2509578.2509586(135-152)Online publication date: 29-Oct-2013
https://dl.acm.org/doi/10.1145/2509578.2509586
Lomuscio APenczek W(2012)Symbolic model checking for temporal-epistemic logicLogic Programs, Norms and Action10.5555/2340883.2340896(172-195)Online publication date: 1-Jan-2012
https://dl.acm.org/doi/10.5555/2340883.2340896
Hassan ZBradley ASomenzi F(2012)Incremental, inductive CTL model checkingProceedings of the 24th international conference on Computer Aided Verification10.1007/978-3-642-31424-7_38(532-547)Online publication date: 7-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31424-7_38
Woźna-Szcześniak BZbrzezny A(2012)SAT-Based bounded model checking for deontic interleaved interpreted systemsProceedings of the 6th KES international conference on Agent and Multi-Agent Systems: technologies and applications10.1007/978-3-642-30947-2_54(494-503)Online publication date: 25-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-30947-2_54
Pigorsch FScholl CSapatnekar S(2010)An AIG-Based QBF-solver using SAT for preprocessingProceedings of the 47th Design Automation Conference10.1145/1837274.1837318(170-175)Online publication date: 13-Jun-2010
https://dl.acm.org/doi/10.1145/1837274.1837318
Chambers BManolios PVroon DBenini LDe Micheli GAl-Hashimi BMueller W(2009)Faster SAT solving with better CNF generationProceedings of the Conference on Design, Automation and Test in Europe10.5555/1874620.1875002(1590-1595)Online publication date: 20-Apr-2009
https://dl.acm.org/doi/10.5555/1874620.1875002
Claessen KEen NSheeran MSörensson NVoronov AÅkesson K(2009)SAT-Solving in Practice, with a Tutorial Example from Supervisory ControlDiscrete Event Dynamic Systems10.1007/s10626-009-0081-819:4(495-524)Online publication date: 1-Dec-2009
https://dl.acm.org/doi/10.1007/s10626-009-0081-8
Cabodi GCamurati PGarcia LMurciano MNocco SQuer S(2008)Trading-off SAT search and variable quantifications for effective unbounded model checkingProceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design10.5555/1517424.1517450(1-8)Online publication date: 17-Nov-2008
https://dl.acm.org/doi/10.5555/1517424.1517450
Cabodi GCamurati PMurciano MNassif SRoychowdhury J(2008)Automated abstraction by incremental refinement in interpolant-based model checkingProceedings of the 2008 IEEE/ACM International Conference on Computer-Aided Design10.5555/1509456.1509495(129-136)Online publication date: 10-Nov-2008
https://dl.acm.org/doi/10.5555/1509456.1509495
Cabodi GMurciano MNocco SQuer S(2008)Boosting interpolation with dynamic localized abstraction and redundancy removalACM Transactions on Design Automation of Electronic Systems10.1145/1297666.129766913:1(1-20)Online publication date: 6-Feb-2008
https://dl.acm.org/doi/10.1145/1297666.1297669
Show More Cited By

View Options

View options

Get Access

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents