Charge! A framework for higher-order separation logic in Coq

Speaker: Jesper Bengtson , 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

Public: Yes

Location: 32-G882 (reading room)

Event Type:

Room Description:

Host: Adam Chlipala, CSAIL

Contact: Adam Chlipala, adamc@csail.mit.edu

Relevant URL: http://www.itu.dk/people/jebe/project/charge.html

Speaker URL: None

Speaker Photo:
None

Reminders to: pl@csail.mit.edu, seminars@csail.mit.edu

Reminder Subject: 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.

Research Areas:

Impact Areas:

See other events that are part of the PL/SE Seminar Series 2013/2014.

Created by Adam Chlipala at Friday, November 01, 2013 at 10:18 AM.