In modern society, people regularly use smartphones and computers in daily life and work, while computer-controlled infrastructure such as transportation, finance, healthcare, and energy plays a vital role behind the scenes. Ensuring the reliability and efficiency of the software that controls these systems is essential for social stability and smooth operation. 

Our laboratory studies techniques for building highly reliable and efficient software based on foundational theories such as formal logic and program theory. We focus on program verification, which mathematically guarantees that a program meets its specification, and program synthesis, which generates programs from specifications. In particular, we are integrating verification and synthesis tools into the functional programming language OCaml to support the development of reliable and efficient programs. We are also developing solvers such as PCSat, MuVal, MuCyc, and MuStrat that express and solve verification and synthesis problems as predicate constraints or fixed-point logical formulas. In addition, we study the theoretical foundations of these tools, including program theory, type theory, constraint solving, optimization theory, fixed-point logic, and its deductive systems.