Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2018: Automated Technology for Verification and Analysis pp 441–457Cite as

Bounded Synthesis of Reactive Programs

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11138))

Abstract

Most algorithms for the synthesis of reactive systems focus on the construction of finite-state machines rather than actual programs. This often leads to badly structured, unreadable code. In this paper, we present a bounded synthesis approach that automatically constructs, from a given specification in linear-time temporal logic (LTL), a program in Madhusudan’s simple imperative language for reactive programs. We develop and compare two principal approaches for the reduction of the synthesis problem to a Boolean constraint satisfaction problem. The first reduction is based on a generalization of bounded synthesis to two-way alternating automata, the second reduction is based on a direct encoding of the program syntax in the constraint system. We report on preliminary experience with a prototype implementation, which indicates that the direct encoding outperforms the automata approach.

Supported by the European Research Council (ERC) Grant OSARES (No. 683300) and by the Saarbrücken Graduate School of Computer Science.

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 EPUB and 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

References

  1. Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. J. Symb. Log. 28(4), 289–290 (1963)

    Article  Google Scholar 

  2. Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 258–262. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_29

    Chapter  Google Scholar 

  3. Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272–275. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_25

    Chapter  Google Scholar 

  4. Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652–657. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_45

    Chapter  Google Scholar 

  5. Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: an experimentation framework for bounded synthesis. [20] 325–332

    Google Scholar 

  6. Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M., et al.: Interactive presentation: automatic hardware synthesis from specifications: a case study. In: Lauwereins, R., Madsen, J. (eds.) DATE, pp. 1188–1193. Nice, France, EDA Consortium, San Jose, CA, USA (2007)

    Google Scholar 

  7. Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5–6), 519–539 (2013)

    Article  Google Scholar 

  8. Finkbeiner, B., Klein, F.: Bounded cycle synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 118–135. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_7

    Chapter  Google Scholar 

  9. Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354–370. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_20

    Chapter  Google Scholar 

  10. Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1–8. Portland, OR, USA, IEEE (2013)

    Google Scholar 

  11. Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 317–330. Austin, TX, USA, ACM (2011)

    Google Scholar 

  12. Osera, P., Zdancewic, S.: Type-and-example-directed program synthesis. In: Grove, D., Blackburn, S. (eds.) PLDI, pp. 619–630. Portland, OR, USA, ACM (2015)

    Google Scholar 

  13. Solar-Lezama, A.: Program sketching. STTT 15(5–6), 475–495 (2013)

    Article  Google Scholar 

  14. Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. STTT 15(5–6), 413–431 (2013)

    Article  Google Scholar 

  15. Madhusudan, P.: Synthesizing reactive programs. In: Bezem, M., (ed.) CSL, Bergen, Norway. Volume 12 of LIPIcs, pp. 428–442. Schloss Dagstuhl (2011)

    Google Scholar 

  16. Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)

    Article  MathSciNet  Google Scholar 

  17. Gerstacker, C.: Bounded Synthesis of Reactive Programs, Bachelor’s Thesis (2017)

    Google Scholar 

  18. Gerstacker, C., Klein, F., Finkbeiner, B.: Bounded synthesis of reactive programs. CoRR 1807.09047 (2018)

    Google Scholar 

  19. Khalimov, A., Bloem, R.: Bounded Synthesis for Streett, Rabin, and CTL\(^{*}\). [20] 333–352

    Google Scholar 

  20. Majumdar, R., Kunčak, V. (eds.): CAV 2017. LNCS, vol. 10427. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9

    Book  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Reactive Systems Group, Saarland University, Saarbrücken, Germany

    Carsten Gerstacker, Felix Klein & Bernd Finkbeiner

Authors
  1. Carsten Gerstacker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Felix Klein
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bernd Finkbeiner
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Carsten Gerstacker .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Shuvendu K. Lahiri

  2. University of Southern California, Los Angeles, CA, USA

    Chao Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Gerstacker, C., Klein, F., Finkbeiner, B. (2018). Bounded Synthesis of Reactive Programs. In: Lahiri, S., Wang, C. (eds) Automated Technology for Verification and Analysis. ATVA 2018. Lecture Notes in Computer Science(), vol 11138. Springer, Cham. https://doi.org/10.1007/978-3-030-01090-4_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-01090-4_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-01089-8

  • Online ISBN: 978-3-030-01090-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation