I investigate the use of models and formal analysis to improve the quality and safety of software-intensive systems. I work mainly at the requirements level on models of system behaviour. I am particularly interested in providing configurable, optimized tools and methodologies to support the use of custom, formal models in specific domains. I use a range of formal analysis tools: theorem provers, model checkers, SMT and SAT solvers.
I am also very interested in computer science outreach activities. I volunteer at elementary schools to introduce computing to students and participate in related activities with UW's Centre for Education in Mathematics and Computing.
I currently serve as a Graduate Student Advocate in the Cheriton School of Computer Science.
Link to Personal Website : https://cs.uwaterloo.ca/~nday/index...
Areas of research
software engineering, model-driven engineering (MDE), modelling and analysis, formal methods, system safety, requirements specification and analysis.
- Waterloo Formal Methods (WatForm)
- Software Engineering Lab
Here is a list of courses that I have taught at University of Waterloo:
- SE212 - Logic and Computation
- CS116 - Introduction to Computer Science 2
- CS745 - Computer-Aided Verification (grad course)
- CS445/SE463 - Software Requirements and Specification
- CS245 - Logic and Computation
- SE112 - Logic and Computation (now renumbered SE 212)
- Ali Abbassi (MMath)
- Sabria Farheen (MMath)
- Jose Serna (MMath)
Past Students and Post-Docs
- Amirhossein Vakili (Post-Doctoral Fellow, 2016)
- Amirhossein Vakili (PhD, 2016)
- Alma Juarez Dominguez (Post-Doctoral Fellow, 2012-2013)
- Alma Juarez Dominguez (PhD, 2012)
- Shahram Esmaeilsabzali (PhD, 2011)
- Alma Juarez Dominguez (MMath, 2005)
- Jianwei Niu (PhD, 2005) (co-supervisor: Jo Atlee)
- Yun Lu (MMath, 2004)
- Jennifer Campbell (MMath, 2003)
I have also worked with a number of undergraduate students on research projects.
Vakili, A., and N. Day, "Finite model finding using the logic of equality with uninterpreted functions", In International Symposium on Formal Methods, volume 9995 of Lecture Notes in Computer Science, 11/2016.
Nancy A. Day and Amirhossein Vakili. Representing hierarchical state machine models in SMT-LIB. In Modelling in Software Engineering (MISE), a workshop of the International Conference on Software Engineering, pages 67-73. ACM, May 2016. [ DOI | http | .pdf ]
Amirhossein Vakili and Nancy A. Day. Verifying CTL-Live properties of infinite state models using an SMT solver. In Foundations of Software Engineering (FSE), pages 213-223. ACM, November 2014.
Amirhossein Vakili and Nancy A. Day. Reducing CTL-Live model checking to first-order logic validity checking. In Formal Methods in Computer-Aided Design (FMCAD), pages 215-218. IEEE, October 2014.
Joanne M. Atlee, Sandy Beidu, Nancy A. Day, Fathiyeh Faghih, and Pourya Shaker. Recommendations for improving the usability of formal methods for product lines. In FME Workshop on Formal Methods in Software Engineering (FormaliSE), pages 43-49. IEEE Computer Society, May 2013. [ DOI | http | .pdf ]
Amirhossein Vakili and Nancy A. Day. Temporal logic model checking in alloy. In International Conference on Abstract State Machines, Alloy, B, VDM, and Z (ABZ), volume 7316 of Lecture Notes In Computer Science, pages 150-163. Springer, June 2012. [ DOI |http | .pdf ]
Amirhossein Vakili and Nancy A. Day. Avestan: a declarative modeling language based on SMT-LIB. In Modelling in Software Engineering (MISE), a workshop of the International Conference on Software Engineering, pages 36-42. IEEE, June 2012. [ DOI | http | .pdf ]
Adam Prout, Joanne M. Atlee, Nancy A. Day, and Pourya Shaker. Code generation for a family of executable modelling notations. Journal of Software and Systems Modelling, 11(2):251-272, 2012. [ DOI | http | .pdf ]