Title :
Symbolic protocol verification with queue BDDs
Author :
Godefroid, Patrice ; Long, David E.
Abstract :
Symbolic verification based on Binary Decision Diagrams (BDDs) has proven to be a powerful technique for ensuring the correctness of digital hardware. In contrast, BDDs have not caught on as widely for software verification, partly because the data types used in software are more complicated than those used in hardware. In this work, we propose an extension of BDDs for dealing with dynamic data structures. Specifically, we focus on queues, since they are commonly used in modeling communication protocols. We introduce Queue BDDs (QBDDs) which include all the power of BDDs while also providing an efficient representation of queue contents. Experimental results show that QBDDs are well-suited for the verification of communication protocols
Keywords :
data structures; decision tables; formal verification; logic testing; protocols; queueing theory; symbol manipulation; Binary Decision Diagrams; Queue BDDs; data types; digital hardware; dynamic data structures; protocol verification; symbolic verification; verification of communication protocols; Automata; Binary decision diagrams; Boolean functions; Data structures; Encoding; Hardware; Protocols; Software systems; Space exploration; State-space methods;
Conference_Titel :
Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
Conference_Location :
New Brunswick, NJ
Print_ISBN :
0-8186-7463-6
DOI :
10.1109/LICS.1996.561318