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