Workshop on the Future of Alloy

April 30 & May 1, 2018. Cambridge, MA

The goal of the workshop is to bring together researchers and users of Alloy, share their perspectives, and formulate short/long-term agendas for improving the language & its tools. We welcome participants from both industry and academia.

The workshop will include discussions on various aspects of Alloy, including (but not limited to):
Extensions: What’s not so easy to express in Alloy, and what language extensions could we make? What are some alternative backends that we could explore (e.g., SMT)?
Benchmarks: How do we collect and share models built by users over the years? What kind of infrastructure do we need?
Usability: What are some obstacles preventing a wider adoption of Alloy? What usability improvements could we make?
Education: How do we teach Alloy to students and practitioners? What education materials could we develop and share among teachers?

The workshop will also include a series of short talks, although they will primarily be intended to ignite discussions among the attendees (not your typical conference presentations!).

Logistics

The workshop will take place over 1.5 days in the Stata Center (home to the Computer Science & AI Lab at MIT) in Cambridge, MA, USA.

The registration fee is $100, and will include lunches, an evening reception, coffee, and refreshments.

Location: MIT Stata Center, 32 Vassar St, Cambridge, MA, Room 32-D463 (directions).
Registration deadline: Mar 31, 2018
Workshop dates: April 30 & May 1 (half day), 2018

Rooms are available at a fixed rate at the following hotels:
Kendall Hotel ($299.99/night; 3 min walk; use promo code CSA18, available until Mar 26)
Hyatt Regency Cambridge ($249.99/night; 20 min walk)
Marriott Cambridge ($357.00/night; 7 min walk)
A number of other hotels are available in the Cambridge/Boston area.

Registration

Closed.

Program

Monday
9:00 am	Opening remarks, Daniel Jackson
9:15	Language Extensions (Chair: Eunsuk, Scribe: Sarfraz) Electrum: Lightweight Specification of Behavioral Models with Rich Configurations, David Chemouil & Julien Brunel (ONERA/DTIS) DynAlloy: An Extension of Alloy for Writing and Analyzing Behavioral Models, Nazareno Aguirre (University of Rio Cuarto and CONICET) Representing and Analyzing Transition Systems in Alloy, Nancy Day (University of Waterloo) Synthesis of Design Tradeoff Spaces with Quantitative Guarantees, Javier Camara (CMU) Discussion
10:30	Break
10:45	Analysis: Alternative Backends (Chair: Emina, Scribe: Eunsuk) Solving Alloy Constraints with an SMT Solver for Relational Logic, Cesare Tinelli (University of Iowa) Translating the Alloy Language to SMT-Lib, Dan Dougherty (WPI) Ocelot: Relational Logic in a Solver-Aided Language, James Bornholt (University of Washington) AlleAlle: An Extensible Relational Model Finder Modulo Theories, Jouke Stoel (CWI) Discussion
12:00 pm	Lunch
1:15	Education (Chair: Daniel, Scribe: Emina) Logic for Systems: Teaching Alloy to the Theory-Averse, Tim Nelson (Brown University) Using Alloy in a Language Lab Approach to Introductory Discrete Mathematics, Charles Wallace (Michigan Technological University) Towards a Web-Based Analyzer to Improve the Teaching of Alloy, Alcino Cunha (INESC TEC & Universidade do Minho) Alloy as an Introduction to Formal Methods, Hillel Wayne Discussion
2:30	Break
2:45	Analysis: Model Exploration & Scalability (Chair: Eunsuk, Scribe: Daniel) Enriching Model Exploration with Provenance, Tim Nelson (Brown University) On Extending Kodkod to Support Temporal Features and Scenario Exploration, Nuno Macedo (INESC TEC & U. Minho) Validating SGAC Access Control Policies with Alloy and ProB, Marc Frappier (Université de Sherbrooke) Tight Bounds Computation and Applications to Bounded Analyses, Marcelo Frias (Buenos Aires Institute of Technology and CONICET) Reducing the Evolutionary Analysis Cost of Alloy, Hamid Bagheri (University of Nebraska-Lincoln) Discussion
4:15	Break
4:30	Discussion: Breakout Session
5:15	Break
6:15	Reception

Tuesday
9:00 am	Applications & Adoption (Chair: Sarfraz, Scribe: Daniel) Alloy and the Future of Networking, Pamela Zave (Princeton University) The Role of Alloy in Developing Scientific Software, John Baugh & Tristan Dyer (NCSU) The Academic Failure with Alloy, Peter Kriens (aQute) AlloyInEcore: Deep Embedding of First-Order Relational Logic into Meta-Object Facility, Ferhat Erata (UNIT Information Technologies R&D Ltd.) Discussion
10:15	Break
10:30	Discussion: Breakout Session (continued)
12:00 pm	Lunch
1:00	Summary & closing remarks
Afternoon	Tutorial: The state of the Alloy codebase & making extensions, Peter Kriens

Organization

General chair: Daniel Jackson (MIT)
Program chairs: Eunsuk Kang (CMU & Toyota ITC), Sarfraz Khurshid (UT Austin), Emina Torlak (University of Washington)