Synopsis: Alloy is used as one of the steps in a "all-in-one" verification approach which includes model checking with model animation in VDM and theorem proving in HOL. The theoretical underpinning is that of the point-free transform and relational calculus, which blends with Alloy in a natural way. In practice, Alloy is very helpful in finding counter examples to proof obligations.

Learning outcomes: This unit stems from more than 20 years of experience at Minho in teaching, researching and applying rigorous methods in the construction of software. By resorting to the formal foundations of modelling, reasoning, programming and testing, this unit bears a special mark into the way future professionals are trained to meet high-quality standards in the design of software solutions to real-life problems.

Credits: 30 ECTS

Institution: University of Minho

Degree: MSc in Computer Science