A Comparison between Statecharts and State Transition Assertions. - Nancy A. Day (TPHOLs, 1992)

An example of linking formal methods with case tools: a model checker for statecharts. - Nancy A. Day (CASCON, 1993)

The Semantics of Statecharts in HOL. - Nancy A. Day; Jeffrey J. Joyce (HUG, 1993)

S: A Machine Readable Specification Notation based on Higher Order Logic. - Jeffrey J. Joyce; Nancy A. Day; Michael R. Donat (TPHOLs, 1994)

Using a Formal Description Technique to Model Aspects of a Global Air Traffic Telecommunications Network. - James H. Andrews; Nancy A. Day; Jeffrey J. Joyce (FORTE, 1997)

Symbolic Simulation of Microprocessor Models using Type Classes in Haskell. - Nancy A. Day; Jeffrey R. Lewis; Byron Cook (CHARME, 1999)

Symbolic Functional Evaluation. - Nancy A. Day; Jeffrey J. Joyce (TPHOLs, 1999)

Combining Stream-Based and State-Based Verification Techniques. - Nancy A. Day; Mark D. Aagaard; Byron Cook (FMCAD, 2000)

A Framework for Multi-Notation Requirements Specification and Analysis. - Nancy A. Day; Jeffrey J. Joyce (ICRE, 2000)

A Framework for Microprocessor Correctness Statements. - Mark D. Aagaard; Byron Cook; Nancy A. Day; Robert B. Jones (CHARME, 2001)

Relating Multi-step and Single-Step Microprocessor Correctness Statements. - Mark D. Aagaard; Nancy A. Day; Meng Lou (FMCAD, 2002)

Composable semantics for model-based notations. - Jianwei Niu 001; Joanne M. Atlee; Nancy A. Day (SIGSOFT FSE, 2002)

High-level optimization of pipeline design. - Jennifer Campbell; Nancy A. Day (HLDVT, 2003)

Understanding and Comparing Model-Based Specification Notations. - Jianwei Niu 001; Joanne M. Atlee; Nancy A. Day (RE, 2003)

A framework for superscalar microprocessor correctness statements. - Mark D. Aagaard; Byron Cook; Nancy A. Day; Robert B. Jones (Int. J. Softw. Tools Technol. Transf., 2003)

Template Semantics for Model-Based Notations. - Jianwei Niu 001; Joanne M. Atlee; Nancy A. Day (IEEE Trans. Software Eng., 2003)

Synchronization-at-Retirement for Pipeline Verification. - Mark D. Aagaard; Nancy A. Day; Robert B. Jones (FMCAD, 2004)

Mapping Template Semantics to SMV. - Yun Lu; Joanne M. Atlee; Nancy A. Day; Jianwei Niu 001 (ASE, 2004)

Compositional reasoning for port-based distributed systems. - Alma L. Juarez Dominguez; Nancy A. Day (ASE, 2005)

Interface Automata with Complex Actions. - Shahram Esmaeilsabzali; Farhad Mavaddat; Nancy A. Day (FSEN, 2005)

Unified use case statecharts: case studies. - Davor Svetinovic; Daniel M. Berry; Nancy A. Day; Michael W. Godfrey (Requir. Eng., 2007)

Modelling feature interactions in the automotive domain. - Alma L. Juarez Dominguez; Nancy A. Day; Jeffrey J. Joyce (MiSE, 2008)

Semantically Configurable Code Generation. - Adam Prout; Joanne M. Atlee; Nancy A. Day; Pourya Shaker (MoDELS, 2008)

Interface Automata with Complex Actions: Limiting Interleaving in Interface Automata. - Shahram Esmaeilsabzali; Nancy A. Day; Farhad Mavaddat (Fundam. Informaticae, 2008)

Semantic Criteria for Choosing a Language for Big-Step Models. - Shahram Esmaeilsabzali; Nancy A. Day; Joanne M. Atlee; Jianwei Niu 001 (RE, 2009)

Prescriptive Semantics for Big-Step Modelling Languages. - Shahram Esmaeilsabzali; Nancy A. Day (FASE, 2010)

A Common Framework for Synchronization in Requirements Modelling Languages. - Shahram Esmaeilsabzali; Nancy A. Day; Joanne M. Atlee (MoDELS (2), 2010)

