This talk is about static analysis of low-level C codes such as those that run on the billions of microcontrollers sold each year. Static analysis is a key building block for technologies such as optimizing compilers and automated formal methods. Our analysis framework has two parts. First, it conservatively classifies variables (e.g. as "volatile but consistently protected by locks") using a collection of cooperating analyses. Second, it performs dataflow analysis based on the classification of variables combined with knowledge of the hardware and software environment. Novel aspects of this framework include strategies for performing dataflow in the presence of interrupt-driven concurrency, for flowing data through some kinds of volatile locations, and for pruning edges from the control flow graph by exploiting knowledge of asynchronous causality relationships in the code. Our framework handles generic C code but is tuned to give good results for sensor network applications running on TinyOS.
Bio: John Regehr is an assistant professor at the University of Utah's School of Computing. His work centers around creating software tools that make it easier to create high-quality embedded software.
| John Regehr |
| School of Computing, University of Utah |
| Date: | Mon Nov 5 2007 |
| Time: | 14:00 to 15:00 |
| Location: | Level 1 Seminar Room, NICTA Kensington (L5) |
| Convened by: | Gerwin Klein |
| Materials: |
Last updated by tbourke at Mon Nov 19 09:56:13 2007 GMT+1100