Abstract
This paper describes a novel technique for fully automated
procedure-modular verification of Java programs equipped
with method-local and global assertions that specify safety
properties of sequences of method invocations. Modularity
of verification is achieved by relativizing the correctness of
global properties on the local properties rather than on the
implementations of methods, and is based on the construction
of maximal models. Tool support is provided by means
of ProMoVer, a tool that is essentially a wrapper around a
previously developed tool set for compositional verification
of control
flow safety properties, where program data is abstracted
away completely. We evaluate the technique on a small but realistic case study.
| Original language | Undefined |
|---|---|
| Title of host publication | 12th Workshop on Formal Techniques for Java-like Programs, FTfJP 2010 |
| Place of Publication | New York |
| Publisher | Association for Computing Machinery |
| Pages | 5:1-5:7 |
| Number of pages | 7 |
| ISBN (Print) | 978-1-4503-0540-2 |
| DOIs | |
| Publication status | Published - 2010 |
| Event | 12th Workshop on Formal Techniques for Java-like Programs, FTfJP 2010 - Maribor, Slovenia Duration: 22 Jun 2010 → 22 Jun 2010 Conference number: 12 https://distrinet.cs.kuleuven.be/events/ftfjp10/ |
Publication series
| Name | |
|---|---|
| Publisher | ACM |
Workshop
| Workshop | 12th Workshop on Formal Techniques for Java-like Programs, FTfJP 2010 |
|---|---|
| Abbreviated title | FTfJP |
| Country/Territory | Slovenia |
| City | Maribor |
| Period | 22/06/10 → 22/06/10 |
| Internet address |
Keywords
- METIS-270992
- Modular Verification
- Temporal Logic
- IR-72645
- EWI-18324
- Maximal Models