Presidential Young Investigator Award: Automatic Verification of Finite State Concurrent Systems

Dill Research研究的是有限状态并发系统的验证，包括抽象系统及其硬件实现。方法是将状态集表示为二叉判定图形式的布尔函数，然后查找并检查从一组初始状态可达的状态集。协议描述语言和验证系统正在开发中，并在真实世界的设计中进行测试。此外，正在努力确定核查特别吸引人的条件，例如在系统抽象的初始设计阶段使用核查。正在为其他用户开发几个基准示例。

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.