In modern society, people regularly use smartphones and computers in their personal lives and work, and unnoticed, computer-controlled infrastructure such as transportation, finance, healthcare, and energy plays a crucial role. Therefore, ensuring the reliability of software that controls computers and improving its efficiency are important challenges for maintaining social stability and smooth functioning. In our laboratory, we research techniques to construct highly reliable and efficient software, based on foundational theories like formal logic and program theory.

• June 2026. The paper “A Hierarchy of Supermartingales for ω-Regular Verification” by Professor Hiroshi Unno et al. was presented at PLDI 2026.
• June 2026. The paper “Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification” by Professor Hiroshi Unno et al. was presented at PLDI 2026.
• May 2026. Professor Hiroshi Unno gave a keynote talk at ISMVL 2026.
• April 2026. We participated in CHC-COMP 2026 with PCSat and MuCyc, two CHC solvers developed in our laboratory.
• April 2026. The paper “A Category-Theoretic Framework for Dependent Effect Systems” by Professor Hiroshi Unno et al. was presented at ESOP 2026.
• March 2026. Takuma Monma and Kazuki Uehara have presented posters about their research at PPL 2026.
• November 2025. The paper “AP-observation Automata for Abstraction-based Verification of Continuous-time Systems” by Assistant Professor Clovis Eberhart et al. was presented at ICTAC 2025.
• October 2025. The paper “On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs” by Professor Hiroshi Unno et al. was presented at OOPSLA 2025.
• October 2025. Takuma Monma, Kazuki Uehara, and Assistant Professor Clovis Eberhart presented a demonstration at the RIEC Open House 2025.
• September 2025. MuVal, a verification tool developed in our laboratory, won the C category at Termination Competition 2024.
• June 2025. The paper “Thrust: A Prophecy-based Refinement Type System for Rust” by Professor Hiroshi Unno et al. was presented at PLDI 2025.
• May 2025. Professor Hiroshi Unno gave an invited lecture at EPIT 2025.
• May 2025. Professor Hiroshi Unno gave an invited talk at a "CHoCoLa" meeting.
• May 2025. Assistant Professor Clovis Eberhart has joined our laboratory.
• April 2025. We participated in CHC-COMP 2025 with PCSat and MuCyc, two CHC solvers developed in our laboratory.
• April 2025. Professor Hiroshi Unno's project, “Foundations and Applications of Program Verification Techniques,” has been selected for funding under the KAKENHI Grant-in-Aid for Scientific Research (S).
• February 2025. The paper “Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking” by Professor Hiroshi Unno et al. was presented at AAAI 2025.
• January 2025. The paper “A Primal-Dual Perspective on Program Verification Algorithms” by Professor Hiroshi Unno et al. received a Distinguished Paper Award at POPL 2025.
• January 2025. The paper “A Primal-Dual Perspective on Program Verification Algorithms” by Professor Hiroshi Unno et al. was presented at POPL 2025.
• January 2025. The paper “Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs” by Professor Hiroshi Unno et al. was presented at POPL 2025.
• October 2024. The paper “Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification” by Professor Hiroshi Unno et al. was presented at OOPSLA 2024.
• September 2024. The paper “Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System” by Professor Hiroshi Unno et al. was presented at ICFP 2024.
• July 2024. MuVal, a verification tool developed in our laboratory, won the Integer Transition Systems category at Termination Competition 2024.
• June 2024. The paper “Inductive Approach to Spacer” by Professor Hiroshi Unno et al. was presented at PLDI 2024.
• April 2024. Professor Hiroshi Unno joined Tohoku University and started the Software Construction Laboratory.

Software and hardware bugs can be a source of

