Seminars

Proof-carrying code has been in existence since Necula and Lee coined the term in 1996. This talk brings forward the details of the development of proof-carrying code from control system specifications. The motivation for this work is the safety-critical nature of many control applications such as aeronautics, robot-assisted surgery, and ground transportation. Several challenges must be addressed during this effort, including: The formal representation of control-theoretic proofs; the migration and representation of these proofs across different layers of software implementation; and the…

Studies suggest that nearly all software errors are triggered by the interaction of no more than six parameters.  If so, testing all n-way combinations of parameters should provide high confidence that nearly all faults have been discovered.  This combinatorial testing is already used by dozens of companies.  Dr. Black will explain what combinatorial testing is and how to apply it to different situations.  Given 10 binary variables, can you exercise all triples with fewer than 20 tests?  He refers to free software available to generate such "covering arrays" for combinations of parameter…

Quality must be designed into and built into software.  Nevertheless testing (dynamic analysis) and static analyzers have roles in delivering excellent software.  Dr. Black will describe what static analysis is (and isn't) and compare it in general with testing.  Then he will talk about the dimensions of static analysis: universality, rigor, and subject matter, and concepts related to static analysis and their results.  Dr. Black will also share his views of the state of the art in static analyzers, citing results from the 2008, 2009, and 2010 Static Analysis Tool Expositions and other…

The artifacts of daily life are inexorably becoming more intelligent by means of embedded systems.  While this brings many advantages in terms of new functions, complexity is limiting progress.  Most UTRC activities in embedded and cyber-physical systems are focused on managing complexity in architectures and design processes in order to support emerging trends to increase functionality.  We will present some of these emerging trends and recent UTRC initiatives to address them, including the DARPA META II project involving MIT, UC Berkeley and UC Santa Barbara and the Autonomous and…

Computer security aims to ensure only "good" behavior happens in computer systems, despite potential action by malicious adversaries. Consequently, the field has focused primarily on the technology to prohibit "bad things," according to some set of rules, and to a lesser extent on the structure of such rules.  Interestingly, the computer security field has largely ignored the process by which humans produce these sets of rules; not surprisingly, fieldwork and anecdotes report how we keep getting the rules "wrong."

This talk presents some of my lab's research addressing this problem…