Tianhai Liu, Dr. rer. nat.

Researcher
Room 227, Building 50.34
Phone: +49 721 608-43856
Fax:      +49 721 608-44021
tianhai.liuXwx3∂kit.edu
 KIT / Institute of Information Security and Dependability (KASTEL)

Am Fasanengarten 5
Building 50.34
76131 Karlsruhe
Germany

Research Interests

  • Formal methods and software verification
  • Cyber-physical systems
  • OSGi-based modular IoT architectures
  • FPGA-cloud-edge integration
  • DevOps/MLOps pipelines for continuous verification
  • AI-assisted software engineering

Projects

TRISTAN (12/2022 – 06/2026)
Role: Project Lead for work packages – Integration and evaluation of RISC-V edge computing with cloud for the automotive domain, aicas GmbH Together for RISC-V Technology and ApplicatioNs (Horizon Europe Project). A collaborative project with 44 universities and consortium partners to expand and develop RISC-V architecture. Focus on seamless integration of edge computing solutions with cloud infrastructure for safety-critical automotive applications.

EU Contribution: € 15,430,543.81 → Project Website
COSMOS (01/2021 – 03/2024)
Role: Project Lead for work packages – Development and integration of DevOps technologies for automotive software development pipeline with X-in-the-Loop simulation, aicas GmbH DevOps for Complex Cyber-physical Systems (Horizon Europe Project). A collaborative project with 12 universities to develop modern DevOps solutions for CPS. Focus on continuous integration and deployment pipelines with Model-in-the-Loop (MIL), Software-in-the-Loop (SIL), Hardware-in-the-Loop (HIL), and Vehicle-in-the-Loop (VIL) testing for the automotive industry.

EU Contribution: € 4,998,571.25 → Project Website
EMC2 (10/2016 – 06/2017)
Role: Research and Development Engineer, aicas GmbH Embedded Multi-Core Systems for Mixed Criticality Applications (Horizon Europe Project). Large-scale project involving 102 organizations to develop multi-core platforms for safety-critical embedded systems.

EU Contribution: € 15,588,761.02 → Project Website
RS3 (01/2016 – 07/2018)
Role: Software Engineer at aicas GmbH, meanwhile work on Ph.D. thesis at KIT Reliably Secure Software Systems (DFG Project). Development of semantic-based certification and analysis tools for safety-critical software systems. → Project Website
Reliable Software Evolution (01/2013 – 06/2015)
Role: PhD Student, KIT German Israeli Foundation Project. Development of formal methods to ensure the reliability of evolving software systems using verification techniques. → Project Website
Analysis of Data Structure Properties in Large Programs (01/2011 – 12/2014)
Role: PhD Student, KIT DFG Project. Advanced static program analysis for large and complex programs using SMT solvers to verify complex data structures. → Project Website

Experience

  • 08/2025 – Present: Postdoc, Karlsruhe Institute of Technology (KIT), Germany
    Project CoNVIDe, Work Package C03: Consistency-Enabled Incremental Quality Analysis of CPS [SFB 1608]
  • 08/2016 – Present: Project Lead and Senior Software Engineer, aicas GmbH, Karlsruhe, Germany
  • 02/2011 – 07/2018: Research Associate (Ph.D. Student), Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany
  • 09/2010 – 02/2011: Research Assistant, TU Darmstadt, Darmstadt, Germany
  • 05/2009 – 03/2010: IBM Research & Development, Böblingen, Germany

Publications