• financial trouble (an attack on the Ethereum DAO stole fifty million dollars),
• social unrest (a routing misconfiguration taking KDDI's network down for two days, Heartbleed vulnerability exposes history of OpenSSL encrypted messages), and even
• human loss (Therac-25 radiation therapy machine sends lethal doses to patients).

The most common way to write bug-free code is to adhere to a set of “good practices” that reduce the chance of writing bugs, such as writing modular code, writing clear documentation, implementing thorough code reviews, or writing good test suites. However, these methods only reduce the chance of writing bugs, but they cannot guarantee the absence of undiscovered bugs. The goal of formal verification is, given

• a system (for example a computer program or a model of a physical object)
• and a formal specification, i.e., an unambiguous description of desired behaviours,

to automatically determine whether the system behaves according to the specification. Depending on the types of systems and specifications, it may rely on tools such as formal logic, type systems, semantics of programming languages, or automata theory.

Verification can ensure that software that has already been written contains no bugs. However, in case there are bugs in the software, most verification methods do not explain where the bug is or how to solve it (which are the fields of fault localization). Another way to ensure that there are no bugs in software is to create software in such a way that there cannot be bugs, which is sometimes called “correct-by-design” or “correct-by-construction”. This is the field of program synthesis, which is close to formal verification and relies mostly on the same tools, but whose goal is slightly different. Here, given a formal specification (but no system), the goal is to automatically create a system that behaves according to this specification.

One possible way to prove absence of bugs in programs is to use type systems. The intuition is conveyed in Robin Milner's famous statement.

Well-typed programs cannot go wrong.

In traditional type systems (such as those of ML), this statement can be formalised as two theorems: the progress theorem, which states that typed programs are not stuck, and the preservation theorem, which states that typed programs evaluate to programs of the same type.

A common approach to automated formal verification is model checking. In this approach, the system is translated to some sort of finite-state transition system, usually an automaton, whose language describes exactly the behaviours of the system. Similarly, the specification is translated to some automaton whose language describe exactly intended behaviours. A method to solve formal verification is then to check that all system behaviours are intended by checking whether the language of the system's automaton is included in that of the specification's automaton using automata-theoretic techniques.

This approach can also be used to solve some forms of synthesis, such as controller synthesis. In controller synthesis, the idea is that we have a system (for example a robot), and we want to synthesise a program that will control the robot to behave according to the specification. Depending on the kind of specifications, the controller can be constrained to be a simple program (for example, a memoryless controller, which only gives inputs depending on the current state of the system). In this case too, the system and specification are translated to automata, but here, we are not interested in language inclusion. Instead, a classic approach to take a product of the automata to create a mathematical game whose winning strategies can be turned into controllers that satisfy the specification.

Another approach to automated formal verification is deductive verification, where constraints are derived from the program and its specification, and solved to check whether the program satisfies its specification. Fixpoint Logics, whose formulas contain least and greatest fixed points, are a family of logics that can be used to derive these constraints. The basic idea here is that, for many different semantics, the semantics of program loops can be encoded as the least fixed point of some operator, so computing the semantics of a program results in computing a least fixed point. Depending on the problem we want to solve, the problem can be translated to a problem in fixpoint logic, such as finding lower and upper bounds for a fixed point equation. One approach to automate these problems is to use templates. For example, when trying to find lower or upper bounds, the template approach consists in assuming that the bounds have a given shape prescribed by the template (for example, that it is a polynomial of fixed degree). This creates constraints on the shape of the bound (for example, constraints on the coefficients of the polynomial), so searching for a bound turns into a constraint-solving problem.

There are several ways to solve the constraints introduced in deductive verification. One way is to use proof assistants, which allows humans to write computer-checked formal proofs. This method can be used to solve basically any kind of constraint as it relies on human ingenuity, but it is not automated. Another way is to use solvers written specifically to solve constraints of a given shape, such as Satisfiability (SAT) solvers and Satisfiability Modulo Theory (SMT) solvers. They are software that are written to be highly efficient in dealing with specific problems. SAT solvers are designed to solve the satisfiability problem on Boolean formulas, that is to know whether it is possible to find an assignment of Boolean variables that makes the formula true. SMT solvers are also designed to solve the satisfiability problem, but on predicate logic formulas, that is to know whether there is an assignment of term and predicate variables that makes the formula true.

The laboratory is situated in the Research Institute of Electrical Communication. We are on the 5th floor. Rooms M518 and M519 are occupied by researchers, while room M536 and M537 are occupied by students. Room M522 is used for reading groups and seminars.

• Tohoku University
• Research Institute of Electrical Communication