Runtime assertion checking (RAC) is a well-established technique for runtime verification of object-oriented (OO) programs. Contemporary RACs use specifications from the receiver’s dynamic type when checking method calls. This implies that in presence of subtyping and dynamic dispatch features of object-oriented programming, these specifications differ from the ones used by static verification tools, which rely on the specifications associated with the static type of the receiver. Besides the heterogeneity problem, this also hinders the benefits of modular reasoning achieved by the notion of supertype abstraction. In this context, we propose a more precise runtime assertion checking for OO programs that better matches the semantics used in static verification tools. While we describe our approach, we discuss how it can be used to avoid the heterogenous semantics problem and among others.

My chief [and long-term] research interest is at improving the productivity of programmers by enabling them to write programs that, as much as possible, look like their design [and design constraints]. I believe that programs that clearly capture the design structure and interfaces they implement are more configurable, fun to develop and easier to maintain.

In pursuit of this goal, my research has been focused in programming language design and implementation, including software engineering, tools and related issues.

I have worked massively in the area of design by contract (DbC) and aspect-oriented programming (AOP). In the former, I have contributed extensively to the implementation of the JML specification language and its [RAC] compiler. In the latter, more recently, I’m excited to have started the next generation of aspect-oriented programming, as outlined in my SBLP 2017 talk. In this context, I’m leading the development of aspect-oriented programming reloaded project, which includes the AspectJML programming language and its Online IDE. AspectJML is [now] a general-purpose aspect-oriented extension to Java. It supports programming in Java, JML, AspectJ, AspectJML, or a mixin of all that. Hence, some of my current research in the Software Productivity Group is AOP[Reloaded]/AspectJML related.