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 24 articles )

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

1 2 next

  1. Fiedor, Tomáš; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš: Nested antichains for WS1S (2019)
  2. Ta, Quang-Trung; Le, Ton Chanh; Khoo, Siau-Cheng; Chin, Wei-Ngan: Automated mutual induction proof in separation logic (2019)
  3. Tatsuta, Makoto; Chin, Wei-Ngan; Al Ameen, Mahmudul Faisal: Completeness and expressiveness of pointer program verification by separation logic (2019)
  4. Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W.: VST-Floyd: a separation logic tool to verify correctness of C programs (2018)
  5. Chen, Taolue; Song, Fu; Wu, Zhilin: Tractability of separation logic with inductive definitions: beyond lists (2017)
  6. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  7. 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)
  8. Faisal Al Ameen, Mahmudul; Tatsuta, Makoto: Completeness for recursive procedures in separation logic (2016)
  9. Gu, Xincai; Chen, Taolue; Wu, Zhilin: A complete decision procedure for linearly compositional separation logic with data constraints (2016)
  10. Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
  11. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  12. Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben: Symbolic execution proofs for higher order store programs (2015)
  13. Sharma, Asankhaya; Wang, Shengyi; Costea, Andreea; Hobor, Aquinas; Chin, Wei-Ngan: Certified reasoning with infinity (2015)
  14. Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan; Yang, Hongli: Invariants synthesis over a combined domain for automated program verification (2013)
  15. Charlton, Nathaniel; Horsfall, Ben; Reus, Bernhard: Crowfoot: a verifier for higher-order store programs (2012)
  16. 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)
  17. Habermehl, Peter; Holík, Lukáš; Rogalewicz, Adam; Šimáček, Jiří; Vojnar, Tomáš: Forest automata for verification of heap manipulation (2012)
  18. Brotherston, James; Distefano, Dino; Petersen, Rasmus Lerchedahl: Automated cyclic entailment proofs in separation logic (2011)
  19. Habermehl, Peter; Iosif, Radu; Vojnar, Tomáš: Automata-based verification of programs with tree updates (2010)
  20. Luo, Chenguang; Craciun, Florin; Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan: Verifying pointer safety for programs with unknown calls (2010)

1 2 next


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