This talk addresses the following problem: given a finite set of system executions, and a template of expected behavior given as a formula in temporal logic with missing sub-formulas, compute the missing sub-formulas that make the formula true for all executions. This so-called query-checking problem has many applications in the analysis of time-series data, including vulnerability detection in server logs and financial trend discovery, as well as generally in system comprehension and system-specification mining. The presentation will introduce temporal logic and motivate temporal-logic query checking as a tool for investigating system executions to uncover root causes for observed system behavior. It then outlines the techniques developed by UMD researchers to automate the solving of these queries. Preliminary experimental results of a prototype implementation are also given. This work is joint with Sam Huang.
Rance Cleaveland is a professor of computer science at the University of Maryland, where he also serves as the Associate Dean for Research at the College of Computer, Mathematical, & Natural Sciences. Additionally, he holds an appointment in the University of Maryland Institute for Advanced Computer Studies. Cleaveland is a Fellow of the IEEE and recently finished a four-year stint as Division Director of Computing and Communication Foundations at the National Science Foundation. He has published widely in the areas of software verification and validation, formal methods, model checking, software specification formalisms, and verification tools. Cleaveland received B.S. degrees in mathematics and computer science from Duke University, and M.S. and Ph.D. degrees in computer science from Cornell University.