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 18 articles , 2 standard articles )

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

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