Formal Methods and Verification

Faculty

Clark Barrett   Patrick Cousot   Benjamin F. Goldberg  Thomas Wies

The long-term goal of the formal methods group is to increase the reliability of hardware and software systems by providing tools and techniques for the analysis of these systems. In formal analysis, a mathematical model of a system is developed, which can then be used to prove properties of the system or to discover bugs in the system when the proof fails. The activities and interests of the formal methods group cover a broad spectrum, from the study of mathematical foundations in temporal and first-order logic, to the implementation of verification tools such as TLV and CVC3, to the application of these tools for proving the correctness of embedded systems and compilers.

Clark Barrett's interests encompass both the theory and application of formal techniques. Theoretical interests include propositional and first-order logic, model and proof theory, and automated deduction. Professor Barrett is a pioneer in the emerging field of Satisfiability Modulo Theories (SMT), in which efficient propositional reasoning is combined with decision procedures for first-order theories to produce solvers that are both automatic and expressive. The flagship tool developed by the group is the SMT solver CVC3, which is used by researchers around the world.

Patrick Cousot is the founder of Abstract Interpretation, a theory of sound approximation of mathematical structures, in particular those involved in the behavior of computer systems. It allows the systematic derivation of sound methods and algorithms for approximating undecidable or highly complex problems in various areas of computer science (semantics, verification and proof, model-checking, static analysis, program transformation and optimization, typing, software steganography, etc.). Its main current application is on the safety and security of complex hardware and software computer systems.

Benjamin Goldberg works at the interface between programming languages, compilers, and verification. One of the directions of his work is to develop techniques for insuring correct compilation, that is, automatic methods for verifying that a compiler is producing executable code that is a correct translation of the source code. A related effort is the development of techniques for the automatic synthesis of correct executable code from high level requirements specifications, particularly in the area of embedded systems. Tools developed by the Translation Validation project were successfully applied to validate optimizations by widely used industrial compilers.

Thomas Wies research interests are in formal methods, verification, and programming languages. In particular, he is interested in the theory and development of tools that increase software productivity and assist software engineers in building reliable software. This includes tools for automated verification, automated error detection, and automated debugging. A central thrust of Professor Wies' research is the development of abstraction techniques for automated reasoning about complex data and control in modern software artifacts, such as heap-allocated data structures and concurrency.

Related Web Pages

Analysis of Computer Systems Group  


top | contact webmaster