2026

  • Tianhai Liu, Maximilian Müller, Tobias Hey, Vitus Lüntzel, Muhammad Minhas, Anne Koziolek, Bernhard Beckert: Can Formal Specifications Be Synthesized from Tests Alone? Accepted at IEEE/ACM International Conference on Automated Software Engineering, New Ideas and Emerging Results Track (ASE NIER) 2026, 2026.
  • Catalin Bogdan Ciobanu, Francesco Conti, Cairo Caplan, Holger Schmidt, Wolfgang Ecker, Rob Wullems, Patrick Pype, Tiberio Fanti, Davide Schiavone, Dominik Baumann, Alexandru Pușcașu, Răzvan Stancu, Octavian Buiu, Sven Mehlhop, Jörg Walter, Frank Oppenheimer, Gianvito Urgese, Teodoro Urso, Reoberto Bosio, Alessio Burrello, George Suciu, Mari-Anais Sachian, Nicoleta Capbun, Robert Florescu, Simona Costinescu, Ambily Suresh, Florian Lorber, Honorius Galmeanu, Mihai Munteanu, Szilard Hegedus, Darshak Sheladiya, Florian Krebs, Henrik Theiling, Mattia Paladino, Daniele Gregori, Federico Proverbio, Jan Kastil, Alexander Schober, Rainer Buchty, Mladen Berekovic, Amrit Sharma Poudel, Saleh Mulhem, Emanuele Valpreda, Andrea Zunino, Luigi Feola, Samuel Matea, Cosmin Moisa, Perian Cristian, Andrei Stan, Alexandru-Tudor Popovici, Cosmin-Andrei Popovici, George-Emil Vieriu, Daniel Gracia Pérez, Sylvain Girbal, Jérôme Quèvremont, André Sintzoff, Fatma Jebali, Caaliph Andriamisaina, Florian Egert, Maurizio Capra, Valerio Venceslai, Francesco De Maldé, Maria Elena D'Agostino, Gabriele Magnani, Davide Baroffio, Andrea Galimberti, Carlo Brandolese, Costin-Emanuel Vasile, Radu Hobincu, Alexandra-Mihaela Enescu, Calin Bira, Elijah Seth Cishugi, Marco Ottavi, Esther Soriano-Viguer, Ester Lopez-Mora, Vicente Nicolau-Gallego, Odysseas Chatzopoulos, Vasileios Karakostas, Dimitris Gizopoulos, Konstantinos Georgopoulos, Ioannis Papaefstathiou, Iakovos Mavroidis, Sallar Ahmadi-Pour, Rolf Drechsler, Jaume Abella, Sergi Alcaide, Frederik Haxel, Federico Peccia, Jonathan Schröter, Arefeh Mahdavi, Stefan Wallentowitz, Felix Mai, Angelo Garofalo, Davide Rossi, Giuseppe Tagliavini, Hassan Loulou, Francois Clement, Saad Saleh, Paul Detterer, Gert-Jan van Schaik, Nils Wistoff, Luca Benini, Tianhai Liu, James J. Hunt, Andreas Vörg, Philipp van Kempen, Johannes Geier, Ulf Schlichtmann, Ingo Feldner: Forging Robust Building Blocks for Next-Gen RISC-V Chips: Virtual Repository and IP Card. Accepted at 29th Euromicro Conference Series on Digital System Design (DSD) 2026, 2026.
  • Tianhai Liu, Andreas Bremer, Ivan Panov, Alexander Weigl, Shmuel Tyszberowicz, Bernhard Beckert: Realisability-Driven Repair of Natural-Language Requirements via Neuro-Symbolic Reasoning. Accepted at International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA) 2026, XbC-IAI, 2026.
  • Muhammad Asim Minhas, Erik Burger, Ralf Reussner, Tianhai Liu: A Unified Model-driven Framework for Co-Designing System Architecture and Safety Analysis in Cyber-Physical Systems. Accepted at The 22nd European Conference on Modelling Foundations and Applications (ECMFA'26), 2026.
  • Tianhai Liu, James J. Hunt, Holger Blasum, and Darshak Sheladiya: Bringing Cloud-Connected Automotive Workloads to RISC-V: A CVA6-Based FPGA Case Study. RISC-V Summit Europe 2026, Bologna, 8-12 June, 2026. https://doi.org/10.5445/IR/1000193589
  • Tianhai Liu and James J. Hunt: FPGA Lifecycle Management for RISC-V Systems. RISC-V Summit Europe 2026, Bologna, 8-12 June, 2026. https://doi.org/10.5445/IR/1000193590
  • Tianhai Liu, Shmuel Tyszberowicz, Bernhard Beckert: Observable Consistency Checking of Requirements and Models. In Proceedings of the 21st International Conference on Evaluation of Novel Approaches to Software Engineering - Volume 1, (ENASE'26), ISBN 978-989-758-828-0, ISSN 2184-4895, pages 50-63. Best Paper Award https://doi.org/10.5445/IR/1000193552
  • Tianhai Liu, Shmuel Tyszberowicz, Bernhard Beckert: Analyses as First-Class Citizens in Model-Driven Development. In Proceedings of the 29th International Conference on Fundamental Approaches to Software Engineering, (FASE'26), LNCS, vol 16504, pp 180–201. https://doi.org/10.1007/978-3-032-22774-4_10

2023

  • Christian Birchler, Cyrill Rohrbach, Hyeongkyun Kim, Alessio Gambi, Tianhai Liu, Jens Horneber, Timo Kehrer, Sebastiano Panichella: TEASER: Simulation-Based CAN Bus Regression Testing for Self-Driving Cars Software. ASE 2023: 2058-2061. https://doi.org/10.1109/ASE56229.2023.00154
  • Christian Birchler, Cyrill Rohrbach, Hyeongkyun Kim, Alessio Gambi, Tianhai Liu, Jens Horneber, Timo Kehrer, Sebastiano Panichella: TEASER: Simulation-based CAN Bus Regression Testing for Self-driving Cars Software. CoRR abs/2307.03279 (2023). https://doi.org/10.48550/arXiv.2307.03279

2018

  • Tianhai Liu: Efficient Verification of Programs with Complex Data Structures Using SMT Solvers. PhD Thesis, Karlsruhe Institute of Technology, 2018. https://doi.org/10.5445/IR/1000084545

2017

2016

  • Tianhai Liu, Shmuel S. Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl, Mana Taghdiri: Computing Specification-Sensitive Abstractions for Program Verification. SETTA 2016: 101-117. https://doi.org/10.1007/978-3-319-47677-3_7

2014

  • Daniel Grunwald, Christoph Gladisch, Tianhai Liu, Mana Taghdiri, Shmuel S. Tyszberowicz: Generating JML Specifications from Alloy Expressions. Haifa Verification Conference 2014: 99-115. https://doi.org/10.1007/978-3-319-13338-6_9
  • Tianhai Liu, Mateus Araújo, Marcelo d'Amorim, Mana Taghdiri: A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution. Haifa Verification Conference 2014: 284-299. https://doi.org/10.1007/978-3-319-13338-6_21

2012

Education

  • 02/2011 – 07/2018: Dr. rer. nat. (Ph.D.), Computer Science, Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany
  • 10/2006 – 04/2010: Master of Computer Science, Department of Computer Science, Dresden University of Technology, Dresden, Germany
  • 09/2002 – 07/2006: Bachelor of Computer Science, Department of Computer Science and Technology, Chongqing University, Chongqing, China

Student Opportunities & Theses

I am currently supervising Master/Bachelor theses, working students, and interns both at KIT and in industry (aicas GmbH). If you are interested in any of the topics listed below or have your own ideas related to my research interests, please feel free to contact me.

Professional Memberships

  • since 05/2022: Member, Association of Chinese Computer Scientists in Germany (GCI) [GCI]
  • since 11/2012: Member, Association of Chinese Mathematicians and Applied Mathematicians in Germany (GCMA) [GCMA]

Last updated: May 2026