Computer Systems and Engineering Seminar Series

Prove If You Can, Test If You Cannot

Speaker:Dr. Rance Cleaveland
Date: Friday, October 20, 2017
Time: 12:00pm - 1:00pm
Location: 125 Hudson Hall, Duke
Lunch served at 11:45


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.


Rance Cleaveland is a Professor of Computer Science at the University of Maryland 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 is a co-founder of Reactive Systems, Inc., a company that makes model-based testing tools for embedded software, and a past recipient of National Young Investigator Awards from the National Science Foundation and the Office of Naval Research and the Alcoa Engineering Research Achievement prize from NCSU. He has also won undergraduate teaching awards from UMD and NCSU. He has published over 145 papers in the areas of software verification and validation, formal methods, cyber-physical systems, model checking, software and system specification formalisms, verification tools, and embedded-software testing. 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.

Hosted by:
Dr. Miroslav Pajic