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)

1. Introduction to {log}
2. Specifying state machines in {log}
3. Running {log} state machines
4. Automatic verification of state machines in {log}
5. If automatic verification fails...
6. 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.