Skip to main content
SpringerLink
Log in

Program Generation Using Simulated Annealing and Model Checking

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2016)

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

Included in the following conference series:

Abstract

Program synthesis can be viewed as an exploration of the search space of candidate programs in pursuit of an implementation that satisfies a given property. Classic synthesis techniques facilitate exhaustive search, while genetic programming has recently proven the potential of generic search techniques. But is genetic programming the right search technique for the synthesis problem? In this paper we challenge this belief and argue in favor of simulated annealing, a different class of general search techniques. We show that, in hindsight, the success of genetic programming has drawn from what is arguably a hybrid between simulated annealing and genetic programming, and compare the fitness of classic genetic programming, the hybrid form, and pure simulated annealing. Our experimental evaluation suggests that pure simulated annealing offers better results for automated programming than techniques based on genetic programming.

This work was supported by the Ministry of Higher Education in Iraq through the University of Kirkuk and by the EPSRC through grant EP/M027287/1.

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

Institutional subscriptions

Notes

  1. 1.

    The changes are usually not referred to as mutations, but the rules of obtaining them are the same. We use the term mutations for simulated annealing, too, in order to ease the comparison between simulated annealing and genetic programming.

References

  1. Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.L., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  2. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  3. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Clark, J.A., Jacob, J.L.: Protocols are programs too: the meta-heuristic search for security protocols. Inf. Softw. Technol. 43, 891–904 (2001)

    Article  Google Scholar 

  5. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  6. Clarke Jr., E.M., Grumberg, O., Peled, O.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  7. David, C., Kroening, D., Lewis, M.: Using program synthesis for program analysis. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 483–498. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48899-7_34

    Chapter  Google Scholar 

  8. Davis, L.: Genetic Algorithms and Simulated Annealing. Morgan Kaufmann Publishers Inc., San Francisco (1987)

    MATH  Google Scholar 

  9. Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8, 569 (1965)

    Article  Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. Fearnley, J., Peled, D., Schewe, S.: Synthesis of succinct systems. J. Comput. Syst. Sci. 81(7), 1171–1193 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  12. 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 

  13. Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: LICS, pp. 321–330. IEEE Computer Society Press (2005)

    Google Scholar 

  14. Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transfer 15(5–6), 519–539 (2013)

    Article  MATH  Google Scholar 

  15. Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312–317. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  16. Henderson, D., Jacobson, S.H., Johnson, A.W.: The theory and practice of simulated annealing. In: Glover, F., Kochenberger, G.A. (eds.) Handbook of Metaheuristics, pp. 287–319. Springer, New York (2003)

    Google Scholar 

  17. Henzinger, T.A., Otop, J.: From model checking to model measuring. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 273–287. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  18. Holzmann, G.J.: The model checker SPIN. Softw. Eng. 23(5), 279–295 (1997)

    Article  MathSciNet  Google Scholar 

  19. Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226–238. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  20. Johnson, C.G.: Genetic programming with fitness based on model checking. In: Ebner, M., O’Neill, M., Ekárt, A., Vanneschi, L., Esparcia-Alcázar, A.I. (eds.) EuroGP 2007. LNCS, vol. 4445, pp. 114–124. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  21. Katz, G., Peled, D.A.: Model checking-based genetic programming with an application to mutual exclusion. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 141–156. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Katz, G., Peled, D.: Model checking driven heuristic search for correct programs. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS, vol. 5348, pp. 122–131. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. Katz, G., Peled, D.: Synthesizing solutions to the leader election problem using model checking and genetic programming. In: Namjoshi, K., Zeller, A., Ziv, A. (eds.) HVC 2009. LNCS, vol. 6405, pp. 117–132. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Koza, J.R.: Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, Cambridge (1992)

    MATH  Google Scholar 

  25. Kupferman, O., Vardi, M.Y.: Church’s problem revisited. Bull. Symb. Logic 5(2), 245–263 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  26. Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  27. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  28. Lahtinen, J., Myllymäki, P., Silander, T., Tirri, H.: Empirical comparison of stochastic algorithms. In: 2NWGA, pp. 45–60 (1996)

    Google Scholar 

  29. Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97–107. ACM (1985)

    Google Scholar 

  30. Madhusudan, P., Thiagarajan, P.S.: Distributed controller synthesis for local specifications. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 396–407. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  31. Mann, J., Smith, G.: A comparison of heuristics for telecommunications traffic routing. In: Modern Heuristic Search Methods, pp. 235–254 (1996)

    Google Scholar 

  32. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE Computer Society Press (1977)

    Google Scholar 

  33. Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: FOCS, pp. 746–757. IEEE Computer Society Press (1990)

    Google Scholar 

  34. Schewe, S., Finkbeiner, B.: Synthesis of asynchronous systems. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 127–142. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  35. Solar-Lezama, A.: Program sketching. Int. J. Softw. Tools Technol. Transf. 15(5–6), 475–495 (2013)

    Article  Google Scholar 

  36. von Essen, C., Jobstmann, B.: Program repair without regret. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 896–911. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Liverpool, Liverpool, UK

    Idress Husien & Sven Schewe

Authors
  1. Idress Husien
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sven Schewe
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Idress Husien .

Editor information

Editors and Affiliations

  1. IMT - School for Advanced Studies, Lucca, Italy

    Rocco De Nicola

  2. Institute of Computer Languages, TU Wien, Wien, Austria

    Eva Kühn

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Husien, I., Schewe, S. (2016). Program Generation Using Simulated Annealing and Model Checking. In: De Nicola, R., Kühn, E. (eds) Software Engineering and Formal Methods. SEFM 2016. Lecture Notes in Computer Science(), vol 9763. Springer, Cham. https://doi.org/10.1007/978-3-319-41591-8_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-41591-8_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-41590-1

  • Online ISBN: 978-3-319-41591-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation