Home

Committees

Call for Papers

Submission

Tutorials

Workshop

Program

---

Activities

Invited Speakers

Venue

Transportation

Hotels

Enjoy the area!

Weather

Contact

Tutorials - Monday, February 22, 2010

1. BART (B Automatic Refinement Tool) - Full Day
2. An Advanced Introduction to Alloy - Full Day

1- BART (B Automatic Refinement Tool) - Full day

Lilian Burdy, Clearsy

BART (B Automatic Refinement Tool) is a tool for automatizing the refinement of B machines. It aims at providing help for refining a B specification into an implementation (when refinement is used to convert a detailed B specification into a B0 implementation).

In this one-day tutorial, we will:

• introduce the BART tool and its integration in Atelier B,
• explain when it can be used and how to use it on simple examples.

We will also introduce interactive refinement notions by:

• describing the language used to write refinement rules,
• explaining how to use those rules to refine more complex examples and
• introducing the interactive refinement interface.

For this tutorial, attendees are requested to bring their personal laptop. A new version of Atelier B and BART will be distributed to participants for installation.

2- An Advanced Introduction to Alloy - Full day

Eunsuk Kang and Joseph Near, MIT

Alloy is a declarative modeling language based on first-order relational logic. The language is expressive enough to describe structurally complex systems, but simple enough to be amenable to fully automated anaysis. The Alloy Analyzer is equipped with a powerful model finder that can simulate traces of a system, visualize them, or search for counterexamples to a property.

This one-day tutorial on the Alloy Analyzer will be divided into two parts. In the first half, we will begin with an introduction to Alloy, and describe the essential features of the Alloy Analyzer, such as simulation, property checking, visualization, and debugging with an unsatisfiable core. In the second half, we will discuss more advanced topics, including different modeling idioms, meta-modeling features, and checking code against specifications.

The tutorial will be hands-on. We recommend that the participants bring laptops with Alloy 4 installed.