Charge! A framework for higher-order separation logic in Coq
, IT-University of Copenhagen
Date: Tuesday, November 05, 2013
Time: 12:30 PM to 1:30 PM Note: all times are in the Eastern Time Zone
Location: 32-G882 (reading room)
Host: Adam Chlipala, CSAIL
Contact: Adam Chlipala, firstname.lastname@example.org
Relevant URL: http://www.itu.dk/people/jebe/project/charge.html
Speaker URL: None
TALK: Charge! A framework for higher-order separation logic in Coq
We present a comprehensive set of algebraic structures to reason about higher-order separation logic in Coq. Using Coq's native support for type classes we are able to construct a modular library that allows users to construct both separation logics and specification logics to reason about programs written in a wide variety of languages. Currently, Charge! has been used successfully to verify programs written both in Java and x86 assembly. This talk will focus on how Charge! is used to construct separation and specification logics from a memory model of a small Java-like language.
Created by Adam Chlipala at Friday, November 01, 2013 at 10:18 AM.