Your Erlang Program
  1. Write your code in the editor or load an example.
  2. Set your options:
    • "Analysis Only" does not verify any property, it just generates the ACS,
    • "Verify Absence-of-Errors" checks absence of runtime exceptions (e.g. sending to a non-pid),
    • "Verify Assertions" checks safety of all the properties specified in the code,
    • "Verify All" verifies 2 and 3.
  3. Press Run. Your results will be rendered here. In the panel below you will find a graphical representation of the generated ACS. Click on it to view it in a larger window.

Please refer to the documentation for more details.

This model can be saved and verified with BFC.
  • No example loaded

Select an example from the list on the left: you will be able to see a description here and a preview of the first lines of the code below.

You will also be able to download the example as an Erlang source file that can be executed with the Erlang interpreter. In that case make sure you dowloaded soter.erl soter.hrl grammars.hrl.

Press Ok to load the example.


            

DOs

  • Enter valid Erlang code, or
  • Load Examples with the dialog
  • Write assertions using the -uncoverable directive
  • You can use all the macros defined in soter.hrl and grammars.hrl as they are included by default
  • Press Run to run Soter on your code and wait for the answer

DON'Ts

  • Do not call primitives besides spawn, self and send (Pid ! Msg)
  • Do not call functions in external modules
  • Do not use -module, -include or -include_lib directives
  • (see Limitations for a detailed description of the features of Erlang not supported by Soter)

See Erlang.org for more details about the Erlang Language

See Soter Documentation for more details about using Soter

See Full Paper for more details about how Soter works

Oxford University

SOTER 0.1 web interface

Safety verifier fOr The ERlang language

Emanuele D'Osualdo

Jonathan Kochems

Luke Ong

Department of Computer Science, Oxford University