Skip to main content
SpringerLink
Log in

Program Model Checking via Action Planning

  • Conference paper
Model Checking and Artificial Intelligence (MoChArt 2010)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6572))

Included in the following conference series:

Abstract

In this paper we present steps towards a prototype implementation of a C++ software model checker based on AI planning technology. It parses source code annotated with assertions and translates it into the planning domain description language to invoke recent planners. Lifted back to the source code level, computed plans then serve as counterexamples. As the approach can participate from efficient planner in-built search heuristics, the verification procedure is directed. For the translation process, different aspects like parsing, generation of a dependency graph, slicing, property conversion, and data abstraction are described. The program model checker has been embedded as a plugin in the Eclipse software development environment, resulting in an interactive debugging aid. First empirical findings compare the approach with an existing directed program model checker parses the same input and executes object code.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Albarghouthi, A., Baier, J., McIlraith, S.A.: On the use of planning technology for verification. In: Workshop on ICAPS 2009 (2009)

    Google Scholar 

  2. Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: Exploiting program structure for model checking concurrent software. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 1–15. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Bakera, M., Edelkamp, S., Kissmann, P., Renner, C.D.: Solving μ-calculus parity games by symbolic planning. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS, vol. 5348, pp. 15–33. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

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

  5. Bonet, B., Haslum, P., Hickmott, S.L., Thiébaux, S.: Directed unfolding of Petri nets. T. Petri Nets and Other Models of Concurrency 1, 172–198 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 142–170 (1992)

    Article  Google Scholar 

  7. Bylander, T.: The computational complexity of propositional STRIPS planning. Artificial Intelligence, 165–204 (1994)

    Google Scholar 

  8. Cimatti, A., Giunchiglia, E., Giunchiglia, F., Traverso, P.: Planning via model checking: A decision procedure for AR. In: Steel, S. (ed.) ECP 1997. LNCS, vol. 1348, pp. 130–142. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  9. Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, strong, and strong cyclic planning via symbolic model checking. Artif. Intell. 147(1-2), 35–84 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  10. Cimatti, A., Roveri, M., Bertoli, P.: Conformant planning via symbolic model checking and heuristic search. Artif. Intell. 159(1-2), 127–206 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  11. Clarke, E., Kröning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Clarke, E., Kröning, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  14. Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)

    Google Scholar 

  15. Cordeiro, L., Fischer, B.: Bounded model checking of multi-threaded software using smt solvers, vol. abs/1003.3830 (2010)

    Google Scholar 

  16. Culberson, J.C., Schaeffer, J.: Pattern databases. Computational Intelligence 14(4), 318–334 (1998)

    Article  MathSciNet  Google Scholar 

  17. Dams, D., Namjoshi, K.S.: Orion: High-precision methods for static error analysis of C and C++ programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 138–160. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  18. Aan de Brugh, N.H.M., Nguyen, V.Y., Ruys, T.C.: moonWalker: Verification of.NET programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 170–173. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. Edelkamp, S.: Promela planning. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 197–212. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  20. Edelkamp, S., Jabbar, S.: Action planning for directed model checking of Petri nets. Electronic Notes in Theoretical Computer Science (ENTCS) 149(2), 3–18 (2006)

    Article  MATH  Google Scholar 

  21. Edelkamp, S., Jabbar, S., Lluch-Lafuente, A.: Action planning for graph transition systems. In: ICAPS 2005-Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (2005)

    Google Scholar 

  22. Edelkamp, S., Jabbar, S., Midzic, D., Rikowski, D., Sulewski, D.: External memory search for verification of multi-threaded C++ programs. KI 22(2), 44–50 (2008)

    Google Scholar 

  23. Edelkamp, S., Jabbar, S., Sulewski, D.: Distributed verification of multi-threaded C++ programs, vol. 198, pp. 33–46 (2008)

    Google Scholar 

  24. Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. STTT 5(2-3), 247–267 (2004)

    Article  MATH  Google Scholar 

  25. Edelkamp, S., Rensink, A.: Graph transformation and AI planning. In: ICAPS 2007-Workshop on the Knowledge Engineering Competition (2007)

    Google Scholar 

  26. Edelkamp, S., Schuppan, V., Bošnački, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS, vol. 5348, pp. 65–89. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  27. Fox, M., Long, D.: PDDL2.1: An extension of pddl for expressing temporal planning domains. JAIR 20, 61–124 (2003)

    MATH  Google Scholar 

  28. Gerevini, A., Haslum, P., Long, D., Saetti, A., Dimopoulos, Y.: Deterministic planning in the fifth international planning competition: 7pddl3

    Google Scholar 

  29. Gleick, J.: Little bug, big bang. New York Times vom 1 (Dezember 1996)

    Google Scholar 

  30. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  31. Groce, A., Visser, W.: Heuristics for model checking java programs. STTT 6(4), 260–276 (2004)

    Article  MATH  Google Scholar 

  32. Haslum, P., Bonet, B., Geffner, H.: New admissible heuristics for domain-independent planning. In: AAAI, pp. 1163–1168 (2005)

    Google Scholar 

  33. Havelund, K., Pressburger, T.: Model checking java programs using JAVA pathfinder. STTT 2(4), 366–381 (2000)

    Article  MATH  Google Scholar 

  34. Havelund, K., Visser, W.: Program model checking as a new trend. STTT 4(1), 8–20 (2002)

    Article  Google Scholar 

  35. Helmert, M.: Decidability and undecidability results for planning with numerical state variables. In: AIPS, pp. 303–312 (2002)

    Google Scholar 

  36. Helmert, M.: A planning heuristic based on causal graph analysis. In: ICAPS, pp. 161–170 (2004)

    Google Scholar 

  37. Helmert, M., Domshlak, C.: Landmarks, critical paths and abstractions: What’s the difference anyway? In: ICAPS (2009)

    Google Scholar 

  38. Helmert, M., Haslum, P., Hoffmann, J.: Flexible abstraction heuristics for optimal sequential planning. In: ICAPS, pp. 176–183 (2007)

    Google Scholar 

  39. Hoffmann, J.: The Metric-FF planning system: Translating ignoring delete lists to numeric state variables. JAIR 20, 291–341 (2003)

    MATH  Google Scholar 

  40. Hoffmann, J., Edelkamp, S.: The deterministic part of ipc-4: An overview, vol. 24, pp. 519–579 (2005)

    Google Scholar 

  41. Hoffmann, J., Edelkamp, S., Thiebaux, S., Englert, R., Liporace, F., Trueg, S.: Engineering benchmarks for planning: the domains used in the deterministic part of IPC-4. JAIR 26(2), 453–541 (2006)

    MATH  Google Scholar 

  42. Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)

    Google Scholar 

  43. Kautz, H.A., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search. In: AAAI, pp. 1194–1201 (1996)

    Google Scholar 

  44. König, B., Kozioura, V.: Augur - a tool for the analysis of graph transformation systems. Bulletin of the EATCS 87, 126–137 (2005)

    Article  Google Scholar 

  45. Kupferschmid, S., Hoffmann, J., Larsen, K.G.: Fast directed model checking via russian doll abstraction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 203–217. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  46. Leven, P., Mehler, T., Edelkamp, S.: Directed error detection in C++ with the assembly-level model checker stEAM. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 39–56. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  47. McDermott, D.: The 1998 AI Planning Competition. AI Magazine 21(2) (2000)

    Google Scholar 

  48. Mehler, T.: Challenges and Applications of Assembly-Level Software Model Checking. PhD thesis, Dortmund University of Technology (2006)

    Google Scholar 

  49. Merino, P., del Mar Gallardo, M., Martinez, J., Pimentel, E.: αSPIN: Extending SPIN with abstraction. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 254–258. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  50. Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 82–97. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  51. Stroustrup, B.: The C++ Programming Language, 2nd edn. Addison-Wesley Publishing Company, Reading (1994)

    MATH  Google Scholar 

  52. Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering Journal 10(2), 203–232 (2003)

    Article  Google Scholar 

  53. Visser, W., Mehlitz, P.C.: Model checking programs with Java PathFinder. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, p. 27. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  54. Wehrle, M., Helmert, M.: The causal graph revisited for directed model checking. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 86–101. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TZI, University of Bremen, Germany

    Stefan Edelkamp & Damian Sulewski

  2. TU Dortmund, Germany

    Mark Kellershoff

Authors
  1. Stefan Edelkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mark Kellershoff
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Damian Sulewski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science and Engineering, University of New South Wales, 2052, Sydney, Australia

    Ron van der Meyden

  2. Institut für Informatik, Albert-Ludwigs-Universität Freiburg, 79110, Freiburg, Germany

    Jan-Georg Smaus

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Edelkamp, S., Kellershoff, M., Sulewski, D. (2011). Program Model Checking via Action Planning. In: van der Meyden, R., Smaus, JG. (eds) Model Checking and Artificial Intelligence. MoChArt 2010. Lecture Notes in Computer Science(), vol 6572. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20674-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-20674-0_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-20673-3

  • Online ISBN: 978-3-642-20674-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation