**ABZ 2023 Tutorial on {log}**

**{log}: Programming and Automated Proof in Set Theory**

{log} (read setlog) is a programming language and satisfiability solver

based on set theory and set relation algebra, implementing the concept of

*formulas as programs*---as an alternative approach to
*formulas as types*

or *proofs as programs*.

As a programming language it is at the intersection of Constraint

Logic Programming, set programming and declarative programming. As a

satisfiability solver {log} implements several decision procedures for

the theory of finite sets and finite set relation algebra.

In {log} one can write abstract programs using all the power of set theory

and binary relations. These programs can resemble B or Z specifications.

Then, the correctness of {log} programs is more evident than if they were

written in conventional programming languages. Furthermore, {log}

programs are also set formulas. Hence, engineers can use {log} again to

*automatically* prove their programs verify non trivial properties.

We call the capacity of {log} code to behave as a formula and as a program,

the *formula-program duality*; actually, in {log} one can write *forgrams*

instead of plain programs.

If you want to know more about {log} before deciding whether or not you

are interested in the tutorial take a look at this short introduction and check

out the {log} site.

**Instructor:** Maximiliano Cristiá (cristia -at- cifasis-conicet.gov.ar),

professor of Software Engineering at Universidad Nacional de Rosario,

Argentina.

This tutorial is based on courses and seminars given at Argentina, Italy

and Luxembourg.

**Outline** (duration 2-3 hours)

- Introduction to {log}
- Specifying state machines in {log}
- Running {log} state machines
- Automatic verification of state machines in {log}
- If automatic verification fails...
- How {log} works?

**Resources UPDATED** (May 28th)

- Slides
**NEW !!!** - {log} web site
- {log} version that will be used during the tutorial
**NEW VERSION !!!** - {log} user's manual
- Class notes on translating B machines into {log}
- Class notes on translating Z specifications into {log}

**Prerequisites:** Participants are expected to have a working

knowledge in at least one of the specification languages making part of the

ABZ 2023 conference. Put it in another way, participants are expected to

have an idea of how state machines can be specified by means of set theory.

Besides, participants are encouraged to bring their computers so they

can have a hands-on experience on {log}. Prior to attending the tutorial

we recommend to install SWI-Prolog.