Nancy Day

Associate Professor

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



• Google Scholar
• DBLP
• ACM Digital Library

Refereed Publications

Joseph Poremba, Nancy A. Day, and Amirhossein Vakili. New techniques for static symmetry breaking in many-sorted finite model finding. IEEE Transactions on Software Engineering (IEEE TSE), 49(6):3487 -- 3503, June 2023. [ DOI ]

Jose Serna, Nancy A. Day, and Shahram Esmaeilsabzali. Dash: Declarative behavioural modelling in Alloy with control state hierarchy. Journal of Software and Systems Modelling (SoSym), 22:733--749, April 2023. [ DOI | http ]

Will Boney, Barbara F. Csima, Nancy A. Day, and Matthew Harrison-Trainor. Which classes of structures are both pseudo-elementary and definable by an infinitary sentence? Bulletin of Symbolic Logic, 29(1):1--18, March 2023. [ DOI ]

Elias Eid and Nancy A. Day. Static profiling Alloy models. IEEE Transactions on Software Engineering (IEEE TSE), 49(2):743--759, February 2023. [ DOI ]

Tamjid Hossain and Nancy A. Day. Dash+: Extending Alloy with hierarchical states and replicated processes for modelling transition systems. In International Workshop on Model-Driven Requirements Engineering (MoDRE) @ IEEE International Requirements Engineering Conference (RE), pages 21--29. IEEE, September 2021. [ DOI | .pdf ]

Aman Dureja, Aditya Keerthi, Andrew Liang, Paul Zhang, and Nancy A. Day. Aldb : Debugging alloy models of behavioural requirements. In International Workshop on Model-Driven Requirements Engineering (MoDRE) @ IEEE International Requirements Engineering Conference (RE), pages 21--30. IEEE, August 2020. [ DOI | .pdf ]

Sabria Farheen, Nancy A. Day, Amirhossein Vakili, and Ali Abbassi. Transitive-closure-based model checking in alloy. Journal of Software and Systems Modelling (SoSym), 19:721--740, January 2020. [ DOI | .pdf ]

Mitchell Kember, Lynn Tran, George Gao, and Nancy A. Day. Extracting counterexamples from transitive-closure-based model checking. In Workshop on Modelling in Software Engineering (MISE) @ International Conference on Software Engineering (ICSE), pages 47--54. ACM, May 2019. [ DOI | .pdf ]

Stefania Gnesi, Nico Plat, Nancy A. Day, and Matteo Rossi, editors. Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May 27, 2019. IEEE / ACM, 2019. [ http ]

Ali Abbassi, Amin Bandali, Nancy A. Day, and Jose Serna. A comparison of the declarative modelling languages B, Dash, and TLA+. In International Workshop on Model-Driven Requirements Engineering (MoDRE) @ IEEE International Requirements Engineering Conference (RE), pages 11--20. IEEE Computer Society, August 2018. [ .pdf ]

Laure Millet, Nancy A. Day, and Jeffrey J. Joyce. Morse: Reducing the feature interaction explosion problem using subject matter knowledge as abstract requirements. In International Requirements Engineering Conference (RE), pages 251--261. IEEE Computer Society, August 2018. [ .pdf ]

Jose Serna, Nancy A. Day, and Sabria Farheen. Dash: A new language for declarative behavioural requirements with control state hierarchy. In International Workshop on Model-Driven Requirements Engineering (MoDRE) @ IEEE International Requirements Engineering Conference (RE), pages 64--68. IEEE Computer Society, September 2017. [ .pdf ]

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

Nancy A. Day and Amirhossein Vakili. Representing hierarchical state machine models in SMT-LIB. In Workshop on Modelling in Software Engineering (MISE) @ International Conference on Software Engineering (ICSE), 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 Shing-Chi Cheung, Alessandro Orso, and Margaret-Anne D. Storey, editors, 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. Avestan: a declarative modeling language based on SMT-LIB. In Joanne M. Atlee, Robert Baillargeon, Robert B. France, Geri Georg, Ana Moreira, Bernhard Rumpe, and Steffen Zschaler, editors, Workshop on Modelling in Software Engineering (MISE) @ International Conference on Software Engineering (ICSE), pages 36--42. IEEE, June 2012. [ DOI | http | .pdf ]

