Professional Interests

Research Interests / Other CSCI Interests

Research Interests

Software plays an increasing role in the operation of critical systems. As these systems become more complex, ensuring software correctness becomes much more difficult. I am interested in automated formal techniques for precisely specifying, implementing, and verifying software. To support these activities, I have developed several translation and analysis tools to support formal reasoning and test case generation. I have significant experience in applying formal verification and auto-test generation techniques to production DO178B Level A and B avionics software development efforts.

I have 15 years experience in software development and analysis, including 10 years experience in Model-Based Development & safety-critical systems. Most of that time has been spent developing simulation, translation, testing, and formal analysis tools for Model-Based Development languages including Simulink, Stateflow, Lustre, and RSML-e. I have led successful formal verification projects on large industrial avionics models, including displays (Rockwell-Collins ADGS-2100 Window Manager), redundancy management and control allocation (AFRL CerTA FCS program) and autoland (AFRL CerTA CPD program). I was the lead developer of the Rockwell-Collins Gryphon tool suite, which can be used for compilation, test-case generation, and formal analysis of Simulink/Stateflow models. This tool suite has been used both for academic research and industrial verification projects.

I completed my PhD at the University of Minnesota in January, 2005.  As a graduate student, I worked in the Critical Systems Research Group ( CriSys ), where I helped design a synchronous language called Requirements State Machine Language without Events (RSML-e).  My Masters thesis provided the first complete formalization of RSML-e, written in the Z formalism. This formalization has formed the backbone of the RSML-e NIMBUS Simulator and translation tools from RSML-e to model checking and theorem proving tools.  My PhD dissertation re-formalized RSML-e using higher-order abstract syntax and structural operational semantics to create a provably-correct translator from RSML-e to a subset of C. 

Other CSCI Interests

I am very interested in a class of languages called Synchronous Languages that can be used to specify the behavior of process-control or reactive systems. Synchronous languages  have several useful properties for specification:

Because of their relative simplicity and these properties, synchronous languages have a straightforward tech-transfer path, and are being used in several industrial settings.  Notable commercial languages in this class include Simulink, SCADE , Esterel , and MatrixX

I am also interested in general purpose programming languages and software design. I have worked extensively with logic programming languages (λProlog), functional programming languages (Standard ML) and object-oriented languages (C++) and am familiar with many of the design patterns applicable to compilers and GUI applications. I am interested in improvements in the state of the practice both from new languages, and idioms for working with existing languages.

The views and opinions expressed in this page are strictly those of the page author.
The contents of this page have not been reviewed or approved by the University of Minnesota.