Nancy Day

Associate Professor

David R. Cheriton School of Computer Science
University of Waterloo

Refereed Publications

Amirhossein Vakili and Nancy A. 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, pages 677-693, November 2016. Acceptance rate: 26.5%. [ DOI | http | .pdf ]

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. [ DOI | http | .pdf ]

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. [ DOI | http | .pdf ]

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 ]

Amirhossein Vakili and Nancy A. Day. Using model checking to analyze static properties of declarative models. In Automated Software Engineering, pages 428-431. IEEE Computer Society, November 2011. [ DOI | http | .pdf ]

Shahram Esmaeilsabzali and Nancy A. Day. Semantic quality attributes for big-step modelling languages. In International Conference on Fundamental Approaches to Software Engineering (FASE), volume 6603, pages 65-80. Springer, March-April 2011. Acceptance Rate: 29%. [ DOI | http | .pdf ]

Shahram Esmaeilsabzali, Nancy A. Day, and Joanne M. Atlee. A common framework for synchronization in requirements modelling languages. In International Conference on Model Driven Engineering Languages and Systems, volume 6395 of Lecture Notes in Computer Science, pages 198-212. Springer, October 2010. Acceptance Rate: 20.8%. [ DOI | http | .pdf ]

Shahram Esmaeilsabzali and Nancy A. Day. Prescriptive semantics for big-step modelling languages. In International Conference on Fundamental Approaches to Software Engineering (FASE), volume 6013 of Lecture Notes in Computer Science, pages 158-172. Springer, March 2010. Acceptance Rate: 25%. [ DOI | http | .pdf ]

Shahram Esmaeilsabzali, Nancy A. Day, Joanne M. Atlee, and Jianwei Niu. Deconstructing the semantics of big-step modelling languages. Requirements Engineering Journal, 15(2):235-265, 2010. [ DOI | http | .pdf ]

Shahram Esmaeilsabzali, Nancy A. Day, Joanne M. Atlee, and Jianwei Niu. Semantic criteria for choosing a language for big-step models. In International Symposium on Requirements Engineering (RE), pages 181-190. IEEE Computer Society Press, August-September 2009. Acceptance Rate: 21%. [ DOI | http | .pdf ]

Adam Prout, Joanne M. Atlee, Nancy A. Day, and Pourya Shaker. Semantically configurable code generation. In International Conference on Model Driven Engineering Languages and Systems, volume 5301 of Lecture Notes In Computer Science, pages 705-720. Springer, September-October 2008. Acceptance Rate: 21%, Distinguished Paper Award (one of two). [ DOI | http | .pdf ]

Alma L. Juarez Dominguez, Nancy A. Day, and Jeffrey J. Joyce. Modelling feature interactions in the automotive domain. In Modelling in Software Engineering (MISE), a workshop of the International Conference on Software Engineering, pages 45-50. ACM, May 2008. [ DOI | http | .pdf ]

Shahram Esmaeilsabzali, Nancy A. Day, and Farhad Mavaddat. Interface automata with complex actions: Limiting interleaving in interface automata. Fundamenta Informatica, 82(4):465-512, 2008. [ http | .pdf ]

Davor Svetinovic, Daniel M. Berry, Nancy A. Day, and Michael W. Godfrey. Unified use case statecharts: case studies. Requirements Engineering Journal, 12(4):245-264, 2007. [ DOI | http | .pdf ]

Shahram Esmaeilsabzali, Farhad Mavaddat, and Nancy A. Day. Interface automata with complex actions. Electronic Notes Theoretical Computer Science, 159:79-97, 2006. Proceedings of the IPM International Workshop on Foundations of Software Engineering (FSEN), Distinguished Paper Award. [ DOI | http | .pdf ]

Alma L. Juarez Dominguez and Nancy A. Day. Compositional reasoning for port-based distributed systems. In Automated Software Engineering, pages 376-379. ACM, November 2005. Acceptance Rate: 22%. [ DOI | http | .pdf ]

Shahram Esmaeilsabzali, Nancy A. Day, , and Farhad Mavaddat. Specifying search queries for web service discovery. In International Workshop on Service-Oriented Computing: Consequences for Engineering Requirements (SOCCER), a workshop of the IEEE International Conference on Requirements Engineering (RE), 2005. [ .pdf ]

Mark Aagaard, Nancy A. Day, and Robert B. Jones. Synchronization-at-retirement for pipeline verification. In Formal Methods in Computer-Aided Design (FMCAD), volume 3312 of Lecture Notes In Computer Science, pages 113-127. Springer, November 2004. [ DOI | http | .pdf ]

Yun Lu, Joanne M. Atlee, Nancy A. Day, and Jianwei Niu. Mapping template semantics to SMV. In Automated Software Engineering, pages 320-325. IEEE Computer Society, 2004. Acceptance Rate: 30%. [ DOI | http | .pdf ]

Jianwei Niu, Joanne M. Atlee, and Nancy A. Day. Understanding and comparing model-based specification notations. In International Symposium on Requirements Engineering (RE), pages 188-199. IEEE Computer Society, September 2003. Acceptance Rate: 19%. [ DOI | http | .pdf ]

