Implicit Relations and Their Derivatives for Symbolic State Space Generation
In the modern-day, the ever-growing dependence on information and communication technology has led to the development of a vast number of critical applications. Despite fast-paced production and the increasing complexity of systems, the expectation of building low-defect systems is inevitable. Symbolic model checking, one of the many system verification techniques, checks every state of the system against good and bad properties to assist in building a low-defect system and requires the entire state space of the system. Saturation, a symbolic state-space generation algorithm that works faster than most explicit techniques, traditionally uses decision diagrams for encoding systems and their reachability set. While decision diagrams compactly represent large sets of states, they cause significant overhead to the saturation algorithm when used for representing system behavior. In this talk, we explore alternative novel data structures that are both compatible with saturation and more efficient with low runtime overheads with respect to the state-of-the-art techniques. The talk will be dedicated to exploring the methods, namely implicit relations, for system behavior abstraction developed to enhance the performance of the saturation algorithm. Experimental results showcasing the scope and efficiency of implicit relations and their derivatives will be presented.
Committee: Andrew Miner (major professor), Samik Basu, Gianfranco Ciardo, Robyn Lutz, and Wallapak Tavanapong
Join on Webex: https://iastate.webex.com/iastate/j.php?MTID=m6e3a295662ec030397522aec5c2d462a