Eleventh Annual IEEE Symposium on

Logic in Computer Science (LICS 1996)

Paper: Symbolic Protocol Verification with Queue BDDs (at LICS 1996)

Authors: Patrice Godefroid David E. Long


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.


    author = 	 {Patrice Godefroid and David E. Long},
    title = 	 {Symbolic Protocol Verification with Queue BDDs},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {198-206},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}