Loading...
Please wait, while we are loading the content...
Similar Documents
ESC4: a modern caching ESC for Java
| Content Provider | ACM Digital Library |
|---|---|
| Author | Chalin, Patrice James, Perry R. |
| Abstract | JML4 is an Eclipse-based Integrated Verification Environment for the Java Modeling Language (JML) that supports several forms of verification, including Runtime Assertion Checking, Extended Static Checking (ESC), and Full Static Program Verification. The first of these developed was ESC4, JML4's ESC component. This paper presents its architecture. ESC4's verification-condition (VC) generation is based on the approach described by Barnett and Leino, but we provide an optimization for loops. A configurable Prover Coordinator allows the easy implementation of various proof strategies. Caching discharged VCs helps reduce the number of calls to the provers when reverifying code. Caches are not commonly used because of their fragility w.r.t. source code changes, but we propose a simple way to make them more resilient. |
| Starting Page | 19 |
| Ending Page | 26 |
| Page Count | 8 |
| File Format | |
| ISBN | 9781605586809 |
| DOI | 10.1145/1596486.1596491 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2009-08-25 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Jml4 Esc4 Java modeling language |
| Content Type | Text |
| Resource Type | Article |
