Formal Methods
Overview:
Our research involves the use of mathematics to assist with the specification, design, implementation, and verification of computing systems.
Faculty:
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:
- About Us
- Research
- Faculty
- Awards & Honors
- Undergraduate Program
- CS Degrees
- For Non-CS majors
- Courses
- Advising
- Undergraduate Research
- Honors Programs
- Interdisciplinary Study & Certificate Programs
- Study Abroad
- Jobs & Internships
- Scholarships
- Prospective Students
- Why Study CS?
- Where to Study Computing at UT
- K - 12: Get Started Now
- Apply to CS from High School
- Apply to Turing Scholars from High School
- Freshman Research Initiative
- Transfer to UT CS from Another University
- Transfer to CS from Another UT Major
- Apply for Admission to CS from Entry-Level CS
- Schedule a Visit
- Student Life & Organizations
- Demographics
- Alumni
- Forms
- Code of Conduct
- Graduate Program
- Giving & Collaboration
- Careers
- Outreach
- Alumni
- UTCS Direct