Amirhossein Vakili and Nancy A. Day. Temporal logic model checking in Alloy. In John Derrick, John S. Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, and Elvinia Riccobene, editors, 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 ]

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 (SoSym), 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 Perry Alexander, Corina S. Pasareanu, and John G. Hosking, editors, 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 Dimitra Giannakopoulou and Fernando Orejas, editors, International Conference on Fundamental Approaches to Software Engineering (FASE), volume 6603, pages 65--80. Springer, March-April 2011. [ DOI | http | .pdf ]

Shahram Esmaeilsabzali, Nancy A. Day, and Joanne M. Atlee. A common framework for synchronization in requirements modelling languages. In Dorina C. Petriu, Nicolas Rouquette, and Øystein Haugen, editors, International Conference on Model Driven Engineering Languages and Systems, volume 6395 of Lecture Notes in Computer Science, pages 198--212. Springer, October 2010. [ DOI | http | .pdf ]

Shahram Esmaeilsabzali and Nancy A. Day. Prescriptive semantics for big-step modelling languages. In David S. Rosenblum and Gabriele Taentzer, editors, International Conference on Fundamental Approaches to Software Engineering (FASE), volume 6013 of Lecture Notes In Computer Science, pages 158--172. Springer, March 2010. [ 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. [ DOI | http | .pdf ]

Adam Prout, Joanne M. Atlee, Nancy A. Day, and Pourya Shaker. Semantically configurable code generation. In Krzysztof Czarnecki, Ileana Ober, Jean-Michel Bruel, Axel Uhl, and Markus Völter, editors, International Conference on Model Driven Engineering Languages and Systems, volume 5301 of Lecture Notes In Computer Science, pages 705--720. Springer, September-October 2008. [ DOI | http | .pdf ]

Alma L. Juarez Dominguez, Nancy A. Day, and Jeffrey J. Joyce. Modelling feature interactions in the automotive domain. In Joanne M. Atlee, Robert B. France, Geri Georg, Ana Moreira, Bernhard Rumpe, Steven Völkel, and Steffen Zschaler, editors, Workshop on Modelling in Software Engineering (MISE) @ International Conference on Software Engineering (ICSE), 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 David F. Redmiles, Thomas Ellman, and Andrea Zisman, editors, Automated Software Engineering, pages 376--379. ACM, November 2005. [ 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 Alan J. Hu and Andrew K. Martin, editors, 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. [ 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. [ 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 ]

Jianwei Niu, Joanne M. Atlee, and Nancy A. Day. Template semantics for model-based notations. IEEE Transactions on Software Engineering (IEEE TSE), 29(10):866--882, 2003. [ 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 ]

Mark Aagaard, Nancy A. Day, and Meng Lou. Relating multi-step and single-step microprocessor correctness statements. In Mark Aagaard and John W. O'Leary, editors, Formal Methods in Computer-Aided Design (FMCAD), volume 2517 of Lecture Notes In Computer Science, pages 123--141. Springer, November 2002. [ 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. [ DOI | http | .pdf ]

Mark Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones. A framework for microprocessor correctness statements. In Tiziana Margaria and Thomas F. Melham, editors, 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 Warren A. Hunt Jr. and Steven D. Johnson, editors, 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. Utrecht University, Department of Computer Science, Technical Report UU-CS-1999-28. [ .pdf ]

Nancy A. Day and Jeffrey J. Joyce. Symbolic functional evaluation. In Yves Bertot, Gilles Dowek, André Hirschowitz, C. Paulin, and Laurent Théry, editors, Theorem Proving in Higher Order Logics, volume 1690 of Lecture Notes In Computer Science, pages 341--358. Springer, September 1999. [ DOI | http | .pdf ]

Nancy A. Day, Jeffrey R. Lewis, and Byron Cook. Symbolic simulation of microprocessor models using type classes in haskell. In Laurence Pierre and Thomas Kropf, editors, Correct Hardware Design and Verification Methods (CHARME), volume 1703 of Lecture Notes In Computer Science, pages 346--349. 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 Atsushi Togashi, Tadanori Mizuno, Norio Shiratori, and Teruo Higashino, editors, 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 Thomas F. Melham and Juanito Camilleri, editors, 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 Ann Gawman, Evelyn Kidd, and Per-Åke Larson, editors, 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 Jeffrey J. Joyce and Carl-Johan H. Seger, editors, 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 Luc J. M. Claesen and Michael J. C. Gordon, editors, 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.99.