Mark Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones. A framework for superscalar microprocessor correctness statements. International Journal on Software Tools for Technology Transfer, 4(3):298-312, 2003. [ DOI | http | .pdf ]

Jianwei Niu, Joanne M. Atlee, and Nancy A. Day. Template semantics for model-based notations. IEEE Transactions on Software Engineering, 29(10):866-882, 2003. [ DOI | http | .pdf ]

Jennifer Campbell and Nancy A. Day. High-level optimization of pipeline design. In Eighth IEEE International High-Level Design Validation and Test Workshop 2003, San Francisco, CA, USA, November 12-14, 2003, pages 43-48. IEEE Computer Society, 2003. [ DOI | http | .pdf ]

Mark Aagaard, Nancy A. Day, and Meng Lou. Relating multi-step and single-step microprocessor correctness statements. In Formal Methods in Computer-Aided Design (FMCAD), volume 2517 of Lecture Notes In Computer Science, pages 123-141. Springer, November 2002. Received the highest possible overall reviews. [ DOI | http | .pdf ]

Jianwei Niu, Joanne M. Atlee, and Nancy A. Day. Composable semantics for model-based notations. In Foundations of Software Engineering (FSE), pages 149-158. ACM, November 2002. Acceptance Rate: 13%. [ DOI | http | .pdf ]

Mark Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones. A framework for microprocessor correctness statements. In Correct Hardware Design and Verification Methods (CHARME), volume 2144 of Lecture Notes In Computer Science, pages 433-448. Springer, September 2001. [ DOI | http | .pdf ]

Nancy A. Day, Mark Aagaard, and Byron Cook. Combining stream-based and state-based verification techniques. In Formal Methods in Computer-Aided Design (FMCAD), volume 1954 of Lecture Notes In Computer Science, pages 126-142. Springer, November 2000. [ DOI | http | .pdf ]

Nancy A. Day, Michael R. Donat, and Jeffrey J. Joyce. Taking the hol out of HOL. In NASA Langley Formal Methods Workshop, June 2000. [ .pdf ]

Nancy A. Day and Jeffrey J. Joyce. A framework for multi-notation requirements specification and analysis. In International Symposium on Requirements Engineering (RE), pages 39-48. IEEE Computer Society, June 2000. [ DOI | http | .pdf ]

Nancy A. Day, John Launchbury, , and Jeff Lewis. Logical abstractions in haskell. In Haskell Workshop, October 1999. [ .pdf ]

Nancy A. Day, Jeffrey R. Lewis, and Byron Cook. Symbolic simulation of microprocessor models using type classes in haskell. In Correct Hardware Design and Verification Methods (CHARME), volume 1703 of Lecture Notes In Computer Science, pages 346-349. Springer, September 1999. [ DOI | http | .pdf ]

Nancy A. Day and Jeffrey J. Joyce. Symbolic functional evaluation. In Theorem Proving in Higher Order Logics, volume 1690 of Lecture Notes In Computer Science, pages 341-358. Springer, September 1999. [ DOI | http | .pdf ]

James H. Andrews, Nancy A. Day, and Jeffrey J. Joyce. Using a formal description technique to model aspects of a global air traffic telecommunications network. In Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE X / PSTV XVII'97, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE X) and Protocol Specification, Testing and Verification (PSTV XVII), volume 107 of IFIP Conference Proceedings, pages 417-432. Chapman & Hall, November 1997. [ .pdf ]

Nancy A. Day, Jeffrey J. Joyce, and Gerry Pelletier. Formalization and analysis of the separation minima for aircraft in the North Atlantic Region. In NASA Langley Formal Methods Workshop, volume 3356. NASA Conference Publication, September 1997. [ .pdf ]

Nancy A. Day. Formal validation of system specifications. In Doctoral Consortium, International Conference on Software Engineering, 1997.

Jeffrey J. Joyce, Nancy A. Day, and Michael R. Donat. S: A machine readable specification notation based on higher order logic. In Higher Order Logic Theorem Proving and Its Applications, volume 859 of Lecture Notes In Computer Science, pages 285-299. Springer, September 1994. [ DOI | http | .pdf ]

Nancy A. Day. An example of linking formal methods with case tools: a model checker for statecharts. In Conference of the Centre for Advanced Studies (CASCON), pages 97-107. IBM, October 1993. [ DOI | http | .pdf ]

Nancy A. Day and Jeffrey J. Joyce. The semantics of statecharts in HOL. In Higher Order Logic Theorem Proving and Its Applications, volume 780 of Lecture Notes In Computer Science, pages 338-351. Springer, August 1993. [ DOI | http | .pdf ]

Nancy A. Day. A comparison between statecharts and state transition assertions. In Higher Order Logic Theorem Proving and Its Applications, volume A-20 of IFIP Transactions, pages 247-262. North-Holland/Elsevier, September 1992. [ .pdf ]


This file was generated by bibtex2html 1.96.

David R. Cheriton School of Computer Science, University of Waterloo

Last modified on Tuesday 24th of January 2017 10:49:58 AM