Overview

This course covers advanced techniques for Software Verification (demonstrating that software meets is requirements) and Validation (demonstrating that software meets the expectations of the end-user). Verification techniques focus on automated deduction and testing. Topics related to automated deduction include applying tools that use industry-developed SMT-solvers like Microsoft’s Z3 to perform deep learning of a program’s behavior and automated checking of the discovered behavior against developer-friendly specifications with an underlying logic foundation. Testing topics include applying recently developed techniques for automated property-based testing and fuzzing. Automated deduction and testing concepts are presented in an integrated fashion. Validation techniques include the use of use-case notation, behavior diagrams, testing, and simulation to illustrate the systems behavior to end users so that they can confirm that the system achieves their intentions.

The course includes a significant project component in which students apply the techniques above to sections of medical device software, including the control software for an infant incubator and infusion pump. The tools used in the course have been developed in collaboration with industry partners on Department of Defense-related projects.

Time and Location

• MWF 11:30 - 12:20
• DUE 1116