CHASE: A Static Checker for JML's Assignable Clause

Néstor Cataño, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

27 Citations (Scopus)

Abstract

This paper presents a syntactic method to check so-called assignable clauses of annotated Java programs. Assignable clauses describe which variables may be assigned by a method. Their correctness is crucial for reasoning about class specifications. The method that we propose is incomplete, as it only makes a syntactic check and it does not take aliasing or expression evaluation into account, but it provides efficient means to find the most common errors in assignable clauses. This is demonstrated by applying the method to the specification of an industrial case study.
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings
EditorsLenore D. Zuck, Paul C. Attie, Agostino Cortesi, Supratik Mukhopadhyay
PublisherSpringer
Pages26-40
Number of pages15
DOIs
Publication statusPublished - 2003
Externally publishedYes
Event4th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2003 - New York, United States
Duration: 9 Jan 200311 Jan 2003
Conference number: 4

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume2575

Conference

Conference4th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2003
Abbreviated titleVMCAI 2003
CountryUnited States
CityNew York
Period9/01/0311/01/03

Fingerprint

Dive into the research topics of 'CHASE: A Static Checker for JML's Assignable Clause'. Together they form a unique fingerprint.

Cite this