Skip to main content
SpringerLink
Log in
Book cover

International Conference on Verification, Model Checking, and Abstract Interpretation

VMCAI 2014: Verification, Model Checking, and Abstract Interpretation pp 1–20Cite as

SAT-Based Synthesis Methods for Safety Specs

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8318))

Abstract

Automatic synthesis of hardware components from declarative specifications is an ambitious endeavor in computer aided design. Existing synthesis algorithms are often implemented with Binary Decision Diagrams (BDDs), inheriting their scalability limitations. Instead of BDDs, we propose several new methods to synthesize finite-state systems from safety specifications using decision procedures for the satisfiability of quantified and unquantified Boolean formulas (SAT-, QBF- and EPR-solvers). The presented approaches are based on computational learning, templates, or reduction to first-order logic. We also present an efficient parallelization, and optimizations to utilize reachability information and incremental solving. Finally, we compare all methods in an extensive case study. Our new methods outperform BDDs and other existing work on some classes of benchmarks, and our parallelization achieves a super-linear speedup.

This work was supported in part by the Austrian Science Fund (FWF) through projects RiSE (S11406-N23 and S11408-N23) and QUAINT (I774-N23), and by the European Commission through project STANCE (317753).

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Becker, B., Ehlers, R., Lewis, M., Marin, P.: ALLQBF solving by computational learning. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 370–384. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  2. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. FAIA, vol. 185. IOS Press (2009)

    Google Scholar 

  4. Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. Electronic Notes in Theoretical Computer Science 190(4), 3–16 (2007)

    Article  Google Scholar 

  5. Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. CoRR, abs/1311.3530 (2013), http://arxiv.org/abs/1311.3530

  6. Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Brayton, R., Mishchenko, A.: ABC: An academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Ehlers, R.: Symbolic bounded synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 365–379. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  9. Ehlers, R., Könighofer, R., Hofferek, G.: Symbolically synthesizing small circuits. In: FMCAD 2012, pp. 91–100. IEEE (2012)

    Google Scholar 

  10. Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1-3), 35–45 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  11. Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 263–277. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Fröhlich, A., Kovasznai, G., Biere, A.: A DPLL algorithm for solving DQBF. In: Pragmatics of SAT (PoS 2012, aff. to SAT 2012) (2012)

    Google Scholar 

  13. Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 230–244. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. Jiang, J.-H.R., Lin, H.-P., Hung, W.-L.: Interpolating functions from large boolean relations. In: International Conference on Computer-Aided Design (ICCAD 2009), pp. 779–784. IEEE (2009)

    Google Scholar 

  15. Kojevnikov, A., Kulikov, A.S., Yaroslavtsev, G.: Finding efficient circuits using SAT-solvers. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 32–44. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  16. Könighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: FMCAD 2011, pp. 91–100. IEEE (2011)

    Google Scholar 

  17. Korovin, K.: iProver – an instantiation-based theorem prover for first-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292–298. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317–353 (1980)

    Article  MATH  Google Scholar 

  19. Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. JSAT 7(2-3), 71–76 (2010)

    Google Scholar 

  20. Moon, I., Kukula, J.H., Shiple, T.R., Somenzi, F.: Least fixpoint approximations for reachability analysis. In: ICCAD 1999, pp. 41–44. IEEE (1999)

    Google Scholar 

  21. Morgenstern, A., Gesell, M., Schneider, K.: Solving games using incremental induction. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 177–191. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  22. Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF (tool presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 430–435. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  23. Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293–304 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  24. Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  25. Seidl, M., Könighofer, R.: Partial witnesses from preprocessed quantified Boolean formulas. In: DATE 2014 (to appear, 2014)

    Google Scholar 

  26. Seidl, M., Lonsing, F., Biere, A.: qbf2epr: A tool for generating EPR formulas from QBF. In: Workshop on Practical Aspects of Automated Reasoning (2012)

    Google Scholar 

  27. Sohail, S., Somenzi, F.: Safety first: A two-stage algorithm for LTL games. In: FMCAD 2009, pp. 77–84. IEEE (2009)

    Google Scholar 

  28. Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 4–13. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  29. Staber, S., Bloem, R.: Fault localization and correction with QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 355–368. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  30. Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Applied Information Processing and Communications (IAIK), Graz University of Technology, Austria

    Roderick Bloem & Robert Könighofer

  2. Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria

    Martina Seidl

Authors
  1. Roderick Bloem
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert Könighofer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martina Seidl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. One Microsoft Way, Microsoft Research, 98052, Redmond, WA, USA

    Kenneth L. McMillan

  2. DI - Ecole Normale Supérieure, 45, rue d’Ulm, 75230, Paris Cedex 05, France

    Xavier Rival

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bloem, R., Könighofer, R., Seidl, M. (2014). SAT-Based Synthesis Methods for Safety Specs. In: McMillan, K.L., Rival, X. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2014. Lecture Notes in Computer Science, vol 8318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54013-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-54013-4_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-54012-7

  • Online ISBN: 978-3-642-54013-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation