Taxonomic Search: byron OR cook, Presentation
Modern software systems are ubiquitous and complex, often running on critical platforms ranging from human implant devices to nuclear power plant controls. How can we be sure that these programs will behave as intended? Programmers must first specify the correct behavior of their programs, and one widely accepted specification language is temporal logic. Despite decades of research in finite-state contexts and some adaptations of finite-state algorithms, we still lack scalable tools for proving temporal logic properties of software.
Dr. Ben Cook is currently acting senior manager of Sandia National Laboratories’ Information and Cognitive Sciences Group, which focuses on exploratory research in data analytics, visualization, cognitive science and mathematical modeling. This group also provides stewardship of Sandia’s Cyber Engineering Research Institute facility in New Mexico.
I will describe a new approach to the old problem of automatic temporal property verification. As well as leading to dramatic performance improvements over existing techniques, this approach also brings some light to a couple of age-old questions.