erlang2trs

erlang2trs is a tool for transforming Erlang programs into term rewrite systems so that existing techniques and tools for rewrite systems can be used.

It takes as input an Erlang program with the following restricted syntax:

• variables must start with an uppercase,
• atoms should be prefixed with "atom_"
• comments to the right of Erlang code are not allowed
• spawn and self can only appear in the right-hand side of a pattern matching equation

An example program follows (you can find more examples in the web interface tab):

% A simple sequence of calls;

proc1 -> Pid1 = spawn(proc2),
         Pid1 ! atom_a.

proc2 -> Pid2 = spawn(proc3),
         receive 
            X -> Pid2 ! X
         end.

proc3 -> receive 
            X -> atom_ok
         end.

A technical description of the transformation can be found in this paper:

• Germán Vidal. Towards Erlang verification by term rewriting. LOPSTR 2013. PDF

Check the web interface in the next tab (a simple text-only page with the source and target programs can be found here).

Please let me know if you have any question or comment to gvidal@dsic.upv.es.

Source program (you can load in an example and edit it)

Choose a file: select a file examples/e1 examples/e2 examples/e3 examples/e4 examples/e5 examples/e6 clear         START

Curry program generated:

The transformed programs can be executed in Curry. Moreover, they include an initial call "init" that can be used to check them.