Congratulations to ACM Fellow Marsha Chechik!
Written by Taneea S Agrawaal
Marsha Chechik, Professor, Department of Computer Science at the University of Toronto, has been named an ACM Fellow for her “foundational advances in formal reasoning for quality software development at scale.” This recognition—bestowed on fewer than 1 percent of ACM members—highlights her work at the intersection of formal methods and software engineering, where she has helped bridge rigorous theory with real‐world practice. Over the course of her career, Marsha has advanced automated reasoning technologies, making it possible to analyze complex, distributed systems with greater precision and usability.
We are delighted to have this exclusive interview for ACM Women, in which she discusses the challenges of modeling uncertainty, strategies for introducing formal analysis into existing development workflows, and the role of AI in shaping the future of software verification.
Congratulations on your ACM Fellow Award! Your ACM Fellow citation emphasizes your work on formal reasoning for “quality software development at scale.” As software systems grow increasingly complex and distributed, what foundational advances in formal methods do you believe are most critical to ensuring reliability in large-scale systems?
Marsha: Thank you! I am broadly interested in modeling and analysis of software systems. The two come hand-in-hand. Modeling means making decisions about what is critical to capture (e.g., uncertainty) and what might be abstracted away (e.g., numerical constraints). These decisions are critically related to what we hope our analysis to tell us. Development of powerful automated reasoning technologies such as SMT solvers enable effective reasoning about a variety of properties of complex systems.
Your research integrates both theoretical rigor and practical quality in software. How do you define “quality” in modern software development, and how can formal reasoning balance competing priorities like safety, adaptability, and scalability?
Marsha: Adaptability and scalability are not properties expressible in formal logic. In fact, neither is safety. I think that one of the reasons of success of our research has been our choice to work on the boundary between formal methods and software engineering. Yes, we regularly make contributions to the formal methods literature, from foundations to tooling to applications, but we approach formal methods work from the software engineering perspective: elicitation of the right requirements, development of languages and logics to support the kinds of questions that we see users wanting to ask, focus on reuse, communication of analysis outcomes, engaging the user in helping the formal reasoning succeed, attaching analysis onto existing processes, mixing verification methods as required by the problem we are solving, etc.
As one of only 55 ACM Fellows selected this year (representing the top 1% of ACM members), what does this recognition mean for your field? How can such honors amplify the visibility of formal methods in addressing industry’s growing demand for reliable, large-scale systems?
Marsha: Compared to several other areas of CS, most notably machine-learning but even other areas of software engineering such as empirical methods, formal methods is not a very prolific area, as measured in the number of published papers and received citations. So recognition of the impact of this area by the ACM awards committee is very welcome. I also hope that it would help recent graduates in this field compete successfully for jobs in top academic institutions. (Having served as Chair of my department, I can attest first-hand how some areas produce graduates with 30 publications, significantly affecting university recruitment committees 🙂.)
Your work has influenced both academic research and industrial practice. What lessons have you learned about translating formal reasoning techniques into tools or processes that developers adopt, especially in organizations resistant to formal verification?
Marsha: I am not going to say anything surprising here. Organizations, at least in my experience, are reluctant to embrace revolutionary ideas, but are very happy for automated analysis support for the processes they already engage in. So, a long time is spent building a relationship with an organization and trying to understand what they actually do (as opposed to what we think they should do!). Once we are able to meet them where they are at, showing that our tools have a potential to bring concrete value, they become much more willing to engage in exploration of more advanced ideas.
In the wake of recent efforts to dismantle DEI initiatives—such as legislative bans on diversity programs in U.S. states and institutional pushback inspired by the Trump administration’s anti-DEI rhetoric—how can fields like formal methods, and others that already struggle with underrepresentation, ensure progress toward inclusivity isn’t reversed? As a leader in this space, what strategies have you found effective in advocating for diversity while navigating political or institutional resistance?
Marsha: For many of us, myself included, increasing participation of women in Computer Science has been a lifelong pursuit. As a community, we have made significant progress – and success of ACM-W and the selection of a number of women and members of other underrepresented groups as ACM Fellows is a testament of that. This elevation comes with an even greater responsibility of advocacy for broadening participation, including mentorship, ensuring representation in program committees and leadership roles, nominating colleagues for awards, etc.
With the rise of AI/ML-driven systems and cyber-physical infrastructures (e.g., smart cities), what new verification challenges do you foresee in maintaining “quality at scale,” and how should the formal methods community adapt?
Marsha: Now is an incredible time to be in this field. Raise of AI helps the field solve some of the problems it has been grappling with for years such as finding the right program invariants. More importantly, with Generative AI, we can now engage users, individuals without formal methods or perhaps even computer science training, into building domain models, understanding environmental assumptions, and then observing analysis outcomes such as violation scenarios. This massively expands the domain of applicability of formal methods, from expert-crafted models of complex algorithms to code generation supporting a daily task of software development to being able to specify and reason about complex legal, ethical, sustainability properties of systems interacting with humans.
Furthermore, with AI’s unparallel ability to generate (not necessarily correct or useful) code, core formal methods goals – specifying what you want and then checking that the produced outcome is correct, become even more important, far outside of its traditional domain of safety-critical systems.
For those aspiring to contribute to foundational fields like formal reasoning, what guidance would you offer to ensure their work achieves both academic rigor and real-world impact?
Marsha: In the world that now aims to solve right about every problem with “let’s just train an LLM to do something and put another LLM in charge of checking whether the answers are correct”, there is a lot of room for more foundational, more complex solutions. So if you are aspiring to contribute to formal reasoning – welcome! There is a lot to be done! However, AI is here to stay, and we should remain vigilant that our logic-based solutions are not only (scientifically) novel but also (practically) significant, that is, they are competitive for solving real problems compared to AI. That being said, as I mentioned earlier, it is now significantly easier to penetrate the boundary between real and formal worlds, testing validity of abstractions, checking assumptions and engaging users.
Thank you for this interview, Dr Chechik and congratulations once again!