Keynote Speakers

Rance Cleaveland (University of Maryland) on Friday at 11:00am
Title: “Prove if you can, test if you cannot” (abstract)
Biography: Rance Cleaveland is Professor of Computer Science at the University of Maryland (UMD) at College Park, where he also served formerly as Executive and Scientific Director of the Fraunhofer USA Center for Experimental and Software Engineering. 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. In 1992 he received Young Investigator Awards from the US National Science Foundation and from the Office of Naval Research; in 1994 he was awarded the Alcoa Engineering Research Achievement prize at North Carolina State University; and in 1991 and 2011 he received teaching awards from NCSU and UMD, respectively. He 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.

David Greve (Rockwell Collins) on Saturday at 8:30am.
Title: “Analyzing Information Flow Properties of C Programs” (abstract)
Biography: David Greve is a Principal Engineer in the Advanced Technology Center at Rockwell Collins specializing in the construction and analysis of formal models of computing systems. David was instrumental in the formal analysis of the Rockwell Collins AAMP7 intrinsic partitioning mechanism and the Green Hills INTEGRITY-178B operating system in support of their respective MILS/Common Criteria certifications. As part of these efforts he helped formalize a useful notion of information flow in both the ACL2 and PVS theorem proving systems. His most recent work in this area has focused on the development of Data Flow Logic (DFL), a domain specific language for specifying and verifying information flow properties of software written in C. David received his Master’s degree in Electrical Engineering from the University of Illinois in 1992.