A Formalization IDE Integrated with a Verifying Compiler (ICOOOLPS 2017 - 12th Workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems)

Write a Blog >>

Sun 18 - Fri 23 June 2017 Barcelona, Spain

co-located with PLDI, ECOOP, Curry On, DEBS, LCTES and ISMM

Who

Daniel Welch, Blair Durkee, Mike Kabbani, Murali Sitaraman

Track

ICOOOLPS 2017

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Mon 19 Jun 2017 17:30 - 18:00 at Vertex WS216 - Afternoon II Chair(s): Olivier Zendra

Abstract

This demonstration will illustrate the features of a Formalization IDE (F-IDE) that is supported by a verifying compiler. This RESOLVE F-IDE supports construction of mathematical developments, formal interface specifications of generic, object-based concepts, and alternative implementations annotated with internal assertions to enable verification. While the F-IDE includes features users of modern IDE’s have come to expect, the environment goes beyond these by integrating mathematical and programmatic type checking and proving, among others. The F-IDE makes it easy for users to generate and run executable, property-preserving Java.

Link to Publication

http://dl.acm.org/citation.cfm?id=3098580&CFID=775126081&CFTOKEN=88871719

DOI

https://doi.org/10.1145/3098572.3098580

File attachments

Preprint (a6-welch.pdf)	2.8MiB

Daniel Welch

Clemson University

Blair Durkee

Clemson University

Mike Kabbani

Clemson University

Murali Sitaraman

Clemson University

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Mon 19 Jun
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:00	Afternoon IIICOOOLPS at Vertex WS216 Chair(s): Olivier Zendra

16:00 60m Other		Panel: Do new Computing Environments lead to new Language Constructs? ICOOOLPS Eric Jul University of Oslo, Edd Barrett King's College London, Steve Blackburn Australian National University , Ben L. Titzer Google
17:00 30m Talk		Diff Graphs for a fast Incremental Pointer Analysis ICOOOLPS Jakob Krainz Friedrich-Alexander University Erlangen-Nürnberg, Michael Philippsen Link to publication DOI File Attached
17:30 30m Demonstration		A Formalization IDE Integrated with a Verifying Compiler ICOOOLPS Daniel Welch Clemson University, Blair Durkee Clemson University, Mike Kabbani Clemson University, Murali Sitaraman Clemson University Link to publication DOI File Attached