Java Typestate Checker

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

2 Citations (Scopus)

Abstract

Detecting programming errors and vulnerabilities in software is increasingly important, and building tools that help developers with this task is a crucial area of investigation on which the industry depends. In object-oriented languages, one naturally defines stateful objects where the safe use of methods depends on their internal state; the correct use of objects according to their protocols is then enforced at compile-time by an analysis based on behavioral types. We present Java Typestate Checker (JATYC), a tool based on the Checker Framework that verifies Java programs with respect to typestates. These define the object’s states, the methods that can be called in each state, and the states resulting from the calls. The tool offers the following strong guarantees: sequences of method calls obey to object’s protocols; completion of objects’ protocols; detection of null-pointer exceptions; and control of the sharing of resources through access permissions. To the best of our knowledge, there are no research or industrial tools that offer all these features. In particular, the implementation of sharing control in a typestate-based tool seems to be novel, and has an important impact on programming flexibility, since, for most programs, the linear discipline imposed by behavioral types is too strict. Sharing of objects is enabled by means of an assertion language incorporating fractional permissions; to lift from programmers the burden of writing the assertions, JATYC infers all of these by building a constraint system and solving it with Z3, producing general assertions sufficient to accept the code, if these exist.

Original languageEnglish
Title of host publicationCoordination Models and Languages - 23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Proceedings
EditorsFerruccio Damiani, Ornela Dardha
Place of PublicationCham
PublisherSpringer
Pages121-133
Number of pages13
ISBN (Electronic)978-3-030-78142-2
ISBN (Print)978-3-030-78141-5
DOIs
Publication statusPublished - 2021
Event23rd IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021 - Virtual, Online
Duration: 14 Jun 202118 Jun 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Volume12717 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference23rd IFIP WG 6.1 International Conference on Coordination Models and Languages, COORDINATION 2021 held as part of 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021
CityVirtual, Online
Period14/06/2118/06/21

Keywords

  • access permissions
  • Behavioral types
  • inference
  • object-oriented programming
  • typestates

Fingerprint

Dive into the research topics of 'Java Typestate Checker'. Together they form a unique fingerprint.

Cite this