Abstract. The finite powerset construction upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. In this paper we define three g...
Roberto Bagnara, Patricia M. Hill, Enea Zaffanella
Abstract. We present a generic framework for the automatic and modular inference of sound class invariants for class-based object oriented languages. The idea is to derive a sound ...
Abstract. Java is a very successful programming language which is also becoming widespread in embedded systems, where software correctness is critical. Jlint is a simple but highly...
Abstract. We study the type system introduced by Boyapati and Rinard in their paper “A Parameterized Type System for Race-Free Java Programs” and try to infer the type annotati...