Please note: These pages are work in progress!



soter - Safety checker fOr The ERlang language!


soter [OPTIONS]... FILE

soter --stats module.erl
soter --dump --quiet module.erl


Soter is a program analyser for Erlang modules. It extracts an abstract (approximate sound) model from the source-code of the Erlang module and tries to verify safety properties of it using a powerful model checking back-end (BFC).

The name Soter derives from the Ancient Greek name of the spirit of safety, preservation and deliverance from harm.

Please Note: in order for Soter to work properly you need to have BFC installed in you system and the bfc executable must be in your PATH.

Output meaning:

Soter normally goes through three phases:

  1. Parsing of input Erlang module;
  2. Extraction of the abstract model;
  3. Verification of the properties (using BFC).

If phase 1 or 2 encounter errors, error messages get written to stderr and Soter terminates with exit code 1.

In phase 3, Soter will attempt to verify each of the specified properties in turn. The outcome of such attempts can be one of:



-f --fromcore

input is assumed to be in CoreErlang


do not apply simplification of ACS


use a Peano encoding of positive integers (use with care)

-m --main=FUN-NAME

the name of the function representing the entry point of the program; it must be of arity 0. The default is `main'


-d --dump -odir=[DIR]

dump all intermediate results to the specified directory; if no directory is specified, soter will use (and create if non existing) a directory with the name of the module in the directory of the module. The dumped files are described in the Output files section.

-s --stats

show statistics

-v --verbose

Loud verbosity

-q --quiet

Quiet verbosity


Reserved for future use


-A --prove-all

attempt to prove absence of any error

-a --prove-assertions

attempt to prove absence of assertion violations

-e --prove-no-error

attempt to prove absence of `error' exceptions

-u --prove --uncoverable=PROP

tells Soter to prove the specified property. See soter(7) for syntax.

--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. See soter(7) for syntax.

-D --val-depth=INT

specifies a depth for the data abstraction

-M --msg-depth=INT

specifies a depth for the message abstraction

--ct --cfa-timeout=INT

timeout for the CFA in seconds (no timeout if <= 0)

--bt --bfc-timeout=INT

timeout for the BFC verification in seconds (no timeout if <= 0)


-? --help

Display help message

-V --version

Print version information


The Erlang module supplied as input should follow these guidelines:

Refer to soter(7) for a detailed description of the current restriction on the Erlang programs accepted by Soter.

A tipical Erlang module that can be analysed by Soter looks like the following:



-uncoverable("wrong_incipit > 0").

main() ->
    N = ?any_nat(),
    P = spawn(fun()-> f(N) end),
    P ! {hi, self()} ,
        X -> X

f(N) ->
        {hi, P} ->
            P ! {hey, N}
            start_protocol(N, P);
        bla ->


See soter(7) for the full details.


Suppose FILE = examples/myfile.erl then after running soter on it you will find a new subdirectory of examples/ called myfile containing the following files:

This is the Core Erlang version of myfile.erl
This is the Intermediate Representation of the program
This is the full content of the output of the CFA
This file (meant to be used with is a Graphviz file showing the generated ACS in graphical form
The ACS model translated into the BFC input format. The ids of the local states coincide with the ones displayed in the nodes of the ACS in the dot file
These files correspond to translations of the ACS after simplification
This contains a summary of the performance
This contains the results of the verification of each property.



Soter deals with a `pure' core fragment of the Erlang language. See soter(7) for details.

Reporting Bugs

Email bug reports to

Known Bugs

Soter can be very slow for big inputs. Use with care.


BFC is a program by Alexander Kaiser and can be downloaded at

Details on the syntax for properties can be found at soter(7)