- Charge! A framework for hig...
- Edit Event
- Cancel Event
- Preview Reminder
- Send Reminder
- Other events happening in November 2013
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:
Created by Adam Chlipala at Friday, November 01, 2013 at 10:18 AM.