Now showing items 1-11 of 11

    • Astra: Evaluating Translations from Alloy to SMT-LIB 

      Abbassi, Ali (University of Waterloo, 2018-12-21)
      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 ...
    • A Comprehensive Study of Declarative Modelling Languages 

      Bandali, Amin (University of Waterloo, 2020-07-14)
      Declarative behavioural modelling is a powerful modelling paradigm that enables users to model system functionality abstractly and formally. An abstract model is a concise and compact representation of key characteristics ...
    • Dash+: Extending Alloy with Replicated Processes for Modelling Transition Systems 

      Hossain, Tamjid (University of Waterloo, 2022-09-27)
      Modelling systems abstractly shows great promise to uncover bugs early in system development. The formal language Alloy provides the means of writing constraints abstractly but lacks explicit constructs for describing ...
    • Dash: Declarative Behavioural Modelling in Alloy 

      Serna, Jose (University of Waterloo, 2019-01-25)
      An abstract model is a representation of the fundamental characteristics and properties of a system, and its purpose is to provide feedback to stakeholders about the correctness of the system during the early stages of ...
    • Detection of Feature Interactions in Automotive Active Safety Features 

      Juarez Dominguez, Alma L. (University of Waterloo, 2012-05-02)
      With the introduction of software into cars, many functions are now realized with reduced cost, weight and energy. The development of these software systems is done in a distributed manner independently by suppliers, ...
    • Improvements to Transitive-Closure-based Model Checking in Alloy 

      Farheen, Sabria (University of Waterloo, 2018-01-19)
      Model checking, which refers to the verification of temporal properties of a transition system, is a common formal method for verifying models. Transitive-closure-based model checking (TCMC), developed by Vakili et al., ...
    • Linking Alloy with SMT-based Finite Model Finding 

      Tariq, Khadija (University of Waterloo, 2021-01-28)
      Alloy is a well-known declarative language for modelling systems early in the development process. Currently, it uses the Kodkod library as its back-end for finite model finding (finding instances of the model by determining ...
    • Mapping Template Semantics to SMV 

      Lu, Yun (University of Waterloo, 2004)
      Template semantics is a template-based approach to describing the semantics of model-based notations, where a pre-defined template captures the notations' common semantics, and parameters specify the notations' distinct ...
    • Prescriptive Semantics For Big-Step Modelling Languages 

      Esmaeilsabzali, Shahram (University of Waterloo, 2011-02-22)
      With the popularity of model-driven methodologies and the abundance of modelling languages, a major question for a modeller is: Which language is suitable for modelling a system under study? To answer this question, one ...
    • Profiling Alloy Models 

      Eid, Elias (University of Waterloo, 2021-09-03)
      Modeling of software-intensive systems using formal declarative modeling languages offers a means of managing software complexity through the use of abstraction and early identification of correctness issues by formal ...
    • Temporal Logic Model Checking as Automated Theorem Proving 

      Vakili, Amirhossein (University of Waterloo, 2016-01-19)
      Model checking is an automatic technique for the verification of temporal properties of a system. In this technique, a system is represented as a labelled graph and the specification as a temporal logic formula. The core ...


      University of Waterloo Library
      200 University Avenue West
      Waterloo, Ontario, Canada N2L 3G1
      519 888 4883

      All items in UWSpace are protected by copyright, with all rights reserved.

      DSpace software

      Service outages