Description

This page accompanies a submission to the Journal of Automated Reasoning.

Tools

FORT-h

• precompiled binaries for Linux and MacOS
• description
• source

FORTify

• precompiled binaries for Linux and MacOS
• description

FORT-s

• precompiled binaries for Linux and MacOS
• description
• source

Certificates

Certificates are formal expressions according to the following grammar.

Experiments

Comparing different representations of properties

• GCR
• GNFP
• Encodings of conversion (<->*)
• Encodings of NF

Properties involving multiple TRSs

• GCOM
• CE/NE

Optimizations

• Lemma 29: "UNC" vs "{+2} GUNC"
• Collapsing epsilon-transitions: Consistency

Comparison with other tools

• GCR
• NFP
• UNC
• UNR
• COM