Your Erlang Program
- Write your code in the editor or load an example.
- 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.
- 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.
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
Press Ok to load the example.
- Enter valid Erlang code, or
- Load Examples with the dialog
- Write assertions using the
- You can use all the macros defined in
as they are included by default
- Press Run to run Soter on your code and wait for the answer
- Do not call primitives besides
self and send (
Pid ! Msg)
- Do not call functions in external modules
- Do not use
- (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
Safety verifier fOr The ERlang language
Department of Computer Science, Oxford University