TeachHIP: Teaching Automated Verification using HIP/SLEEK

(online) EXAMPLEs

TeachHIP's Overview

TeachHIP, is an online resource for teaching automated verification to students using the HIP/SLEEK verification system.

Lesson Plan

  • Lesson 1 - Introduction and Multiple Specifications [ 2018-PDF | 2015-Slides]
    • SLEEK Exercises [Txt]
    • HIP Exercises [Txt]
  • Lesson 2 - Termination and Structured Specifications [Slides]
    • HIP Exercises [Txt]
  • Lesson 3 - Immutable Specifications and Concurrency
  • Lesson 4 - Shape Inference and Pure Bi-Abduction
  • Example programs

    Example programs (on the left panel) can be run ONLINE.

    Check the content of the stdhip.h file

    Please contact Asankhaya Sharma or Andreea Costea if you have any problems/suggestions/discussions or simply want to learn more about TeachHIP.

    TeachHIP is based on the web interface of HIPimm developed by Andreea Costea.