FORTissimo — TACAS 2021  

Description

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


FORT-h


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

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. In addition, (ground) commutation of COPS#1118 can be certified in 2 minutes and 57 seconds.