Program
Verification
Book

PV1 ⊧ APOETanalyses a multi-threaded program to see if it conforms to expectations of the tool

Program analyser based on abstract unfoldings.

Application domain/field

Abstract interpretation
Concurrent programs

Expected input

Concurrent C program that uses the POSIX thread library
Parameters to control the widening level and the use of cutoffs

Internals

The exploration strategy in this tool is based on POET.

Comments

Note that the author calls "APOET" the second version of "POET".

C Concurrency Haskell

Links

Repository (CAV '17 release): https://github.com/marcelosousa/poet/tree/RELEASE-CAV-2017
- Last commit date: 19 Oct 2018 (default branch)
Repository (of POET): https://github.com/marcelosousa/poet
- Last commit date: 19 Oct 2018 (default branch)
Last commit date: marcelosousa/poet 19 Oct 2018 (default branch)
Last commit date: 19 Oct 2018 (last activity)

Related papers

Abstract Interpretation with Unfoldings (CAV '17)

Last publication date

13 July 2017

Related tools

AstreeA, Impara, CBMC

ProVerB specific

Markdown description: view/edit
Reason for this entry: CAV 2017
Contained in the ProVerB22 dataset (paper + artefact)

ProVerB is a part of SLEBoK. Last updated: February 2023.