• Which classes of structures are both pseudo-elementary and definable by an infinitary sentence? 

  Boney, Will; Csima, Barbara F.; Day, Nancy A.; Harrison-Trainor, Matthew (2019-03-21)

  When classes of structures are not first-order definable, we might still try to find a nice description. There are two common ways for doing this. One is to expand the language, leading to notions of pseudo-elementary ...

• Representing Behavioural Models with Rich Control Structures in SMT-LIB 

  Day, Nancy A.; Vakili, Amirhossein (University of Waterloo, 2015-09-01)

  We motivate and present a proposal for how to represent extended finite state machine behavioural models with rich hierarchical states and compositional control structures (e.g., the Statecharts family) in SMT-LIB. Our ...

• DASH: Declarative Modelling with Control State Hierarchy (Preliminary Version) 

  Serna, Jose; Day, Nancy A.; Esmaeilsabzali, Shahram (University of Waterloo, 2018)

  We present a new language, called DASH, for describing formal behavioural models. DASH combines common modelling constructs to describe abstractly both data and control in an integrated manner. DASH uses the Alloy language ...

• Astra Version 1.0: Evaluating Translations from Alloy to SMT-LIB 

  Abbassi, Ali; Day, Nancy A.; Rayside, Derek (2019-06-13)

  We present a variety of translation options for converting Alloy to SMT-LIB via Alloy’s Kodkod interface. Our translations, which are implemented in a library that we call Astra, are based on converting the set and relational ...

• Adaptive CPU Allocation for Resource Isolation and Work Conservation 

  Guo, Cong (University of Waterloo, 2020-07-06)

  Consolidating multiple workloads on the same physical machine is an effective measure for utilizing resources efficiently and reducing costs. The main objective is to execute multiple demanding workloads using no more than ...

• Finite Model Finding Using the Logic of Equality with Uninterpreted Functions 

  Vakili, Amirhossein; Day, Nancy A. (Springer, 2016)

  The problem of finite model finding, finding a satisfying model for a set of first-order logic formulas for a finite scope, is an important step in many verification techniques. In MACE-style solvers, the problem is mapped ...

• Representing hierarchical state machine models in SMT-LIB 

  Day, Nancy A.; Vakili, Amirhossein (ACM, 2016-05)

  We motivate and present a proposal for how to represent the syntax of behavioural models written in extended finite-state machine languages with hierarchical states (e.g., the Statecharts family) in SMT-LIB. By including ...

• Robot Social Engineering 

  Postnikoff, Brittany (University of Waterloo, 2020-07-06)

  This thesis establishes the new field of Robot Social Engineering. We define Robot Social Engineering as the use of social abilities and techniques by robots to manipulate others in order to achieve a goal. We build the ...

• DASH: A New Language for Declarative Behavioural Requirements with Control State Hierarchy 

  Serna, Jose; Day, Nancy A.; Farheen, Sabria (IEEE, 2017-09-04)

  We present DASH, a new language for describing formal behavioural models of requirements. DASH combines the ability to write abstract, declarative transitions (as in Z or Alloy) with a labelled control state hierarchy (as ...

• A Comparison of the Declarative Modelling Languages B, Dash, and TLA+ 

  Abbassi, Ali; Bandali, Amin; Day, Nancy; Serna, Jose (IEEE, 2019-08)

  Declarative behavioural modelling is a powerful modelling paradigm that enables users to model system func- tionality abstractly and concisely. We compare two well-used formal declarative modelling languages, B and TLA+, ...

• Extracting Counterexamples from Transitive-Closure-Based Model Checking 

  Kember, Mitchell; Tran, Lynn; Gao, George; Day, Nancy (IEEE, 2019)

  We address the problem of how to extract counterexamples for the transitive-closure-based model checking (TCMC) technique. TCMC is a representation of the CTLFC (CTL with fairness constraints) model checking problem in ...

• Morse: Reducing the Feature Interaction Explosion Problem Using Subject Matter Knowledge as Abstract Requirements 

  Millet, Laure; Day, Nancy; Joyce, Jeffrey J. (IEEE, 2018-08)

  The feature interaction problem appears in many different kinds of complex systems, especially systems whose elements are created or maintained by separate entities - for example, a modern automobile that incorporates ...

• Analysis of Textual and Non-Textual Sources of Sentiment in Github 

  De Zoysa, Nalin (University of Waterloo, 2020-05-29)

  Github is a collaborative platform that is used primarily for the development of software. In order to gain more insight into how teams work on Github, we wish to analyze the sentiment content available via communication ...

• Barehand Mode Switching in Touch and Mid-Air Interfaces 

  Surale, Hemant (University of Waterloo, 2020-05-28)

  Raskin defines a mode as a distinct setting within an interface where the same user input will produce results different to those it would produce in other settings. Most interfaces have multiple modes in which input is ...

• Scalable and Reliable Middlebox Deployment 

  Ghaznavi, Milad (University of Waterloo, 2020-05-28)

  Middleboxes are pervasive in modern computer networks providing functionalities beyond mere packet forwarding. Load balancers, intrusion detection systems, and network address translators are typical examples of middleboxes. ...

• On the Integration of Unmanned Aerial Vehicles into Public Airspace 

  Gharibi, Mirmojtaba (University of Waterloo, 2020-05-28)

  Unmanned Aerial Vehicles will soon be integrated in the airspace and start serving us in various capacities such as package delivery, surveillance, search and rescue missions, inspection of infrastructure, precision ...

• Differentially Private Learning with Noisy Labels 

  Mohapatra, Shubhankar (University of Waterloo, 2020-05-28)

  Supervised machine learning tasks require large labelled datasets. However, obtaining such datasets is a difficult task and often leads to noisy labels due to human errors or adversarial perturbation. Recent studies have ...

• Leveraging Watermarks to Improve Performance of Streaming Systems 

  Farhat, Omar (University of Waterloo, 2020-05-28)

  Modern stream processing engines (SPEs) process large volumes of events propagated at high velocity through multiple queries. By continuously receiving watermarks, which are marker events injected into the stream to signify ...

• Extracting and Cleaning RDF Data 

  Farid, Mina (University of Waterloo, 2020-05-28)

  The RDF data model has become a prevalent format to represent heterogeneous data because of its versatility. The capability of dismantling information from its native formats and representing it in triple format offers a ...

• Asking for Help with a Cost in Reinforcement Learning 

  Vandenhof, Colin (University of Waterloo, 2020-05-15)

  Reinforcement learning (RL) is a powerful tool for developing intelligent agents, and the use of neural networks makes RL techniques more scalable to challenging real-world applications, from task-oriented dialogue systems ...

View more