Thanks! It's great to see interest in our work on HN. Yes, this is the precursor to and basis for our current work on refinement type inference for C. For thos

Thanks! It's great to see interest in our work on HN. Yes, this is the precursor to and basis for our current work on refinement type inference for C. For those who haven't seen it, our recent work has focused on extending the automatic program verification techniques shown in this talk to work for low-level programs - that is, programs that use mutable state, pointer arithmetic, and so on. The project page for our Liquid Types-based verifier for C programs is here: http://goto.ucsd.edu/csolve/ http://goto.ucsd.edu/csolve/ The project page for the overall Liquid Types project is here: http://goto.ucsd.edu/~rjhala/liquid/ http://goto.ucsd.edu/~rjhala/liquid/