HIP
The HIP/SLEEK systems are aimed at automatic verification of functional correctness of heap manipulating programs. HIP is a separation logic based automated verification system for a simple imperative language, able to modularly verify the specifications of heap-manipulating programs. The specification language allows user defined inductive predicates used to model complex data structures. Specifications can contain both heap constraints and various pure constraints like arithmetic constraints, bag constraints. Based on given annotations for each method/loop, HIP will construct a set of separation logic proof obligations in the form of formula implications which are sent to the SLEEK separation logic prover. SLEEK is a fully automatic prover for separation logic with frame inferring capability.
Keywords for this software
References in zbMATH (referenced in 11 articles )
Showing results 1 to 11 of 11.
Sorted by year (- Abdulla, Parosh Aziz; Holík, Lukáš; Jonsson, Bengt; Lengál, Ondřej; Trinh, Cong Quy; Vojnar, Tomáš: Verification of heap manipulating programs with ordered data by extended forest automata (2016)
- Faisal Al Ameen, Mahmudul; Tatsuta, Makoto: Completeness for recursive procedures in separation logic (2016)
- Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
- Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben: Symbolic execution proofs for higher order store programs (2015)
- Chin, Wei-Ngan; David, Cristina; Nguyen, Huu Hai; Qin, Shengchao: Automated verification of shape, size and bag properties via user-defined predicates in separation logic (2012)
- Habermehl, Peter; Holík, Lukáš; Rogalewicz, Adam; Šimáček, Jiří; Vojnar, Tomáš: Forest automata for verification of heap manipulation (2012)
- Habermehl, Peter; Iosif, Radu; Vojnar, Tomáš: Automata-based verification of programs with tree updates (2010)
- Luo, Chenguang; Craciun, Florin; Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan: Verifying pointer safety for programs with unknown calls (2010)
- Nguyen, An N.; Quan, Tho T.; Nguyen, Phung H.; Bui, Thang H.: COMBINE: a tool on combined formal methods for bindingly verification (2010)
- Nguyen, Huu Hai; David, Cristina; Qin, Shengchao; Chin, Wei-Ngan: Automated verification of shape and size properties via separation logic (2007)
- Sevcík, Jaroslav: Proving resource consumption of low-level programs using automated theorem provers. (2007)
Further publications can be found at: http://loris-7.ddns.comp.nus.edu.sg/~project/hip/index.html#papers