jStar: Towards Practical Verification for Java j j j
Dino Distefano, Matthew Parkinson · 2008
In this paper we introduce a novel methodology for verifying a large set of Java programs which builds on recent theoretical devel- opments in program verification: it combines the idea of abstract predicate families (24-26) and the idea of symbolic execution and abstraction using separation logic (9). 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 de- sign patterns (subject/observer, visitor, factory, and pooling). Al- though these patterns are extensively used by object-oriented de- velopers in real-world applications, so far they have been highly challenging for existing object-oriented verification techniques. Categories and Subject Descriptors D.2.4 (Software Engineer- ing): Program Verification; D.3.3 (Programming Languages): Language Constructs and Features—Classes and inheritance