Alloy has been used as a teaching tool in the following courses offered by MIT and other universities:
6.894 Lightweight Formal Methods
Daniel Jackson (Lecturer)
Robert Seater (TA)
MIT (Spring 2005)
Synopsis: Software is everywhere. Bad software makes life miserable and is likely, eventually, to result in catastrophes. The old ways of developing software from vague specs and designs, by trial and error, with minimal tool support won't produce the radical improvement that's needed. Lightweight formal methods is a new approach that combines classical ideas of formal specification and verification with new automatic checking technologies, and a more cost-effective and risk-driven style.
Students will read classic technical papers and articles on broader issues; will get a grounding in the big ideas of formal methods; and will become proficient in using the latest lightweight methods for software design, specification and programming. The Alloy language will be used in the first half of the course to demonstrate modeling patterns and approaches, but the focus will not be the specifics of that language. The second half of the course will introduce a variety of other tools, including ESC/Java and NuSMV. Students will work on final projects in small teams.
6.170 Laboratory in Software Engineering
Daniel Jackson and Paul Fitzpatrick
MIT (Fall 2004)
Synopsis: This course is a a core electrical engineering computer science subject at MIT. It introduces concepts and techniques relevant to the production of large software systems. Students are taught a programming method based on the recognition and description of useful abstractions. Topics include: modularity; specification; data abstraction; object modeling; design patterns; and testing. Several programming projects of varying size undertaken by students working individually and in groups.
Advanced Topics in Software Design
MIT (Spring 2002)
Synopsis: Topics are likely to include: modelling languages (Alloy, JML); programming language constructs for expressing design (functors, typeclasses, units, mixins, aspects); classification of problems and solutions (problem frames, analysis patterns, design patterns); decoupling theories (axiomatic design, design structure matrices, module dependences).
GS03/4023 Validation and Verification
Spring 2007, University College London
Aims: The course will train students in the
principles and techniques of validating and verifying complex
software systems. The training will be at an intellectually
demanding level and will cover not only the state-of-the practice
in validation and verification, but also the most significant
trends, problems and results in validation and verification
research.
Learning Outcomes: On completion of the course unit, the
successful student should have a good knowledge and understanding
of basic notions of correctness, consistency, faults and
failures, testing and execution trace analysis. The successful
student should also be able to understand the use of logic as a
formal language for specification of systems, to understand the
use of the main verification techniques used in symbolic model
checking, to understand the architecture and be able to use a
main tool (such as SMV) to verify simple systems. Further,
successful students will be able to appreciate the limitations of
the current tools and have insights in ongoing advanced research
topics to overcome them.
CS 643 Formal Verification of Software
Stevens Institute of Technology, Fall 2004
Upon completion of this course, you will be familiar with the scope and limits of formal verification, including the role of semantics, major specification approaches, and feasibile automated support. You will be familiar with rules for proving correctness of sequential code including loops as well as concurrent programs. You will be skilled in the use of first order predicate logic to specify structural models of software including invariants and operation transitions. You will be skilled in the use of the Alloy tool for checking such specifications and generating test examples from them. You will be skilled in the use of the ESC/Java-2 tool for verification of method implementations with respect to specifications.
University of Washington, Spring 2004
The PhD qualifying course in Software Engineering, with a focus on formal methods and architectural-level design.
SOFTENG 461 - Special Topic in Software Engineering 1
Dr. Jing Sun (coordinator) and Dr. John Hamer.
University of Auckland, New Zealand, 2004
SOFTENG 461 looks at the formal specification, design, and (automatic) analysis of software systems. A variety of specification notations will be presented, including Alloy, Z and OCL. The course compares the various approaches, with an emphasis on their practical application.
Corso di Ingegneria del Software 1
Select "Accesso libero" for free access, then "V facolta' di Ingegneria-Ingegneria dell'informazione", and then finally "Ingegneria del Software 2 (Carlo Ghezzi)".
Pietro Braione and Carlo Ghezzi
Politecnico di Milano (the Polytechnic University of Milan), 2003-2004
Synopsis: The slides of the course (in English) can be found on the page of the course (in Italian). To download the slides you must select "Materiale" on the top.
5309V, 7009T2, 7009U2 (a portuguese course using Alloy for projects)
Universidade do Minho, Portugal
Synopsis: Esta opcao destina-se preferencialmente a alunos que tenham frequentado MFP-I e MFP-II.
Nesta opcao pretende-se que os alunos tomem contacto com ferramentas que hoje existem no mercado de uso comercial e industrial, por exemplo, o Toolkit para VDM-SL da IFAD, o RAISE, o B-method etc.
Tratando-se de uma disciplina para finalistas, pretende-se desenvolver (ainda que no contexto dos Metodos Formais) um conjunto de `soft-skills' essenciais a qualquer tecnico de informatica dos dias de hoje. Exige-se organizacao e espirito cooperativo por parte dos alunos.
22c:181 - Formal Methods in Software Engineering
The University of Iowa, Spring 2003
Synopsis: In this course, we will study a collection of techniques for formal software development, spanning the whole development process: from high-level semantic modeling, to system architecture design, to coding and debugging. The study will be done not in the abstract, however, but through the use of actual tools supporting these techniques. In particular, we will study and use:
CISC 422: Formal Methods in Software Engineering
Juergen Dingel
Queen's University (Winter 2001, Winter 2002)
Synopsis: CISC422 is an introduction to the formal specification, design, and automatic analysis of software artifacts. The course presents a variety of specification notations (propositional and predicate logic, Z, Alloy, UML/OCL, temporal logic), and discusses corresponding analysis techniques (theorem proving, constraint checking, animation, model checking) using existing commercial and research tools (Jape, Z/Eves, Alloy, USE, SMV). The course compares the various approaches and attempts to balance theory (e.g., discussing theorems) and practise (e.g., discussing tools).
C475 Software Engineering -- Environments
Susan Eisenbach and Michael Huth
Imperial College London, United Kingdom, Fall 2002
Synopsis: We stress the need for formal object modeling languages for the design of large and complex sofware artefacts. We study one such language, Daniel Jackson's Alloy (MIT) in detail. In presenting Alloy, we will discuss the aspects and trade-offs of its design decisions. We then use Alloy to formally model current software designs in the realm of mobility, security, and (possibly) wireless computing. Time permitting we may compare Alloy to two other modelling languages: UML and Z.
CS4211 Advanced Software Engineering
National University of Singapore (Fall 2002)
Synopsis: This course introduces students to problems that occur in large scale software production. The course examines technical aspects of software development life cycle and stresses a model driven approach to software engineering. Formal (mathematical and logic based) approaches to software modeling are covered and emphasized. A number of advanced software engineering topics will be studied:
CS 525V : Introduction to Computer-Aided Verification
WPI, Spring 2002
If you designed a new system or protocol, would you sign a liability contract guaranteeing that your design met its requirements? Do you wish that software and hardware companies would replace disclaimers with warranties? (wording adapted from D.L. Parnas)
Synopsis: As computer systems and protocols grow increasingly complex, detecting errors in their designs becomes increasingly difficult. The growing use of computer systems in safety-, life-, and financially-critical applications demands validation techniques that guarantee the absence of certain classes of errors. Testing, however, can never guarantee that systems are error-free. What's a designer to do?
Computer-aided verification complements conventional testing with techniques for formally proving that designs satisfy certain behavioral requirements (such as "every request is eventually acknowledged"). Major semiconductor companies use these techniques on many systems, including cache coherence protocols, floating point units, communication protocols, and pipelined architectures. Agencies such as NASA use these techniques to validate aspects of critical systems (such as deep space probes).
This seminar will explore the theory and practice of computer-aided verification. We will study techniques for modeling systems and specifying and verifying their behavior. This year, the course will focus on modeling and specifying software systems, though we may look at simple circuits and protocols at the start of the semester for comparison. Assignments will involve paper reading and presenting, pencil and paper exercises, and using software tools to verify designs.
Software Specification (CIS 771)
Kansas State University (Spring 2002)
Synopsis: This course emphasizes tool-based formal specification methods and focuses on Alloy (5 weeks of lecture material), OCL/USE (5 weeks of lecture material), and ESC/Java (2 weeks of lecture material). A downloadable archive is available for instructors that includes a variety of pedagogical materials such as PowerPoint lecture slides, links to streaming video recordings of lectures, sources for lecture examples, weekly quizzes and solutions, homeworks and solutions, and exams and solutions. A separate distribution for students includes only the lecture slides and examples.
222 Formal Methods in Software Engineering
University of California, Irvine (Winter 2001)
Synopsis: Examination of formal specification models, including algebraic/axiomatic, state-transition, model-based, operational, and temporal logics, along with their related analysis techniques. Formal models in software development are discussed as are different proof techniques.
CSE814: Formal Methods in Software Development
Michigan State University, Fall 2001
Synopsis: Formal methods are used to precisely specify and reason about the behaviors of software systems. This course surveys several methods with an emphasis on methods that support reasoning about specifications and designs. Three themes will pervade our survey:
CS 599 Formal Methods in Software Architectures
University of Southern California (Fall 2000)
Synopsis: This course will expose students to formal specification methods, with a particular focus on those used in software architectures. A secondary focus of the class will be on the many software development activities, including architecture, that benefit from the use of formal methods. Several categories of formal methods will be studied, including algebraic, axiomatic, model-based, state-based, and temporal. Specific modeling formalisms within each category will be highlighted and their applicability to software architectures assessed. Students will study different types of formal specification languages and utilize specific languages to describe software systems.