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