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 9 articles , 2 standard articles )
Showing results 1 to 9 of 9.
- 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)
- Beyer, Dirk: Second competition on software verification. (Summary of SV-COMP 2013) (2013)
- Dudka, Kamil; Müller, Petr; Peringer, Petr; Vojnar, Tomáš: Predator: a tool for verification of low-level list manipulation. (Competition contribution) (2013)
- 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)
- 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)