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.

  • APT — Automated program transformations for general-purpose synthesis and analysis.
  • ATC - Verified C code generation from the ACL2 theorem prover.
  • ATJ - Java code generation from the ACL2 theorem prover.
  • DTRE — Data Type Refinement Environment.
  • EDCS — Evolution based on precise semantic design records.
  • Hyperproperties — Hyperproperty-preserving program refinement.
  • KIDS — Automated support for the development of correct and efficient programs from formal specifications.
  • MIDAS - Integration of model-based development with formal program synthesis for improved adaptability.
  • Specware — Category-theoretic transformation-based general-purpose synthesis.

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.

  • ACL2 Ethereum — Formally specifying and implementing an Ethereum client using the ACL2 theorem prover and the APT toolkit.
  • CASE — Scalable and explainable inference via specialization of Flex, a formally derived prover/solver.
  • Constraintware — Synthesis of high-performance constraint solvers.
  • CRASH — Synthesis of concurrent garbage collectors.
  • Diversity — Using software generation and repair for cyber-defense.
  • HACMS — High-assurance TCP/IP protocol stack.
  • Java — Formal modeling, proofs, and synthesis of a Java bytecode verifier.
  • JCRE — Formal modeling, proofs, and synthesis of an embedded smart card operating system.
  • TRS — Making trusted systems resilient via formal re-synthesis from updated specifications.
  • vTPM — Formal modeling, proofs, and synthesis of a virtual Trusted Platform Module.

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.

  • AutoSmart — Automatic generation of high-assurance smart card applications.
  • PDA — A security protocol derivation assistant.
  • Planware — Domain-specific planning and scheduling.

Formal Analysis and Verification

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

  • APT — Automated program transformations for general-purpose synthesis and analysis.
  • Axe — A toolkit for program verification and analysis, including a rewriter, theorem prover, equivalence checker, and lifters from imperative code into logic.
  • CASE — Scalable and explainable inference via specialization of Flex, a formally derived prover/solver.

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

  • APAC — Sound static analysis of Android apps, to exclude malware.
  • DerivationMiner — Mining formal stepwise refinement derivations.

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.

  • Formal Verification of R1CS — Lifting R1CS (Rank 1 Constraint Systems) into logic, and proving them equivalent to specifications written in the ACL2 theorem prover.
  • ACL2 Ethereum — Formally specifying and implementing an Ethereum client using the ACL2 theorem prover and the APT toolkit.
  • F6 — Design and formal verification of a multi-level secure, fault-tolerant software platform for fractionated satellites.
  • Java — Formal modeling, proofs, and synthesis of a Java bytecode verifier.
  • JCRE — Formal modeling, proofs, and synthesis of an embedded smart card operating system.
  • vTPM — Formal modeling, proofs, and synthesis of a virtual Trusted Platform Module.

Security

Security is a major application areas of ours.

  • ACL2 Ethereum — Formally specifying and implementing an Ethereum client using the ACL2 theorem prover and the APT toolkit.
  • APAC — Sound static analysis of Android apps, to exclude malware.
  • AutoSmart — Automatic generation of high-assurance smart card applications.
  • F6 — Design and formal verification of a multi-level secure, fault-tolerant software platform for fractionated satellites.
  • Hyperproperties — Hyperproperty-preserving program refinement.
  • Java — Formal modeling, proofs, and synthesis of a Java bytecode verifier.
  • JCRE — Formal modeling, proofs, and synthesis of an embedded smart card operating system.
  • PDA — A security protocol derivation assistant.
  • VIBRANCE — Automatic removal of security vulnerabilities from Java applications.
  • vTPM — Formal modeling, proofs, and synthesis of a virtual Trusted Platform Module.

Planning and Scheduling

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

  • Planware — Domain-specific planning and scheduling.

Machine Learning

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