Description

This page accompanies a paper that will appear in the proceedings of TACAS 2021. The corresponding artifact can also be downloaded.

FORT-h

• precompiled binaries for Linux and MacOS
• Description: FORT-h

FORTify

• precompiled binaries for Linux and MacOS
• Description: FORTify

FORTify is based on the formalization of a decision procedure for the first-order theory of rewriting described in this paper.

Certificates

Certificates are formal expressions according to the following grammar.

Experiments

FORT-h (+ FORTify) vs FORT 2.0

• Table 1
• Table 2
• Table 3

Certification

The following tables show the experiments we performed with FORTify. Here FORT-h was run with a 60 seconds timeout and the produced certificate was passed on to FORTify with a 600 seconds timeout.

• normalization
• termination
• (1) groundness and (2) existence of a function symbol of arity > 1

In addition, (ground) commutation of COPS#1118 can be certified in 2 minutes and 57 seconds.