Our research involves the use of mathematics to assist with the specification, design, implementation, and verification of computing systems.

Topics:

• Declarative Programming:
  • Declarative approaches to search. Nonmonotonic logic. Stable models. Semantics of answer set programming languages. Answer set solvers.
• Concurrency:
  • Theory of concurrency and causality, Language for distributed and concurrent programming, Process algebra.
• Hardware and Software Verification:
  • Microprocessor ISA specification. Microcode verification. Floating-point verification. Binary code analysis. Number theory and metamathematics.
• Model Checking:
  • Property checking. Predicate abstraction. Automatic verification. Reachability. State-space exploration.
• Security:
  • Model checking. Constraint solving. Computational soundness.
• Theorem Proving:
  • Rewriting. Rule-driven simplification. Decision and semi-decision procedures. Heuristic proof techniques. Induction. Integrated proof techniques. Domain-specific proof techniques. Metafunctions. Search. Interactive guidance. Proof development environments.

Courses:

• CS 389R Recursion and Induction

Research Groups:

• The Mechanized Theorem Proving Group