Directed Model Checking with Distance-Preserving Abstractions

1. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.: Efficient guiding towards cost-optimality in uppaal. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)

   Chapter  Google Scholar 

2. Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: Design Automation Conference, pp. 29–34 (2000)

   Google Scholar 

3. Dierks, H.: Comparing model checking and logical reasoning for real-time systems. Formal Aspects of Computing 16(2), 104–120 (2004)

   Article  MATH  Google Scholar 

4. Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Software Tools for Technology Transfer (2003)

   Google Scholar 

5. Edelkamp, S., Lluch-Lafuente, A.: Abstraction databases in theory and model checking. In: Proc. ICAPS Workshop on Connecting Planning Theory with Practice (June 2004)

   Google Scholar 

6. Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)

   Chapter  Google Scholar 

7. Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Trail-directed model checking. Electr. Notes Theor. Comput. Sci. 55(3) (2001)

   Google Scholar 

8. Graf, S., Steffen, B., Lüttgen, G.: Compositional minimization of finite state systems using interface specifications. Formal Aspects of Computing 8, 607–616 (1996)

   Article  MATH  Google Scholar 

9. Groce, A., Visser, W.: Heuristics for model checking Java programs. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 242–245. Springer, Heidelberg (2002)

   Chapter  Google Scholar 

10. Kaltenbach, M., Misra, J.: A theory of hints in model checking. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 423–438. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

11. Krieg-Brückner, B., Peleska, J., Olderog, E.-R., Baer, A.: The UniForM workbench, a universal development environment for formal methods. In: Wing, J., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, p. 1186. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

12. Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 35–52. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

13. Lafuente, A.L.: Directed Search for the Verification of Communication Protocols. PhD thesis, Institute of Computer Science, University of Freiburg (June 2003)

    Google Scholar 

14. Larsen, K., Petterson, P., Yi, W.: Uppaal in a nutshell. STTT – International Journal on Software Tools for Technology Transfer 1(1, 2), 134–152 (1997)

    Article  MATH  Google Scholar 

15. Matsumoto, M., Nishimura, T.: Mersenne Twister: A 623-dimensionally equidistributed uniform pseudo-random number generator. ACM Transactions on Modeling and Computer Simulation 8(1), 3–30 (1998)

    Article  MATH  Google Scholar 

16. Pearl, J.: Heuristics. Morgan Kaufmann, San Francisco (1983)

    MATH  Google Scholar 

17. Qian, K., Nymeyer, A.: Guided invariant model checking based on abstraction and symbolic pattern databases. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 497–511. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

18. Sabnani, K.K., Lapone, A.M., Uyar, M.Ü.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37(9), 940–948 (1989)

    Article  Google Scholar 

19. Seitz, C.: Ideas about arbiters. Lambda, 10–14 (1980)

    Google Scholar 

20. Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Design Automation Conference, pp. 599–604 (1998)

    Google Scholar 

Download references