COLLOQUIUM Department of Computer Science and Engineering University of South Carolina Automatic Abstraction for Model Checking Software Specifications with Interrelated Numeric Constraints Yunja Choi Department of Computer Science and Engineering University of Minnesota Date: February 7, 2003 (Friday) Time: 3:30-4:30PM Place: Swearingen 1A03 (Faculty Lounge) Abstract Model checking techniques have not been effective in important classes of software systems characterized by large (or infinite) input domains with interrelated linear and non-linear constraints over the input variables. To address this issue, I have proposed the domain reduction abstraction technique based on data equivalence and trajectory reduction as an alternative and complement to other abstraction techniques. The technique applies the abstraction to the input domain (environment) instead of the model and is applicable to constraint-free and deterministic constrained data transition system with a possible extension to limited non-determinism. The abstraction technique is implemented as an extension of the symbolic model checker NuSMV, which is used as a back-end verification tool in our specification-centered software development framework. Results on avionics systems applications show that the approach is promising. Yunja Choi received the B.S. and M.S. degree in Mathematics from Yonsei University in Seoul, Korea in 1991 and 1993, and the M.S. degree in Computer Science from the University of Minnesota in 1999, where she expect to receive the Ph.D. degree in Computer Science in May 2003. Ms. Choi worked as a software engineer for Samsung Data Systems in Seoul, Korea, from 1993 to 1996 and as an intern at Medtronics, Inc. during her Ph.D. studies. Her research interests lie in formal methods in software engineering, including tool support for automated verification framework and adaptation of model checking technique to software verification.