I’m a final-year Ph.D. student in Software Engineering at the Software and Societal Systems Department (S3D) at Carnegie Mellon University. I work with Dr. Eunsuk Kang and Dr. David Garlan. My research mainly focuses on software architecture, software quality, and formal methods. My goal is to develop methodologies and tools to help developers systematically design and build software systems that are safe and robust.

[Resume][CV][Google Scholar][GitHub]

I’m actively looking for a summer internship opportunity!!!

Projects

• Software Robustness: Engineers and developers always want to make their software systems robust. However, what we really mean about “robustness” is often vague. IEEE defines robustness as the ability of a software system to function correctly under uncertainties in the inputs, while it is unclear what the uncertainties are and how we define the correctness of the function. In this project, we aim to develop a general formal framework for defining and reasoning software robustness. Under this framework, we have developed a tool for computing software robustness for transition systems, and a tool for automatically robustifying a (transition) system. Currently, we are also working on reasoning robustness for systems with ML components.

• AlloyMax: Alloy is a first-order modeling language developed by MIT with SAT as its back-end solver. It is widely used in design verification and model generation. Because of the nature of SAT, using Alloy for model generation generates an arbitrary model that satisfies the constraints, which may not be helpful. AlloyMax extends Alloy with MaxSAT solving that enables it to synthesize optimal models, which not only satisfy the constraints but also optimize for certain requirements. It brings optimization capability to Alloy and allows Alloy to solve a wider range of problems.

Selected Publications

• Robustification of Behavioral Designs against Environmental Deviations.
  Changjian Zhang, Tarang Saluja, Romulo Meira Goes, Matthew Bolton, David Garlan, and Eunsuk Kang. (ICSE 2023).

• AlloyMax: bringing maximum satisfaction to relational specifications. (Distinguished Paper Award)
  Changjian Zhang, Ryan Wagner, Pedro Orvalho, David Garlan, Vasco Manquinho, Ruben Martins, and Eunsuk Kang. 2021. In Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2021). Association for Computing Machinery, New York, NY, USA, 155–167.

• A behavioral notion of robustness for software systems.
  Changjian Zhang, David Garlan, and Eunsuk Kang. 2020. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2020). Association for Computing Machinery, New York, NY, USA, 1–12.

Other Work

• Fortis: A Tool for Analysis and Repair of Robust Software Systems.
  Changjian Zhang, Ian Dardik, Romulo Meira-Goes, David Garlan, Eunsuk Kang. (FMCAD 2023).

• Runtime Resolution of Feature Interactions through Adaptive Requirement Weakening.
  Simon Chu, Emma Shedden, Changjian Zhang, Romulo Meira-Goes, Gabriel Moreno, David Garlan, and Eunsuk Kang. (SEAMS 2023).

• Safe Run-time Reconfiguration for Event-driven Systems with Pub/Sub in ROS.
  Changjian Zhang, Eunsuk Kang, David Garlan. 2018.

Bio

I received my Bachelor’s degree in Computer Science at Beijing Institute of Technology. Then, I received my Master’s degree in Software Engineering at Carnegie Mellon University. Now, I’m a final-year Ph.D. student at CMU, working with Dr. Eunsuk Kang and Dr. David Garlan.