Ali Abbassi, Master’s candidate
David R. Cheriton School of Computer Science
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 operations of Alloy into their equivalent in typed first order logic (TFOL).
Joseph Haraldson, PhD candidate
David R. Cheriton School of Computer Science
We consider the problem of computing the nearest matrix polynomial with a non-trivial Smith Normal Form (SNF). This is a non-convex optimization problem where we find a nearby matrix polynomial with prescribed eigenvalues and associated multiplicity structure in the invariant factors.
Si Chuang Li, Master’s candidate
David R. Cheriton School of Computer Science
Verena Kantere
School of Electrical Engineering and Computer Science, University of Ottawa
Big Data analytics in science and industry are performed on a range of heterogeneous data stores, both traditional and modern, and on a diversity of query engines. Workflows are difficult to design and implement since they span a variety of systems. To reduce development time and processing costs, some automation is needed.
Matthew Amy, PhD candidate
David R. Cheriton School of Computer Science
The design and compilation of correct, efficient quantum circuits is integral to the future operation of quantum computers. This thesis makes contributions to the problems of optimizing and verifying quantum circuits, with an emphasis on the development of formal models for such purposes. We also present software implementations of these methods, which together form a full stack of tools for the design of optimized, formally verified quantum oracles.
Chang Ge, PhD candidate
David R. Cheriton School of Computer Science
