Introduction
This page contains supplementary material of the FSCD paper
A verified algorithm for deciding pattern completeness.
Formalization
The formalization can be inspected in a web-browser (compiled with Isabelle 2024 and AFP 2024).
Section 5.1
Section 5.2
Section 5.3
Section 5.4
Experiments
All tests have been executed using a MacStudio (Apple M2 Max processor)
running MacOS 14.3.1.
First, we use Isabelle's code generator to obtain our
verified decision procedure as Haskell code.
Next, both the decision procedure and the tree automata tests via FORT-h 2.0 have been
compiled using the Haskell compiler ghc version 9.4.7 with -O2.
For testing the pattern completeness test within GHC tests, ghc was invoked without -O2.
Finally, for the complement algorithm we used AGCP v0.02 which was compiled
using SML New Jersey v110.99.4.
The execution time of all experiments are displayed in this table. In the table, you can click on each experiment to see the input.
The timing information is provided in seconds (wall-clock time measurement).
Sources
The submitted sources (Isabelle / Haskell / SML) are available in this archive.
The archive also contains instructions how to rerun the experiments.
Rerunning OUR / GHC / CO / TA should be possible using Macos or Linux.
The Isabelle theories are part of the AFP, in entries Sorted Terms
and Verifying a Decision Procedure for Pattern Completeness.