Nancy Day

Associate Professor

• Home
• Publications
  • Journals/Conferences
  • Technical Reports
  • Theses
  • Artifacts
• Students
• Teaching
• Service
• Contact



• Google Scholar
• DBLP
• ACM Digital Library

I study how to model and analyze software-intensive systems to improve their quality and safety. As the complexity and utility of software continues to increase, industry needs ways of ensuring the correctness of their products. I use a range of formal analysis tools: model checkers, finite model finders, SMT and SAT solvers, and theorem provers.

Areas of research: software engineering, model-driven engineering (MDE), modelling and analysis, formal methods, system safety, requirements specification and analysis.

Research Group: Waterloo Formal Methods (WatForm).

Brief Bio: I arrived at the University of Waterloo in January, 2001. Previously, I was a Postdoctoral Research Associate at the Oregon Graduate Institute. I completed my PhD at the University of British Columbia in October 1998 working with Dr. Jeff Joyce. My undergraduate degree is from the University of Western Ontario, where I spent much of my time running with the cross-country and track and field teams. My work has won awards at MODELS (International Conference on Model-Driven Engineering, Languages and Systems) and ISSC (International System Safety Conference).

If you are a prospective graduate or undergraduate student interested in working with me, please follow this link for details.

I am committed to following best practices for equity, diversity, and inclusion in my teaching, research, and administrative responsibilities.

Latest News:

• Congratulations to Owen Zila who has completed his MMath thesis! Owen is continuing as a PhD student. Improvements to Many-Sorted Finite Model Finding using SMT Solvers August 2023. Owen will be continuing to work with us towards his PhD degree!
• Congratulations to Joe Poremba (now at UBC) and Amir Vakili on the publication of our article on New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding" in IEEE Transactions on Software Engineering, Accepted March 2023.
• Congratulations to Tamjid Hossain who has completed his MMath thesis! Dash+: Extending Alloy with Hierarchical States and Replicated Processes for Modelling Transition Systems
• Jose Serna, Nancy A. Day, and Shahram Esmaeilsabzali. Dash: Declarative behavioural modelling in Alloy with control state hierarchy. Journal of Software and Systems Modelling, Accepted Apr 2022.
• Elias Eid and Nancy A. Day. Static profiling Alloy models in IEEE Transactions on Software Engineering, Accepted March 2022.
• Support for Dash has been integrated into our fork of the Alloy Analyzer