Skip to main content
SpringerLink
Log in

Program Sketching via CTL* Model Checking

  • Conference paper
Model Checking Software (SPIN 2011)

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

Included in the following conference series:

Abstract

Sketching is an approach to automated software synthesis where the programmer develops a partial implementation called a sketch and a separate specification of the desired functionality. A synthesizer tool then automatically completes the sketch to a complete program that satisfies the specification. Previously, sketching has been applied to finite programs with a desired functional input/output behavior and given invariants. In this paper, we consider (non-terminating) reactive programs and use the full branching time logic CTL* to formalize specifications. We show that the sketching problem can be reduced to a CTL* model checking problem provided there is a translation of the program to labeled transition systems.

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

Access this chapter

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 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Le Guernic, P., de Simone, R.: The synchronous languages twelve years later. Proceedings of the IEEE 91(1), 64–83 (2003)

    Article  Google Scholar 

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

    Article  Google Scholar 

  3. Bodík, R., Chandra, S., Galenson, J., Kimelman, D., Tung, N., Barman, S., Rodarmor, C.: Programming with angelic nondeterminism. In: Hermenegildo, M., Palsberg, J. (eds.) Principles of Programming Languages (POPL), Madrid, Spain, pp. 339–352. ACM, New York (2010)

    Google Scholar 

  4. Dijkstra, E.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  5. Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, ch.16, pp. 995–1072. Elsevier, Amsterdam (1990)

    Google Scholar 

  6. Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time strikes back. In: Principles of Programming Languages (POPL), pp. 84–96. ACM, USA (1985)

    Google Scholar 

  7. Filiot, E., Jin, N., Raskin, J.-F.: Compositional algorithms for LTL synthesis. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 112–127. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Halbwachs, N.: Synchronous programming of reactive systems. Kluwer, Dordrecht (1993)

    Book  MATH  Google Scholar 

  9. Knuth, D.: The Art of Computer Programming, vol. 2. Addison-Wesley, London (1998)

    MATH  Google Scholar 

  10. Morgenstern, A., Schneider, K.: A LTL fragment for GR(1)-synthesis. In: International Workshop on Interactions, Games and Protocols (IWIGP), Electronic Proceedings in Theoretical Computer Science (EPTCS), Saarbrücken, Germany (2011)

    Google Scholar 

  11. Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 474–488. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Schneider, K.: Verification of Reactive Systems - Formal Methods and Algorithms. In: Texts in Theoretical Computer Science (EATCS Series). Springer, Heidelburg (2003)

    Google Scholar 

  13. Schneider, K.: The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern (2009)

    Google Scholar 

  14. Shade, E.: Size matters: lessons from a broken binary search. Journal of Computing Sciences in Colleges (JCSC) 24(5), 175–182 (2009)

    Google Scholar 

  15. Solar-Lezama, A.: Program Synthesis by Sketching. PhD thesis, University of California, Berkeley, California, USA (2008)

    Google Scholar 

  16. Solar-Lezama, A., Rabbah, R.,Bodík, R., Ebcioğlu, K.: Programming by sketching for bit streaming programs. In: Hall, M. (ed.) Programming Language Design and Implementation (PLDI), pp. 281–294. ACM, Chicago (2005)

    Google Scholar 

  17. Solar-Lezama, A., Tancau, L., Bodik, R., Saraswat, V., Seshia, S.: Combinatorial sketching for finite programs. In: Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 404–415. ACM, USA (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Kaiserslautern, P.O. Box 3049, 67653, Kaiserslautern, Germany

    Andreas Morgenstern & Klaus Schneider

Authors
  1. Andreas Morgenstern
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Klaus Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Oregon State University, 1148 Kelley Engineering Center, 97331-5501, Corvallis, OR, USA

    Alex Groce

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

    Madanlal Musuvathi

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Morgenstern, A., Schneider, K. (2011). Program Sketching via CTL* Model Checking. In: Groce, A., Musuvathi, M. (eds) Model Checking Software. SPIN 2011. Lecture Notes in Computer Science, vol 6823. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22306-8_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22306-8_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22305-1

  • Online ISBN: 978-3-642-22306-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation