Formal Methods · Software Engineering
Tianhai Liu
Postdoctoral Researcher · Dr. rer. nat.
Karlsruhe Institute of Technology (KIT)
KASTEL – Institute of Information Security and Dependability
tianhai.liu@kit.edu
+49 721 608-43856
Room 227, Building 50.34
Am Fasanengarten 5, 76131 Karlsruhe
Germany
Research
My research focuses on keeping software systems verifiable as they evolve. I work on consistency across requirements, models, and code, and on incremental verification and recertification of cyber-physical systems. At KIT, I contribute to CoNVIDe (CRC/SFB 1608), project C03. At aicas, I lead contributions to European research projects, with expertise spanning real-time systems, modular software architectures, IoT and cloud–edge platforms, and FPGA-based RISC-V systems.
- Incremental verification and recertification
- Consistency management in model-driven engineering
- AI-assisted requirements formalisation and specification synthesis
- SMT-based program analysis and continuous verification
Publications
Accepted Work and Preprints
- TRISTAN and ISOLDE: European Pathways to High-Performance RISC-V Systems
- Consistency Management of Virtual Single Underlying Model for Cyber-Physical Systems
- Keeping Models and Code in Sync: Roundtrip Engineering for Tactical Domain-Driven Design
Peer-reviewed Journal and Conference Papers
2027
- Realisability-Driven Repair of Natural-Language Requirements via Neuro-Symbolic Reasoning
2026
- Analyses as First-Class Citizens in Model-Driven Development
- Observable Consistency Checking across Requirements and Models
- Can Formal Specifications Be Synthesized from Tests Alone?
- CANcept: Model-based CAN Traffic Generation and Manipulation
- A Unified Model-Driven Framework for Co-Designing System Architecture and Safety Analysis in Cyber-Physical Systems
- Forging Robust Building Blocks for Next-Gen RISC-V Chips: Virtual Repository and IP Card
2023
- TEASER: Simulation-Based CAN Bus Regression Testing for Self-Driving Cars Software
2017
- Computing Exact Loop Bounds for Bounded Program Verification
2016
- Computing Specification-Sensitive Abstractions for Program Verification
2014
- A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution
- Generating JML Specifications from Alloy Expressions
2012
- Bounded Program Verification Using an SMT Solver: A Case Study
Posters
- Bringing Cloud-Connected Automotive Workloads to RISC-V: A CVA6-Based FPGA Case Study
- FPGA Lifecycle Management for RISC-V Systems
Doctoral Dissertation
- Efficient Verification of Programs with Complex Data Structures Using SMT Solvers
Selected Research Projects
-
Technical lead for C03 activities in Prof. Beckert’s group: consistency-enabled incremental recertification of cyber-physical systems.
-
Work-package lead at aicas: automotive workloads on RISC-V platforms, cloud–edge integration, and FPGA lifecycle management.
-
Work-package lead at aicas: DevOps workflows and X-in-the-Loop testing for automotive software.
Teaching and Supervision
At KIT, I contribute to teaching Formal Systems, Formal Systems II, Formal Methods in Software Engineering, and Practical Software Engineering, with responsibility for selected teaching units, student supervision, and assessment. I supervise bachelor’s and master’s theses in formal verification, software analysis, and model-driven engineering.
Invited lecture: Semantic Consistency in Model-Driven Development, SETSS 2026, Southwest University, Chongqing.
Student Projects
If you are interested in a thesis related to my research, please get in touch by email.
Academic Service
2026 · Program committee: SETSS. Artifact evaluation committees: FM, ICFP, TACAS.
Background
- Postdoctoral Researcher, KIT / KASTEL
since August 2025 - Project Lead and Senior Software Engineer, aicas GmbH
since August 2016
Education
Dr. rer. nat. in Computer Science, KIT (2018); Master of Computer Science, TU Dresden (2010); Bachelor of Engineering, Chongqing University (2006).