Name
Abstract | ||
|---|---|---|
This demonstration will illustrate both a web- and desktop-based formalization IDE (F-IDE) that are backed by a verifying compiler for the RESOLVE specification and programming language. Each IDE we demo 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 first portion of the demo will illustrate the language and verification in the context of the web-based environment, the second half will demonstrate features of a newer desktop-based IDE that provides additional modern IDE amenities beyond those offered by the web-based version. Each IDE we present integrates feedback for mathematical and programmatic type checking, proving, among others, and permit users to generate and run executable, property-preserving Java. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1145/3098572.3098580 | ICOOOLPS@ECOOP |
Field | DocType | ISBN |
Programming language,Type checking,Computer science,Code generation,Compiler,Implementation,Real-time computing,Big data,Java,Executable | Conference | 978-1-4503-5088-4 |
Citations | PageRank | References |
0 | 0.34 | 8 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel Welch | 1 | 5 | 1.84 |
| Blair Durkee | 2 | 0 | 0.68 |
| Mike Kabbani | 3 | 0 | 0.34 |
| Murali Sitaraman | 4 | 270 | 40.99 |