Deconstructing the semantics of big-step modelling languages. - Shahram Esmaeilsabzali; Nancy A. Day; Joanne M. Atlee; Jianwei Niu 001 (Requir. Eng., 2010)

Semantic Quality Attributes for Big-Step Modelling Languages. - Shahram Esmaeilsabzali; Nancy A. Day (FASE, 2011)

Using model checking to analyze static properties of declarative models. - Amirhossein Vakili; Nancy A. Day (ASE, 2011)

Temporal Logic Model Checking in Alloy. - Amirhossein Vakili; Nancy A. Day (ABZ, 2012)

Avestan: a declarative modeling language based on SMT-LIB. - Amirhossein Vakili; Nancy A. Day (MiSE, 2012)

Code generation for a family of executable modelling notations. - Adam Prout; Joanne M. Atlee; Nancy A. Day; Pourya Shaker (Softw. Syst. Model., 2012)

Recommendations for improving the usability of formal methods for product lines. - Joanne M. Atlee; Sandy Beidu; Nancy A. Day; Fathiyeh Faghih; Pourya Shaker (FormaliSE@ICSE, 2013)

Reducing CTL-live model checking to first-order logic validity checking. - Amirhossein Vakili; Nancy A. Day (FMCAD, 2014)

Verifying CTL-live properties of infinite state models using an SMT solver. - Amirhossein Vakili; Nancy A. Day (SIGSOFT FSE, 2014)

Finite Model Finding Using the Logic of Equality with Uninterpreted Functions. - Amirhossein Vakili; Nancy A. Day (FM, 2016)

Representing hierarchical state machine models in SMT-LIB. - Nancy A. Day; Amirhossein Vakili (MiSE@ICSE, 2016)

DASH: A New Language for Declarative Behavioural Requirements with Control State Hierarchy. - José Serna; Nancy A. Day; Sabria Farheen (RE Workshops, 2017)

A Comparison of the Declarative Modelling Languages B, Dash, and TLA+. - Ali Abbassi; Amin Bandali; Nancy A. Day; José Serna (MoDRE@RE, 2018)

Morse: Reducing the Feature Interaction Explosion Problem using Subject Matter Knowledge as Abstract Requirements. - Laure Millet; Nancy A. Day; Jeffrey J. Joyce (RE, 2018)

Extracting counterexamples from transitive-closure-based model checking. - Mitchell Kember; Lynn Tran; George Gao; Nancy A. Day (MiSE@ICSE, 2019)

Astra Version 1.0: Evaluating Translations from Alloy to SMT-LIB. - Ali Abbassi; Nancy A. Day; Derek Rayside (CoRR, 2019)

Transitive-closure-based model checking (TCMC) in Alloy. - Sabria Farheen; Nancy A. Day; Amirhossein Vakili; Ali Abbassi (Softw. Syst. Model., 2020)

Dash+: Extending Alloy with Hierarchical States and Replicated Processes for Modelling Transition Systems. - Tamjid Hossain; Nancy A. Day (RE Workshops, 2021)

Diversity in Software Engineering Conferences and Journals. - Aditya Shankar Narayanan; Dheeraj Vagavolu; Nancy A. Day; Meiyappan Nagappan (CoRR, 2023)

Static Profiling of Alloy Models. - Elias Eid; Nancy A. Day (IEEE Trans. Software Eng., 2023)

Which Classes of Structures Are Both Pseudo-Elementary and Definable by an Infinitary Sentence? - Will Boney; Barbara F. Csima; Nancy A. Day; Matthew Harrison-Trainor (Bull. Symb. Log., 2023)

Dash: declarative behavioural modelling in Alloy with control state hierarchy. - José Serna; Nancy A. Day; Shahram Esmaeilsabzali (Softw. Syst. Model., 2023)

New Techniques for Static Symmetry Breaking in Many-Sorted Finite Model Finding. - Joseph Poremba; Nancy A. Day; Amirhossein Vakili (IEEE Trans. Software Eng., 2023)

Portus: Linking Alloy with SMT-based Finite Model Finding. - Ryan Dancy; Nancy A. Day; Owen Zila; Khadija Tariq; Joseph Poremba (CoRR, 2024)