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

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

1 2 next

  1. Havlena, Vojtěch; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš: Automata terms in a lazy (\mathrmWSk\mathrmS) decision procedure (2021)
  2. Illous, Hugo; Lemerre, Matthieu; Rival, Xavier: A relational shape abstract domain (2021)
  3. Neider, Daniel; Madhusudan, P.; Saha, Shambwaditya; Garg, Pranav; Park, Daejun: A learning-based approach to synthesizing invariants for incomplete verification engines (2020)
  4. Fiedor, Tomáš; Holík, Lukáš; Lengál, Ondřej; Vojnar, Tomáš: Nested antichains for WS1S (2019)
  5. Pham, Long H.; Le, Quang Loc; Phan, Quoc-Sang; Sun, Jun; Qin, Shengchao: Enhancing symbolic execution of heap-based programs with separation logic for test input generation (2019)
  6. Ta, Quang-Trung; Le, Ton Chanh; Khoo, Siau-Cheng; Chin, Wei-Ngan: Automated mutual induction proof in separation logic (2019)
  7. Tatsuta, Makoto; Chin, Wei-Ngan; Al Ameen, Mahmudul Faisal: Completeness and expressiveness of pointer program verification by separation logic (2019)
  8. Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W.: VST-Floyd: a separation logic tool to verify correctness of C programs (2018)
  9. Chen, Taolue; Song, Fu; Wu, Zhilin: Tractability of separation logic with inductive definitions: beyond lists (2017)
  10. Fiedor, Tomáš; Holík, Lukáš; Janků, Petr; Lengál, Ondřej; Vojnar, Tomáš: Lazy automata techniques for WS1S (2017)
  11. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  12. 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)
  13. Faisal Al Ameen, Mahmudul; Tatsuta, Makoto: Completeness for recursive procedures in separation logic (2016)
  14. Gu, Xincai; Chen, Taolue; Wu, Zhilin: A complete decision procedure for linearly compositional separation logic with data constraints (2016)
  15. Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
  16. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight VeriFast (2015)
  17. Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben: Symbolic execution proofs for higher order store programs (2015)
  18. Sharma, Asankhaya; Wang, Shengyi; Costea, Andreea; Hobor, Aquinas; Chin, Wei-Ngan: Certified reasoning with infinity (2015)
  19. Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan; Yang, Hongli: Invariants synthesis over a combined domain for automated program verification (2013)
  20. Charlton, Nathaniel; Horsfall, Ben; Reus, Bernhard: Crowfoot: a verifier for higher-order store programs (2012)

1 2 next

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