Please note: These pages are work in progress!


This manual page illustrates the various methods for the specification of properties of Erlang modules in Soter.





[long textual description:] label[bound], ... .

Properties Specification

There are currently two methods to specify properties:

  1. Through assertions
  2. Asking soter to prove absence of error using the --prove-no-error switch

In the following section we present the syntax of assertions and the three methods to feed them into Soter:

  1. Through assertions in the code
  2. Writing assertions in a .prop file
  3. Specifying a property with the --prove=PROP switch

Syntax of assertions

A single property is a list of constraints:

constr1, constr2, ..., constrn

each constraint constri can be one of:

If a label is used in more than one constraint of the same property

l >= n1, ..., l >= n2, ..., l >= nk

then these "matching" constraints all together are equivalent to the single constraint

l >= n1+ n2+ ... + nk

so for example a >= 10, b, a, a, b>0 is equivalent to a >= 12, b >= 2.

A run of a program is represented by a sequence of states. A given state meets a constraint l >= n just if there are at least n processes running an instruction labelled with l at that point.

A configuration is a "bad state" wrt to a property constr~1, constr~2, ..., constr~n if it meets all the constraints.

When asked to prove such a property, Soter will try to prove that no reachable state is a bad state wrt to that property. This kind of verification problem is called coverability check hence the `uncoverable' in the names for the assertion macros.


There are two main ways of putting assertions in the code (and they can be freely mixed).

The first method uses the ?label macro to label the relevant program points and then uses the directive


to specify a property involving those labels. As many property as needed can be specified with this method using multiple -uncoverable directives.

The second method uses inline assertions in the code via the macros explained in the dedicated section below.

Once you annotated your code with these assertions, to get them proved by Soter you need to use the --prove-assertions switch.

Inline Assertions


Properties file

Note: this method is available only when using the soter command-line tool, not the web interface.

A property file consists of:

For example:

% This is a comment
Property description:
    label1 >= 10,
    label2 > 3,
    label3, label3.

Another property: % Please document your properties!
    label > 0.

is a legal .prop file containing two properties.

When the mentioned labels are not specified in the code being analysed, the property containing them are simply ignored (and a warning is reported; warnings are only visible in verbose mode).

To ask Soter to prove the properties listed in a .prop file, use the --prop[=FILE] switch.

Single property

A single property can be specified with the switch --prove=PROP. Soter will try to prove PROP among the properties specified with the other methods.

Proving Absence Of Errors

When in "Verify Absence-of-Errors" mode, Soter will try to prove that no process will ever be in a state of error, i.e. an uncaught runtime exception. There is a limited set of such errors which are currently modelled by Soter:

One major omission is pattern-matching errors. Soter is currently ignoring them. The next release of Soter will feature a more precise abstract pattern-matching mechanism that will allow for pattern-matching errors to be detected avoiding too many false-alarms.

Please note that the exception handling features of Erlang, such as catch, are not currently supported by Soter. We aim to add support for them in the next release.

The Soter Macros

In order to write assertions in an Erlang module, Soter provides a set of macros defined in the file soter.hrl that can be imported by putting


after the -module directive and before any definition.

The header file grammars.hrl defines some commonly used non-deterministic generator of inputs (see non determinism). It depends on soter.hrl and must be imported with


after every other include since it defines functions rather than macros.

Important: The inclusion of soter.hrl and grammars.hrl is automatic and implicit in the web interface; the -module and the -include_lib directives should not be used in the web interface.

Relevant Options

The full options for soter are described in soter(1). The following applies to the offline use of the tool only.

Here we list only the options which are relevant to property specifications:

-A --prove-all

attempt to prove absence of any error

-e --prove-no-error

attempt to prove absence of `error' exceptions

-a --prove-assertions

attempt to prove absence of assertion violations

-u --prove --uncoverable=PROP

tells Soter to prove the specified property.

--prop[=FILE] --prove-file

tells Soter to prove every property specified in the .prop file. If no file is specified Soter will attempt to read a .prop file with the same basename of the input Erlang module.

There are two options by which you can manually control the data abstraction parameters:

-D --val-depth=INT

specifies a depth for the data abstraction

-M --msg-depth=INT

specifies a depth for the message abstraction