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. Current version of Predator is available on GitHub.

An extension of Predator for converting low-level pointer programs implementing list containers to high-level list container programs has been implemented. More information on this extension as well as its prototype implementation is available here.

A script to utilize multiple concurrently-running Predator analyzers with various setup is available here.

Awards

  • SV-COMP'24 — The 13th International Competition on Software Verification

    The Predator tool (PredatorHP) took part in the SV-COMP'24 and won gold medal in category MemSafety and won the ReachSafety-Heap sub-category.

  • SV-COMP'21 — The 10th International Competition on Software Verification

    The Symbiotic analyser (primarily developed at FI MU) using the Predator tool running on LLVM won gold medal in category MemSafety and gold medal in category SoftwareSystems.

  • SV-COMP'20 — The 9th International Competition on Software Verification

    The Predator tool (PredatorHP) took part in the SV-COMP'20 and won gold medal in category MemSafety and won the ReachSafety-Heap sub-category.

    The Symbiotic analyser (primarily developed at FI MU) using the Predator tool running on LLVM won silver medal in category MemSafety, gold medal in category SoftwareSystems, and silver medal in category FalsificationOverall.

  • SV-COMP'19 — The 8th International Competition on Software Verification

    The Predator tool (PredatorHP) took part in the SV-COMP'19 and won silver medal in category MemSafety and won the MemSafety-LinkedLists and MemSafety-Heap sub-categories.

  • SV-COMP'18 — The 7th International Competition on Software Verification

    The Predator tool (PredatorHP) took part in the SV-COMP'18 and won silver medal in category MemSafety and won the ReachSafety-Heap, MemSafety-Heap and MemSafety-LinkedLists sub-categories.

  • SV-COMP'17 — The 6th International Competition on Software Verification

    The Predator tool (PredatorHP) took part in the SV-COMP'17 and won gold medal in category MemSafety.

  • SV-COMP'16 — The 5th International Competition on Software Verification

    The Predator tool (PredatorHP) took part in the SV-COMP'16 and won gold medal in category Heap.

  • SV-COMP'15 — The 4th International Competition on Software Verification

    The Predator tool (PredatorHP) took part in the SV-COMP'15 and won one gold and one silver medal.

  •  FLoC Olympic Games 2014

    The Predator tool has been awarded the Kurt Gödel medal at the FLoC Olympic Games 2014 for its successes in three consecutive years of the international competition in software verification SV-COMP.

  •  SV-COMP'14 — The 3rd International Competition on Software Verification

    Predator won the silver medal in category Heap Manipulation and the bronze medal in category Memory Safety. Moreover, in these categories, it achieved the best result among tools with a sound treatment of dynamic memory (i.e., it achieved the best result among the tools dealing with memory in an unbounded way). Predator was the only tool that achieved the maximal possible score on the ProductLines benchmark. The soundness of Predator's verification approach was again confirmed on the Overall benchmark (consisting of 2868 case studies). If you want to reproduce the competition results, please download predator-2013-10-30-d1bd405.tar.gz and follow the instructions in the file README-SVCOMP-2014, which is included in the archive. The release predator-2013-10-30-d1bd405 was tuned to achieve competitive results in SV-COMP'14. As usually, numerous bug fixes, compatibility fixes, and performance improvements were included.

  •  SV-COMP'13 — The 2nd International Competition on Software Verification

    The Predator tool won three categories of the SV-COMP'13 competition.

  •  SV-COMP'12 — The 1st International Competition on Software Verification

    The Predator tool won one of the categories of the SV-COMP'12 competition.

Source Code

gitGitHub repository

Documentation

pdfTechnical Report 2012-04 (extended version of the SAS 2013 paper)
pdfSAS 2013 Presentation

Conference 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. Peringer, and T. Vojnar. Byte-Precise Verification of Low-Level List Manipulation. In Proc. of 20th Static Analysis Symposium — SAS'13, Seattle, USA, volume 7935 of LNCS, pages 214—237, 2013. Springer-Verlag.
  3. K. Dudka, L. Holík, P. Peringer, M. Trtík, and T. Vojnar. From Low-Level Pointers to High-Level Containers. In Proc. of 17th International Conference on Verification, Model Checking, and Abstract Interpretation — VMCAI'16, St. Petersburg, Florida, USA, volume of LNCS 9583, pages 431—452, 2016. Springer-Verlag.
  4. L. Holík, M. Kotoun, P. Peringer, V. Šoková, M. Trtík, and T. Vojnar. Predator Shape Analysis Tool Suite. In Proc. of 12th Haifa Verification Conference — HVC'16, Haifa, Israel, volume 10028 of LNCS, pages 202—209, 2016. Springer-Verlag.

Competition Contributions

  1. 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.
  2. 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.
  3. K. Dudka, P. Peringer, and T. Vojnar. Predator: A Shape Analyzer Based on Symbolic Memory Graphs. In Proc. of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS'14, Grenoble, France, volume 8413 of LNCS, pages 412—414, 2014. Springer-Verlag.
  4. P. Müller, P. Peringer, and T. Vojnar. Predator Hunting Party (Competition Contribution). In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS'15, London, UK, volume 9035 of LNCS, pages 443—446, 2015. Springer-Verlag.
  5. M. Kotoun, P. Peringer, V. Šoková, and T. Vojnar. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution). In Proc. of 22st International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS'16, Eindhoven, Netherlands, volume 9636 of LNCS, pages 942—945, 2016. Springer-Verlag.
  6. P. Peringer, V. Šoková, and T. Vojnar. PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution). In Proc. of 26st International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS'20, Dublin, Ireland, volume 12079 of LNCS, pages 942—945, 2020. Springer, Champ.

Predator Team

Acknowledgement

Over the years, the work on Predator was supported by the Czech Science Foundation (projecta P103/10/0306 and 14-11384S), 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, FIT-S-12-1, and FIT-S-14-2486.