A Formalization IDE Integrated with a Verifying Compiler
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.
Mon 19 Jun
|16:00 - 17:00|
|17:00 - 17:30|
|Link to publication DOI File Attached|
|17:30 - 18:00|
Daniel WelchClemson University, Blair DurkeeClemson University, Mike KabbaniClemson University, Murali SitaramanClemson UniversityLink to publication DOI File Attached