Search Results

Documents authored by Zhang, Cheng

Document
Software Engineering in Practice Track Paper
DOI: 10.4230/LIPIcs.ESEM.2026.87
AI Ethics to Requirements Practice: Building and Evaluating the HealthAI Ethics Assistant

Authors: Yutan Huang, Jingfan Chen, Fanyu Wang, Chetan Arora, John Grundy, and Cheng Zhang

Published in: LIPIcs, Volume 394, 20th International Symposium on Empirical Software Engineering and Measurement (ESEM 2026)

Abstract
Healthcare AI software teams face growing pressure to translate ethical principles and regulatory obligations into concrete requirements, design decisions, and assurance evidence. Day-to-day requirements engineering (RE) practice still lacks lightweight tool support for connecting abstract frameworks, such as the EU AI Act and the NIST AI Risk Management Framework, to actionable requirements work. This paper builds on a two-phase research project. In the first phase, we conducted an empirical interview study with healthcare AI practitioners spanning clinicians as end users of HealthAI systems and software engineers as developers of HealthAI software systems, which surfaced recurring concerns around transparency, accountability, and the difficulty of mapping regulatory obligations to concrete engineering tasks. Informed by those findings, in the second phase we designed, implemented, and conducted an initial evaluation of the HealthAI Ethics Assistant, an AI-enabled RE tool for healthcare AI software systems. The tool supports practitioners in generating, validating, and comparing ethical requirements through a structured Create-Validate-Compare workflow. It was implemented as a full-stack web application and grounded in a structured knowledge base combining regulatory guidance (EU AI Act, NIST AI RMF) with practitioner concerns surfaced by the interview study. The work was conducted in close collaboration with an R&D engineer at a medical device manufacturer, who contributed to industrial problem framing and participated as the first practitioner evaluator in the case study reported here. Our initial evaluation is exploratory, involving a single case study, and used the Technology Acceptance Model and the System Usability Scale. Traceable regulatory references were rated as the most valuable and trustworthy feature, highlighting the importance of explainability and evidence support in compliance-oriented requirements work. The main adoption challenge was not basic usability, but fitting the tool into existing engineering and regulatory workflows. We derive practice-oriented lessons for designing AI-enabled requirements tools in regulated domains: ground LLM outputs in explicit compliance sources, support multiple practitioner perspectives, make generated requirements reviewable rather than authoritative, and align tool use with existing assurance processes. These early results suggest that AI-enabled assistants can help bridge ethical AI principles and practical requirements engineering when designed as auditable, human-in-the-loop support tools rather than autonomous compliance solutions.
Cite as

Yutan Huang, Jingfan Chen, Fanyu Wang, Chetan Arora, John Grundy, and Cheng Zhang. AI Ethics to Requirements Practice: Building and Evaluating the HealthAI Ethics Assistant. In 20th International Symposium on Empirical Software Engineering and Measurement (ESEM 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 394, pp. 87:1-87:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{huang_et_al:LIPIcs.ESEM.2026.87,
  author =	{Huang, Yutan and Chen, Jingfan and Wang, Fanyu and Arora, Chetan and Grundy, John and Zhang, Cheng},
  title =	{{AI Ethics to Requirements Practice: Building and Evaluating the HealthAI Ethics Assistant}},
  booktitle =	{20th International Symposium on Empirical Software Engineering and Measurement (ESEM 2026)},
  pages =	{87:1--87:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-450-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{394},
  editor =	{Feldt, Robert and Paasivaara, Maria and Mendez, Daniel and Wagner, Stefan and Bar\'{o}n, Marvin Mu\~{n}oz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESEM.2026.87},
  URN =		{urn:nbn:de:0030-drops-280555},
  doi =		{10.4230/LIPIcs.ESEM.2026.87},
  annote =	{Keywords: Requirements Engineering, Software Engineering, AI ethics, Healthcare, Large Language Models, Regulatory Compliance.}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.36
Kleene Algebra with Commutativity Conditions Is Undecidable

Authors: Arthur Azevedo de Amorim, Cheng Zhang, and Marco Gaboardi

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra.
Cite as

Arthur Azevedo de Amorim, Cheng Zhang, and Marco Gaboardi. Kleene Algebra with Commutativity Conditions Is Undecidable. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 36:1-36:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{azevedodeamorim_et_al:LIPIcs.CSL.2025.36,
  author =	{Azevedo de Amorim, Arthur and Zhang, Cheng and Gaboardi, Marco},
  title =	{{Kleene Algebra with Commutativity Conditions Is Undecidable}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{36:1--36:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.36},
  URN =		{urn:nbn:de:0030-drops-227933},
  doi =		{10.4230/LIPIcs.CSL.2025.36},
  annote =	{Keywords: Kleene Algebra, Hypotheses, Complexity}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.157
Domain Reasoning in TopKAT

Authors: Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative programs. However, while TopKAT inherits many pleasant features of KATs, such as having a decidable equational theory, it is incomplete with respect to relational models. In other words, there are properties that hold true of all relational TopKATs but cannot be proved with the axioms of TopKAT. This issue is potentially worrisome for program-logic applications, in which relational models play a key role. In this paper, we further investigate the completeness properties of TopKAT with respect to relational models. We show that TopKAT is complete with respect to (co)domain comparison of KAT terms, but incomplete when comparing the (co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate specifications in TopKAT hinges on this type of formula, the aforementioned incompleteness results have a limited impact when using TopKAT to reason about such specifications.
Cite as

Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. Domain Reasoning in TopKAT. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 157:1-157:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ICALP.2024.157,
  author =	{Zhang, Cheng and de Amorim, Arthur Azevedo and Gaboardi, Marco},
  title =	{{Domain Reasoning in TopKAT}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{157:1--157:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.157},
  URN =		{urn:nbn:de:0030-drops-203003},
  doi =		{10.4230/LIPIcs.ICALP.2024.157},
  annote =	{Keywords: Kleene algebra, Kleene Algebra With Tests, Kleene Algebra With Domain, Kleene Algebra With Top and Tests, Completeness, Decidability}
}

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact