Labs
Lab 1
In this lab, you will leverage Large Language Models (LLMs) to formalize natural language problems into Conjunctive Normal Form (CNF). You are required to parse these formulas and utilize the MiniSat C++ API to verify their satisfiability efficiently.
Lab 2
In this lab, you will integrate Symbolic Execution with Large Language Models (LLMs) to automate program verification and repair. You are required to implement MiniSEE, a symbolic execution engine that validates program assertions using the Z3 SMT solver. Finally, you are required to utilize an LLM to automatically repair the incorrect code.
Lab 3
In this lab, you need to use Dafny to formally verify real programs. Dafny is an imperative and functional compiled language and is widely used in formal verification.