Researches decidability and computability and builds tools for automated theorem proving.
|
This project develops algorithms for performing abstract interpretation over new abstract domains whose elements are logical formulas over some theory and the partial order relationship is the implication relationship. Theorem proving community has studied decision procedures for several theories. For performing abstract interpretation over logical formulas in a theory, we need more than a decision procedure. For example, we need a join algorithm that can over-approximation disjunction, and a widen algorithm that guarantees convergence during the fixed-point computation process. |
|
|
These days not too many people worry about foundations of mathematics which is a compliment of sorts: the foundations are solid. Computer science is younger, and its foundations are still work in progress. Logic and Foundations is really a meta-project. Here are some parts in alphabetical order: Abstract State Machines and Behavioral Computation Theory; Database theory; Decision problems and Computational Complexity; Logic and Model Theory, in particular Finite Model Theory; Security; Specification and Testing. |
|
|
We investigate various foundational questions and study decision problems related to reasoning about high-level models that use rich data types or combinations of different theories. |
|
|
SMT Solvers (or Theorem Provers) have traditionally been used for verifying correctness of systems that have been annotated with relevant inductive invariants. Such an annotation usually is an undesirable burden on the user. This project explores techniques for using SMT solvers to automatically discover inductive invariants for proving given safety properties of systems. Additionally, this project also explores techniques for using SMT solvers to synthesize systems in the first place given enough specifications. |
|
|
Z3 is a new high-performance theorem prover for first rorder logic. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 has been integrated with Spec#/Boogie, Pex, Yogi, Vigilante, SAGE, SLAM, HAVOC, SPEED, and SV3. It can read problems in SMT-LIB and Simplify formats. |
|
