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.


References in zbMATH (referenced in 18 articles )

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

  1. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  2. 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)
  3. Faisal Al Ameen, Mahmudul; Tatsuta, Makoto: Completeness for recursive procedures in separation logic (2016)
  4. Gu, Xincai; Chen, Taolue; Wu, Zhilin: A complete decision procedure for linearly compositional separation logic with data constraints (2016)
  5. Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
  6. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  7. Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben: Symbolic execution proofs for higher order store programs (2015)
  8. Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan; Yang, Hongli: Invariants synthesis over a combined domain for automated program verification (2013)
  9. Charlton, Nathaniel; Horsfall, Ben; Reus, Bernhard: Crowfoot: a verifier for higher-order store programs (2012)
  10. 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)
  11. Habermehl, Peter; Holík, Lukáš; Rogalewicz, Adam; Šimáček, Jiří; Vojnar, Tomáš: Forest automata for verification of heap manipulation (2012)
  12. Brotherston, James; Distefano, Dino; Petersen, Rasmus Lerchedahl: Automated cyclic entailment proofs in separation logic (2011)
  13. Habermehl, Peter; Iosif, Radu; Vojnar, Tomáš: Automata-based verification of programs with tree updates (2010)
  14. Luo, Chenguang; Craciun, Florin; Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan: Verifying pointer safety for programs with unknown calls (2010)
  15. Nguyen, An N.; Quan, Tho T.; Nguyen, Phung H.; Bui, Thang H.: COMBINE: a tool on combined formal methods for bindingly verification (2010) ioport
  16. Bansal, Kshitij; Brochenin, Rémi; Lozes, Etienne: Beyond shapes: Lists with ordered data (2009)
  17. Gast, Holger: Lightweight separation (2008)
  18. Nguyen, Huu Hai; David, Cristina; Qin, Shengchao; Chin, Wei-Ngan: Automated verification of shape and size properties via separation logic (2007)


Further publications can be found at: http://loris-7.ddns.comp.nus.edu.sg/~project/hip/index.html#papers