Directed explicit-state model checking in the validation of communication protocols

Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Petterson, P., Romijn, J., Vaandrager, F.W.: Efficient guiding towards cost-imality in uppaal. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 2031. Springer, 2001

Bertoli, P., Cimatti, A., Roveri, M.: Heuristic search symbolic model checking = efficient conformant planning. In: International Joint Conference on Artificial Intelligence (IJCAI), 2001

Biere, A.: μcke - efficient μ-calculus model checking. In: Computer Aided Verification (CAV), 1997, pp. 468–471

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

Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM, 30(2): 323–342, Apr 1983

Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, 2000

Cobleigh, J.M., Clarke, L.A., Osterweil, L.J.: The right algorithm at the right time: Comparing data flow analysis algorithms for finite s tate verification. In: 23rd International Conference on Software Engineering (ICSE). IEEE Computer Society, 2001, pp. 37–46

Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. The MIT Press, 1990

Dijkstra, E.W.: A note on two problems in connection with graphs. Numerische Mathematik, 1: 269–271, 1959

Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: 21st International Conference on Software Engineering (ICSE). IEEE Computer Society, 1999, pp. 411–420

Edelkamp, S.: Data Structures, and Learning Algorithms in State Space Search. PhD thesis, University of Freiburg, 1999. Infix.

Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: 8th International SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science 2057. Springer Verlag, 2001

Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Protocol verification with heuristic search. In: AAAI Symposium on Model-based Validation of Intelligence, 2001

Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Trail-directed model checking. In: Workshop on Software Model Checking, Electrical Notes in Theoretical Computer Science. Elsevier, 2001

Edelkamp, S., Reffel, F.: OBDDs in heuristic search. In: German Conference on Artificial Intelligence (KI), 1998, pp. 81–92

Edelkamp, S., Schrödl, S.: Localizing A*. In: National Conference on Artificial Intelligence (AAAI), 2000, pp. 885–890

Gouda, M.G.: Protocol verification made simple: a tutorial. Computer Networks and ISDN Systems, 25(9): 969–980, 1993

Groce, A., Visser, W.: Model checking java programs using structural heuristics. In: International Symposium on Software Testing and Analysis (ISSTA). ACM Press, 2002

Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for heuristic determination of minimum path cost. IEEE Transactions on on Systems Science and Cybernetics, 4: 100–107, 1968

Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, 1990

Holzmann, G.J.: The model checker Spin. IEEE Transactions on Software Engineering, Special issue on Formal Methods in Software Practice, 23(5):279–295, May 1997

Kamel, M., Leue, S.: Formalization and validation of the general inter-orb protocol (GIOP) using Promela and SPIN. In: Software Tools for Technology Transfer (STTT), 2: 394–409, 2000

Kamel, M., Leue, S.: Vip: A visual editor and compiler for v-promela. In: 6th International Conference, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 1785. Springer, 2000, pp. 471–486

Korf, R.E.: Depth-first iterative-deepening: An optimal admissible tree search. International Joint Conference on Artificial Intelligence (IJCAI), 27(1): 97–109, 1985

Lin, F.J., Chu, P.M., Liu, M.T.: Protocol verification using reachability analysis: the state space explosion problem and relief strategies. In: ACM SIGCOMM, 1987, pp. 126–135

Lluch-Lafuente, A., Leue, S., Edelkamp, S.: Partial order reduction in directed model checking. In: SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science, vol. 2318. Springer, 2002, pp. 112–127

Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992

McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Press, 1993

McVitie, D.G., Wilson, L.B.: The stable marriage problem. Communications of the ACM, 14(7): 486–492, 1971

Muller, D.E., Saoudi, A., Schnupp, P.E.: Alternating automata. The weak monadic theory of the tree, its complexity. In: Laurent Kott (ed.) International Colloquium on Automata, Languages and Programming. Springer, 1986, pp. 275–283

Khurshid, S, Khurshid, P.: Exploring very large state spaces using genetic algorithms. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 2280. Springer, 2002, pp. 266–280

Reffel, F., Edelkamp, S.: Error detection with directed symbolic model checking. In: World Congress on Formal Methods. Springer, 1999, pp. 195–211

Somenzi, F., Bloem, R.: Efficient buchi automata from LTL formulae. In: Computer Aided Verification, 2000

Visser, W., Barringer, H.: Practical CTL* model checking: Should SPIN be extended? Int J Softw Tools Technol Transfer 2(4): 350–365, 2000

Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Design Automatin Conference (DAC). ACM/IEEE, 1998, pp. 599–604