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) Proceedings of TACAS’01. Lecture Notes in Computer Science, vol. 2031, pp. 174–188. Springer, Berlin (2001)

   Google Scholar 

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

3. Dierks H.: Comparing model checking and logical reasoning for real-time systems. Formal Aspects Comput. 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)

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

6. Edelkamp S., Lluch-Lafuente A., Leue S.: Directed explicit model checking with hsf-spin. In: Dwyer, M.B. (eds) Proceedings of SPIN’01. Lecture Notes in Computer Science, vol. 2057, pp. 57–79. Springer, Berlin (2001)

   Google Scholar 

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

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

   Article  MATH  Google Scholar 

9. Groce, A., Visser, W.: Heuristics for model checking Java programs. In: Proceedings of SPIN’02, Lecture Notes in Computer Science, vol. 2318, pp. 242–245. Springer, Berlin (2002)

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. Lecture Notes in Computer Science, vol. 2757, pp. 423–438. Springer, Berlin (2003)

    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’99—Formal Methods: World Congress on Formal Methods in the Development of Computing Systems. Lecture Notes in Computer Science, vol. 1709 (1999)

12. Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) 13th International SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science, vol. 3925, pp. 35–52 (2006)

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

14. Larsen K., Petterson P., Yi W.: Uppaal in a nutshell. STTT—Int. J. Softw. Tools Technol. Transf. 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 Trans. Model. Comput. Simul. 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.) Proceedings of TACAS’04. Lecture Notes in Computer Science, vol. 2988, pp. 497–511 (2004)

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 1, 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)

Download references