Predator

Predator is a tool for automated formal verification of sequential C programs operating with pointers and linked lists. The core algorithms of Predator were originally inspired by works on separation logic with higher-order list predicates, but they are now purely graph-based and significantly extended to support various forms of low-level memory manipulation used in system-level code. Such operations include pointer arithmetic, safe usage of invalid pointers, block operations with memory, reinterpretation of the memory contents, address alignment, etc. The tool can be loaded into GCC as a plug-in. This way you can easily analyse C code sources, using the existing build system, without manually preprocessing them first. The analysis itself is, however, not ready for complex projects yet. The plug-in is based on Code Listener infrastructure (included). Although the tool is intended to be as portable as GCC is, we support only Linux for now.

News

 predator-2013-02-02-8d3ea3d is out!
The new version of Predator uses an improved algorithm for live variable analysis (based on points-to analysis) contributed by Pavel Raiskup. The improved live variable analysis makes the shape analysis running 3x faster in certain cases, for instance on test-0124.c (an implementation of the Merge-Sort algorithm).
 SVCOMP'13 — Predator succeeded in the 2nd International Competition on Software Verification!
Predator is the winner in the FeatureChecks, HeapManipulation, and MemorySafety categories of the 2nd International Competition on Software Verification held at TACAS 2013 in Rome, Italy. If you want to reproduce the competition results, please download the competition candidate and follow the instructions in the file README-sv-comp-TACAS-2013, which is included in the archive.

Build from Sources

textREADME-fedora
textREADME-ubuntu
textREADME
curl http://www.fit.vutbr.cz/~idudka/download/predator-2013-02-02-8d3ea3d.tar.gz \
    | gzip -cd \
    | tar x

cd predator-2013-02-02-8d3ea3d

./switch-host-gcc.sh /usr/bin/gcc

Usage

To employ the Predator plug-in in a build of an arbitrary project fully transparently, it is recommended to set certain environment variables. You can use the script register-paths.sh to do this automatically:

. sl_build/register-paths.sh

Then you can simply use the -fplugin option of GCC as documented in the gcc(1) man page:

gcc -fplugin=libsl.so ...

This will show you the available options of the Predator plug-in itself:

echo please help | gcc -fplugin=libsl.so -fplugin-arg-libsl-help -xc -

Source Code

tgzpredator-2013-02-02-8d3ea3d.tar.gz
gitgit repository

Documentation

textREADME
pdfPresentation (CAV '11)
linkAPI documentation

Related Papers

  1. K. Dudka, P. Peringer, and T. Vojnar. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. In Proc. of 23rd International Conference on Computer Aided Verification - CAV'11, Cliff Lodge, Snowbird, Utah, USA, volume 6806 of LNCS, pages 372--378, 2011. Springer-Verlag.
  2. K. Dudka, P. Müller, P. Peringer, and T. Vojnar. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. In Proc. of 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'12, Talinn, Estonia, volume 7214 of LNCS, pages 545--548, 2012. Springer-Verlag.
  3. K. Dudka, P. Müller, P. Peringer, and T. Vojnar. A Tool for Verification of Low-level List Manipulation. In Proc. of 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'13, Rome, Italy, volume 7795 of LNCS, pages 627--629, 2013. Springer-Verlag.

Predator Team

Acknowledgement

This work was supported by the Czech Science Foundation (project P103/10/0306), the Czech Ministry of Education, Youth, and Sports (projects COST OC10009 and MSM 0021630528), the EU/Czech IT4Innovations Centre of Excellence CZ.1.05/1.1.00/02.0070, and the internal Brno University of Technology projects FIT-S-11-1 and FIT-S-12-1.