Our Research

Our main research goal is to advance the art and practice of formal methods to ensure, by way of mathematical proofs, that code works as intended. Our preferred approach is to synthesize provably correct code from high-level formal specifications via refinement steps carried out by automated transformations. We also work on the analysis and verification of existing code. We develop formal models and validate them via formal proofs to promote clarity, increase confidence, and identify problems and fixes. We develop tools and we use them, along with tools developed by others, in a variety of application domains.

Another major research goal of ours is the automatic generation of high-performance planning and scheduling software.

General-Purpose Synthesis

We have developed general-purpose (i.e. not domain-specific) techniques and tools for synthesizing provably correct code from high-level formal specifications via refinement steps carried out by automated transformations. Our latest development is the APT toolkit, built on the ACL2 theorem prover.

We have applied our and others' synthesis and refinement techniques and tools to a variety of application domains, including blockchain, learning systems, adaptive systems, theorem proving, constraint solving, planning, network stacks, and garbage collection.

Domain-Specific Synthesis

We have developed techniques and tools for synthesizing code from higher-level domain-specific specifications. By taking advantage of the domain specificity, the synthesis process can be often made completely automatic.

Formal Analysis and Verification

We have developed techniques and tools to analyze and verify code.

We have applied our and others' analysis and verification techniques and tools to several application domains, including cryptography and Android apps.

Formal Modeling and Validation

We have developed, using our and others' tools, formal models in a variety of application domains, including blockchain, Android, Java, multi-level security, TCP/IP networking, and virtual Trusted Platform Modules. We have validated these models via formal proofs.

Security

Security is a major application areas of ours.

Planning and Scheduling

We have developed tools to automatically generate high-performance planning and scheduling software.

Machine Learning

We have applied machine learning tools to the software development process.