Bacchiani, LorenzoBravetti, MarioGiunti, MarcoMota, JoãoRavara, António2022-11-082022-11-082022-09-010167-6423PURE: 46064614PURE UUID: 07a496a6-feb7-4991-8332-cc2450b83576Scopus: 85135482139ORCID: /0000-0001-8074-0380/work/122412567http://hdl.handle.net/10362/145315This work was partially supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No. 778233 (BehAPI) and by NOVA LINCS UIDB/04516/2020/TRA/BIM/07 ) via the Portuguese Fundação para a Ciência e a Tecnologia. Publisher Copyright: © 2022 Elsevier B.V.Detecting programming errors 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. Leveraging on the observation that in Object-Oriented Programming (OOP) it is natural to define stateful objects where the safe use of methods depends on their internal state, we present Java Typestate Checker (JATYC), a tool that verifies Java source code with respect to typestates. A typestate defines the object's states, the methods that can be called in each state, and the states resulting from the calls. The tool statically verifies that when a Java program runs: sequences of method calls obey to object's protocols; objects' protocols are completed; null-pointer exceptions are not raised; subclasses' instances respect the protocol of their superclasses. To the best of our knowledge, this is the first OOP tool that simultaneously tackles all these aspects.8281566engBehavioral typesObject-oriented programmingSubtypingType-checkingTypestatesSoftwareComputational Theory and MathematicsGeneral Computer ScienceSDG 9 - Industry, Innovation, and Infrastructurejournal article10.1016/j.scico.2022.102844https://www.scopus.com/pages/publications/85135482139