Portland, Oregon, November 6, 2006

Workshop Programme

9:00-10:30 Tools and Technology

(5) Introductions
(20) Marcelo F. Frias and Juan P. Galeotti
Faster SAT-Based Analysis of OO-Programs by Separation of Mutant and Non Mutant Objects
(20) Fadi Zaraket, Adnan Aziz and Sarfraz Khurshid
Applying a Sequential Circuit Solver to Alloy
(20) Marcelo F. Frias, Carlos G. Lopez Pombo and Mariano M. Moscato
Dynamite: Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications
(25) Discussion
What goes beyond SAT for model-finding?
What role should theorem-proving play?

11:00-12:30 Modeling Frameworks

(20) Charles Chen, Paul Grisham, Sarfraz Khurshid and Dewayne Perry
Design and Validation of a General Security Model with the Alloy Analyzer
(20) Laura Dillon, Kurt Stirewalt, Beata Sarna-Starosta and Scott Fleming
Developing an Alloy Framework akin to OO Frameworks
(15) Alain Wegmann, Lam-Son Le, Lotfi Hussami and Dirk Beyer
Implementation of a Modeling Tool Using Alloy as Meta-Modeling Language and CrocoPat as Validation Tool
(35) Discussion
How reusable is an Alloy model (note that reusability is our working definition of a "framework")?
When does a case study become a framework?
What language features would be helpful for frameworks?

2:00-3:30 Case Studies

(15) Fernando Valles Barajas
A formal model for a requirements engineering tool
(15) Rohit Gheyi, Tiago Massoni and Paulo Borba
A Theory for Feature Models in Alloy
(15) Sanjai Narain, Y. Alice Cheng, Alex Poylisher and Rajesh Talpade
Network Single Point of Failure Analysis via Model Finding
(20) Alanna Zito and Juergen Dingel
Modeling UML2 Package Merge with Alloy
(25) Discussion
How can we help industry more with the use of Alloy?
Is an Alloy methodology possible, and would it help?

4:00-5:30 Education and Other Topics

(15) Michael Lutz
Alloy, Software Engineering, and Undergraduate Education
(15) Darko Marinov and Sarfraz Khurshid
What Will the User Do (Next) in the Tool?
(15) Emina Torlak and Greg Dennis
Kodkod for Alloy Users
(25) Discussion
What is the role of Alloy, tools, formal methods, modelling, etc. in education?
Can Alloy technology be used as a back-end?
(20) Wrap-up: What's next?

6:30 Dinner