Predator

Predator: a tool for verification of low-level list manipulation. (Competition contribution) 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. This paper briefly introduces Predator and describes its participation in the Software Verification Competition SV-COMP’13 held at TACAS’13.


References in zbMATH (referenced in 13 articles , 2 standard articles )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Guthmuller, Marion; Corona, Gabriel; Quinson, Martin: System-level state equality detection for the formal dynamic verification of legacy distributed applications (2018)
  2. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  3. Li, Huisong; Berenger, Francois; Chang, Bor-Yuh Evan; Rival, Xavier: Semantic-directed clumping of disjunctive abstract states (2017)
  4. Reynolds, Andrew; Iosif, Radu; Serban, Cristina: Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic (2017)
  5. Brotherston, James; Gorogiannis, Nikos; Kanovich, Max; Rowe, Reuben: Model checking for symbolic-heap separation logic with inductive predicates (2016)
  6. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
  7. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  8. Beyer, Dirk: Second competition on software verification. (Summary of SV-COMP 2013) (2013) ioport
  9. Dudka, Kamil; Müller, Petr; Peringer, Petr; Vojnar, Tomáš: Predator: a tool for verification of low-level list manipulation. (Competition contribution) (2013) ioport
  10. Iosif, Radu; Rogalewicz, Adam; Simacek, Jiri: The tree width of separation logic with recursive definitions (2013)
  11. Dudka, Kamil; Müller, Petr; Peringer, Petr; Vojnar, Tomáš: Predator: a verification tool for programs with dynamic linked data structures (competition contribution) (2012) ioport
  12. Habermehl, Peter; Holík, Lukáš; Rogalewicz, Adam; Šimáček, Jiří; Vojnar, Tomáš: Forest automata for verification of heap manipulation (2012)
  13. Dudka, Kamil; Peringer, Petr; Vojnar, Tomáš: Predator: A practical tool for checking manipulation of dynamic data structures using separation logic (2011) ioport