jStar: Towards Practical Verification for Java
The work
| Title | jStar: Towards Practical Verification for Java |
|---|---|
| Authors | Dino Distefano; Matthew J. Parkinson |
| Type | conference paper |
| Year | 2008 |
| Citekey | distefano2008jstar |
Where it appeared
| Published in | Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications |
|---|---|
| Publisher | Association for Computing Machinery |
| Pages | 213--226 |
Identifiers
| DOI | 10.1145/1449764.1449782 |
|---|---|
| OpenAlex | W2053154567 |
Access
| Landing page | https://doi.org/10.1145/1449764.1449782 |
|---|
Abstract
In this paper we introduce a novel methodology for verifying a large set of Java programs which builds on recent theoretical developments in program verification: it combines the idea of abstract predicate families and the idea of symbolic execution and abstraction using separation logic. The proposed technology has been implemented in a new automatic verification system, called jStar, which combines theorem proving and abstract interpretation techniques. We demonstrate the effectiveness of our methodology by using jStar to verify example programs implementing four popular design patterns (subject/observer, visitor, factory, and pooling). Although these patterns are extensively used by object-oriented developers in real-world applications, so far they have been highly challenging for existing object-oriented verification techniques.
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Standing | endorsed |
| Approved | 2026-08-07 |
Cite it as
@inproceedings{distefano2008jstar,
title = {jStar: Towards Practical Verification for Java},
author = {Dino Distefano and Matthew J. Parkinson},
year = {2008},
booktitle = {Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications},
pages = {213--226},
publisher = {Association for Computing Machinery},
doi = {10.1145/1449764.1449782},
url = {https://doi.org/10.1145/1449764.1449782},
}
This record lives at https://refs.drheap.org/distefano2008jstar/ and will keep doing so.