CARPA: Counter examples in
Abstract Rewriting Produced Automatically
The tool Carpa automatically generates examples of finite abstract
rewrite systems satisfying a given list of properties
The tool Carpa+ reads a similar list of properties, but instead generates a term rewriting system
satisfying the given list of properties
Internally, first a SAT/SMT fomula is created representing the
specified properties. Then the tool
Yices is called
for doing the real work. Finally, from the Yices output the
desired output is created.
The following can be downloaded:
- A paper
presenting the tool Carpa and the underlying theory (accepted for publication in Mathematical
Structures in Computer Science).
- A manual
presenting the input format of Carpa.
- A zip file containing source files and
a Linux executable for Carpa. It also contains all examples from the
paper.
- The paper Automatically finding particular term
rewriting
systems
presenting the tool Carpa+ and the underlying theory.
- A zip file containing source files and
a Linux executable for Carpa+ and all examples from the paper.
Last change: July 12, 2018