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, connecting formal methods with industrial software engineering experience at aicas.

• 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

Title	Authors	Source
Consistency Management of Virtual Single Underlying Model for Cyber-Physical Systems	Tianhai Liu, Shobit Singh, Mattias Ulbrich, Vitus Lüntzel, Shmuel Tyszberowicz, Bernhard Beckert.	Accepted for the Spring School on Engineering Trustworthy Software Systems (SETSS) 2026 proceedings.
Keeping Models and Code in Sync: Roundtrip Engineering for Tactical Domain-Driven Design	Weixing Zhang, Mario Herb, Wai Chung Dorothy Cheng, Michael Wagner, Bowen Jiang, Tianhai Liu, Anne Koziolek.	Preprint, 2026. arXiv:2608.05612

Peer-reviewed Journal and Conference Papers

2027

Title	Authors	Source
Realisability-Driven Repair of Natural-Language Requirements via Neuro-Symbolic Reasoning	Tianhai Liu, Andreas Bremer, Ivan Panov, Alexander Weigl, Shmuel Tyszberowicz, Bernhard Beckert.	ISoLA 2026 · X-by-Construction Meets Intersymbolic AI, LNCS 17144, 55–75, Springer, 2027. DOI

2026

Title	Authors	Source
Analyses as First-Class Citizens in Model-Driven Development	Tianhai Liu, Shmuel Tyszberowicz, Bernhard Beckert.	FASE 2026, LNCS 16504, 180–201. DOI
Observable Consistency Checking across Requirements and Models	Tianhai Liu, Shmuel Tyszberowicz, Bernhard Beckert.	ENASE 2026, vol. 1, 50–63. DOI KITopen Best Paper Award
Can Formal Specifications Be Synthesized from Tests Alone?	Tianhai Liu, Maximilian Müller, Tobias Hey, Vitus Lüntzel, Muhammad Minhas, Anne Koziolek, Bernhard Beckert.	ASE 2026 · New Ideas and Emerging Results, 4575–4579. DOI arXiv
CANcept: Model-based CAN Traffic Generation and Manipulation	Lino Wertz, Junes Sheikhi, Florian Fehrle, Adrian Rupp, Tianhai Liu, Philipp Kern, Carsten Sinz, Bernhard Beckert.	MODELS 2026 · Tools and Demonstrations, 214–218. DOI
A Unified Model-Driven Framework for Co-Designing System Architecture and Safety Analysis in Cyber-Physical Systems	Muhammad Asim Minhas, Erik Burger, Ralf Reussner, Tianhai Liu.	Journal of Object Technology 25(3), 3:211–224 · ECMFA 2026. DOI
Forging Robust Building Blocks for Next-Gen RISC-V Chips: Virtual Repository and IP Card	Cătălin Bogdan Ciobanu et al. (including Tianhai Liu).	DSD 2026, 423–430. DOI

2023

Title	Authors	Source
TEASER: Simulation-Based CAN Bus Regression Testing for Self-Driving Cars Software	Christian Birchler, Cyrill Rohrbach, Hyeongkyun Kim, Alessio Gambi, Tianhai Liu, Jens Horneber, Timo Kehrer, Sebastiano Panichella.	ASE 2023, 2058–2061. DOI arXiv

2017

Title	Authors	Source
Computing Exact Loop Bounds for Bounded Program Verification	Tianhai Liu, Shmuel S. Tyszberowicz, Bernhard Beckert, Mana Taghdiri.	SETTA 2017, 147–163. DOI

2016

Title	Authors	Source
Computing Specification-Sensitive Abstractions for Program Verification	Tianhai Liu, Shmuel S. Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl, Mana Taghdiri.	SETTA 2016, 101–117. DOI

2014

Title	Authors	Source
A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution	Tianhai Liu, Mateus Araújo, Marcelo d'Amorim, Mana Taghdiri.	HVC 2014, 284–299. DOI
Generating JML Specifications from Alloy Expressions	Daniel Grunwald, Christoph Gladisch, Tianhai Liu, Mana Taghdiri, Shmuel S. Tyszberowicz.	HVC 2014, 99–115. DOI

2012

Title	Authors	Source
Bounded Program Verification Using an SMT Solver: A Case Study	Tianhai Liu, Michael Nagel, Mana Taghdiri.	ICST 2012, 101–110. DOI

Posters

Title	Authors	Source
Bringing Cloud-Connected Automotive Workloads to RISC-V: A CVA6-Based FPGA Case Study	Tianhai Liu, James J. Hunt, Holger Blasum, Darshak Sheladiya.	RISC-V Summit Europe 2026, Bologna · Poster. KITopen DOI
FPGA Lifecycle Management for RISC-V Systems	Tianhai Liu, James J. Hunt.	RISC-V Summit Europe 2026, Bologna · Poster. KITopen DOI arXiv

Doctoral Dissertation

Title	Authors	Source
Efficient Verification of Programs with Complex Data Structures Using SMT Solvers	Tianhai Liu.	Doctoral dissertation, Karlsruhe Institute of Technology, 2018. DOI

Selected Research Projects

• CoNVIDe · SFB 1608 · C03 since 2025 · KIT · DFG

  Technical lead for C03 activities in Prof. Beckert’s group: consistency-enabled incremental recertification of cyber-physical systems.

• TRISTAN 2022–2026 · aicas · Horizon Europe

  Work-package lead at aicas: automotive workloads on RISC-V platforms, cloud–edge integration, and FPGA lifecycle management.

• COSMOS 2021–2024 · aicas · Horizon 2020

  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.

Course overview Thesis topics

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).