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 myfile.bfc
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 myfile.simpl.*
These files correspond to translations of the ACS after simplification myfile.stats
This contains a summary of the performance myfile.results
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)