Dill Research is on the verification of finite-state concurrent systems, both abstract systems and their implementations in hardware. The approach is to represent the set of states as a boolean function in the form of a binary decision diagram, then find and inspect the set of states reachable from a set of initial states. A protocol description language and a verification system are being developed and tested on real-world designs. Additionally, effort is being made to characterize conditions under which verification is particularly attractive, for example using it in the initial design phase when the system is abstract. Several benchmark examples for other users are being developed.
