Midwest Verification Day 2017

Kenneth McMillan (Microsoft Research) on Friday at 9:00 a.m.
Title:Compositional Testing
Abstract: While full formal proof of complex systems remains a challenge, formal methods can readily be applied in practice to improve the performance of testing in exposing design errors. A good example of this is compositional testing. In this methodology each component of a system is given a formal specification and it is proved formally that these specifications guarantee system-level correctness. The components are then rigorously tested against their formal specifications. This approach has the advantages of unit testing in covering component behaviors, while at the same time exposing all system-level errors to testing. Moreover, it can expose latent bugs in components that are not stimulated in the given system but may occur when the component is re-used in a different environment. This talk will cover the basics of compositional testing and discuss some industrial applications.

Biography: Ken McMillan is a principal researcher at Microsoft Research in Redmond, Washington. He works in formal verification, primarily in model checking for hardware and software. He holds a BS in electrical engineering from the University of Illinois at Urbana (1984), an MS in electrical engineering from Stanford (1986) and a Ph.D. in computer science from Carnegie Mellon (1992). He is the author of the book "Symbolic Model Checking", and the SMV symbolic model checking system. For his work in model checking, he has received the ACM doctoral dissertation award, the SRC technical excellence award, the ACM Paris Kannelakis award, the Alan Newell award from Carnegie Mellon and the Computer-aided Verification Conference award. He was formerly a member of the technical staff at AT&T Bell Laboratories and a fellow at Cadence research labs.

Raymond Richards (DARPA) on Saturday at 9:00 a.m.
Title: Design and Verification of System Cyber Resiliency
Abstract: This talk will begin with a short discussion of DARPA’s history, mission, and structure.
The state-of-the-art in systems engineering is very adept at engineering systems for a variety of non-functional properties. These properties include such things as reliability, durability, availability, etc. Colloquially, these properties, which include safety and performance, are known as the –ilities. Unfortunately, cyber properties are not included in the systems engineering domain. A new program at DARPA is looking to advance the state-of-the-art in formal methods technologies to allow systems to be designed for cyber resiliency. This talk will highlight the technical challenges and the approached being developed by the Cyber Assured Systems Engineering (CASE) program.

Biography: Dr. Raymond (“Ray”) Richards joined DARPA in January 2016. His research interests focus on high assurance software and systems.
Dr. Richards joined DARPA from Rockwell Collins Advanced Technology Center (ATC) where he led a research group focused on automated analysis, cyber, and information assurance. In this role he helped to foster the industrial use of formal methods verification to support security accreditations. He also served as the liaison to U.S. Government S&T funding agencies for Rockwell Collins. He has performed research in the formal modeling and analysis of high assurance systems. He led the software development for a high-assurance cross-domain guard, and the formal modeling and analysis effort of a real-time operating system, in support of a Common Criteria EAL6+ evaluation. Dr. Richards has over 20 years of experience in leading the development of state-of-the-art computer hardware, software and systems. Dr. Richards has experience in developing real-time software ranging from high fidelity ground vehicle simulators, to developing safety critical software for air transport category aircraft.
Dr. Richards holds an MBA degree, Ph.D. and M.S. degrees in Electrical and Computer Engineering, and a B.S. degree in Electrical Engineering, all from the University of Iowa. He has several publications in the area of formal methods/software security analysis and one patent.