Tue 22 Sep 2020 18:35 - 18:40 at Koala - LBR + DS Poster (2) Chair(s): Kevin Lee
Formal specifications in \textsf{Alloy} are organized around user-defined data domains, associated with \emph{signatures}, with almost no support for built-in datatypes. This minimality in the built-in datatypes provided by the language is one of its main features, as it contributes to the automated analyzability of models. One of the few built-in datatypes available in Alloy specifications are integers, whose SAT-based treatment allows only for small bit-widths. In many contexts, where relational datatypes dominate, the use of integers may be auxiliary, e.g., in the use of cardinality constraints and other features. However, as the applications of \textsf{Alloy} are increased, e.g., with the use of the language and its tool support as backend engine for different analysis tasks, the provision of efficient support for numerical datatypes becomes a need. In this work, we present our current preliminary approach to providing an efficient, scalable and user-friendly extension to \textsf{Alloy}, with arithmetic support for numerical datatypes. Our implementation allows for arithmetic with varying precisions, and is implemented via standard \textsf{Alloy} constructions, thus resorting to SAT solving for resolving arithmetic constraints in models.
Mon 21 Sep Times are displayed in time zone: (UTC) Coordinated Universal Time
16:00 - 16:40: DS: Presentation 2Doctoral Symposium at Kangaroo Chair(s): Jean-Guy SchneiderDeakin University | |||
16:00 - 16:20 Talk | Towards transparency-encouraging partial software disclosure to enable trust in data usage Doctoral Symposium Christian SchindlerInstitute for Enterprise Systems, University of Mannheim | ||
16:20 - 16:40 Talk | SAT-Based Arithmetic Support for Alloy Doctoral Symposium Cesar CornejoUniversity of Rio Cuarto and CONICET |
Tue 22 Sep Times are displayed in time zone: (UTC) Coordinated Universal Time
18:20 - 19:20: LBR + DS Poster (2)Late Breaking Results / Doctoral Symposium at Koala Chair(s): Kevin LeeDeakin University | |||
18:20 - 18:25 Poster | Managing App Testing Device Clouds: Issues and Opportunities Late Breaking Results | ||
18:25 - 18:30 Talk | Towards transparency-encouraging partial software disclosure to enable trust in data usage Doctoral Symposium Christian SchindlerInstitute for Enterprise Systems, University of Mannheim | ||
18:30 - 18:35 Talk | Automated generation of client-specific backends utilizing existing microservices and architectural knowledge Doctoral Symposium Nils WieberInstitute for Enterprise Systems (InES), University of Mannheim | ||
18:35 - 18:40 Talk | SAT-Based Arithmetic Support for Alloy Doctoral Symposium Cesar CornejoUniversity of Rio Cuarto and CONICET | ||
18:40 - 18:45 Talk | Applying Learning Techniques to Oracle Synthesis Doctoral Symposium Facundo MolinaUniversity of Río Cuarto |