Skip to content
Marcelo Sousa edited this page Oct 19, 2018 · 2 revisions

Abstract Interpretation with Unfoldings

Abstract Interpretation with Unfoldings was the second version of POET baptized APOET presented at the conference CAV in 2017. The paper is available here! Below are the instructions to reproduce APOET's results presented in the paper.

Installation

POET can be installed at least up to GHC-8.0.1.

To install POET follow the steps:

  1. Install the Haskell Platform.

    Test that your installation was successful by running the commands ghc, cabal, and happy.

  2. Install the second release of POET's front-end called simple-c which can be found here

  3. Install the second release of POET which can be found here

If you simply interested in running POET please contact me for binaries.

Reproducing experimental results

The benchmarks used by POET can be found in the repository con-benchmarks. The particular benchmarks used in the CAV 2017 paper are here. For more information about the benchmarks read the README. Since the poet front-end is still experimental and does not accept the standard C language, for each benchmark there is a version for poet and another for cprover's analysers cprover.

Both directories contain bash scripts to reproduce the experiments as well as the logs with the information used in the paper.

Clone this wiki locally