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

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.

Preprint (a6-welch.pdf)2.8MiB

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