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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

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

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

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