Research

Formally verifying that a system conforms to a specification is a challenging problem in computer science. It is so challenging, that there are instances of the problem that are classified as undecidable. Yet, over the past two decades this field of research has seen great advancements.

News!

Our paper "Property Directed Reachability with Extended Resolution" was accepted to CAV 2025. The paper suggests a model checking algorithm that uses a strong proof system (Extended Resolution) efficiently. The final version will be made available soon. If you would like to know more, feel free to contact us.

Here are some of the topics the group is working on:

1. 1. 1. Core model checking algorithms for both hardware and software systems.
      2. Proof systems and model checking.
      3. Using Constrained Horn Clauses (CHCs) in verification.
      4. Proofs from SAT and SMT solvers.
      5. Abstraction techniques.
      6. Using LLMs to improve formal verification.