Fakult?tskolloquium

Current formal methods focus on mathematical proof as a means for establishing that a system is correct with respect to a formal specification.  This perspective can limit the applicability of formal  methods, since the development of such proofs remains a very difficult task requiring specialized expertise, even with computer assistance.  This presentation argues that formal-specification approaches that support both proof and testing as V&V technologies can enhance the practical usefulness of formal methods.  It then describes an approach, called instrumentation-based verification, that is intended to realize this vision.  Examples from the automotive domain will be used to illustrate the application of the work.

Speaker:
Rance Cleaveland is Professor of Computer Science at the University of Maryland (UMD) at College Park. Prior to joining the UMD faculty in 2005, he held professorships at the State University of New York at Stony Brook and at North Carolina State University (NCSU). He also co-founded Reactive Systems, Inc., in 1999 to commercialize tools for model-based testing of embedded software. From 2005 to 2014 he was the Executive and Scientific Director of the Fraunhofer USA Center for Experimental and Software Engineering. He has received a number of awards for both his research and teaching over the years, and has published over 140 papers in the areas of software verification and validation, formal methods, model checking, software specification formalisms, verification tools, software testing, and software architecture. Cleaveland received B.S. degrees (summa cum laude) in Mathematics and Computer Science from Duke University in 1982 and M.S. and Ph.D. degrees from Cornell University in 1985 and 1987, respectively.