Henrique Rebelo's Home Page

Home

Papers

Talks

Projects

CV

 

 

Henrique Rebęlo
Researcher Associate
Centro de Informática
Universidade Federal de Pernambuco

Ph.D. in Computer Science, CIn-UFPE, Brazil (2014)
    In cooperation with University of Central Florida, USA

MSR Intern, Microsoft Research, USA (2010)

+55 (81) 2126 8430 ext. 4770 [voice]
+55 (81) 2126 8430 [FAX]
hemr@cin.ufpe.br


I'm fascinated by the challenges of enabling programmers to write and understand programs using specifications that, as much as possible, record information about their detailed design. I believe that programs that clearly express their specifications and the design structure they implement are easier to maintain. Hence, questions such as what a part of the program does? (without looking at its implementation) and what other parts of the program depend on that behavior become easier to answer.

In pursuit of this goal, most of my research has been in behavioral interface specification language design and implementation. Current work focuses on Java Modeling Language (JML), and is being done with an international collaboration. In this direction, we have developed the aspect-oriented JML, which uses AOP mechanisms to enable an expressive design by contract checking. In the aspect-oriented sense, my current efforts are directed towards the definition of a set of more expressive contracts (design rules) that can help solving the modular reasoning problem about aspect-oriented programs (please refer to the XPIDRs publications).

A long term interest in formal methods for OO software components is behavioral subtyping. The message passing mechanism of OO languages, such as C++ and Java, allows one to easily extend programs by adding new types. This works best if objects of the new types behave like the objects of the old types; the old types are supertypes of the new types, which are called subtypes. How should one reason about programs that use subtyping and message passing?

The idea of behavioral subtyping, which Gary T. Leavens (my current co-advisor) helped develop, supports a modular technique known as supertype abstraction, that solves this problem. However, enforcing such modular technique in contemporary runtime assertion checkers is not a trivial task. Hence, most of my current efforts to restablish a modular runtime assertion checking use a technique called Client-Aware Checking (CAC), which precisely follows the principles behind the supertype abstraction technique. We developed a JML compiler (ajmlc) with CAC support.

I also had the good fortune to work as a research intern (supervised by Shuvendu Lahiri) at the Microsoft Research, Redmond in the Research in Software Engineering (RiSE) group that developed SymDiff, a language-agnostic tool for equivalence checking to reason about imperative program changes. In a nutshell, Symdiff can be summarized as Windiff for behaviors. It builds up on recent advances on program equivalence checking using automated SMT solvers. However, it extends beyond program equivalence and deals with questions such as: (1) can one infer the conditions under which two programs are equivalent? (2) how do the changes affect the public API? Some of my current research is program equivalence checking related.

I am also interested in programming environments, coding styles, other kinds of tools, and advanced modularization techniques.


Distinctions and Awards
* Distinguished Paper Award - SBCARS 2013, Brasilia, Brazil, September 29 to October 4, 2013.
* Best Demo Award - SEKE 2012, San Francisco Bay, USA, July 1-3, 2012.
* Selected as one of MSR Latin American Interns - RiSE group, Redmond, 2010.
* Member of the Advisory Board of Microsoft Innovation Center Pernambuco FY2010 (MIC PE FY2010), since July 2009.
* Project Award - member of the Petrilogic project granted by IBM Eclipse Innovation Grants Awards Program, EIG 2005.
* Sun Certified Programmer for Java2 platform 1.4, Sun Microsystems, 2005.

Computer Societies Membership




 
SEKE'14 - PC Member, 26th International Conference on Software Engineering and
Knowledge Engineering

IJAS - Editorial Board, International Journal On Advances in Software
SEKE'13 - PC Member, 25th International Conference on Software Engineering and
Knowledge Engineering

LA-WASP'13 - Organizer and PC member, 7th Latin American Workshop on Aspect-Oriented
Software Development: Advanced Modularization Techniques

VALID'13 - PC Member, 5th IARIA Intl. Conference on Advances in System Testing and
Validation Lifecycle

VALID'12 - PC Member, 4th IARIA Intl. Conference on Advances in System Testing and
Validation Lifecycle

ICISA'12 - PC Member, 3nd IEEE Intl. Conference on Information Science and Applications
SCP @ Benevol'11 - Referee, Special issue in Science of Computer Programming
VALID'11 - PC Member, 3rd IARIA Intl. Conference on Advances in System Testing and
Validation Lifecycle

ICISA'11 - PC Member, 2nd IEEE Intl. Conference on Information Science and Applications
ICITCS'11 - PC Member, International Conference on IT Convergence and Security
AOSD'11 - Local Organizing Committee, 10th ACM Intl. Conference on AOSD
FOAL'11 - Proceedings Chair, 10th Foundations of AO Languages workshop
VALID'10 - PC Member, 2nd IARIA Intl. Conference on Advances in System Testing and
Validation Lifecycle

VALID'09 - PC Member, 1st IARIA Intl. Conference on Advances in System Testing and
Validation Lifecycle


Centro de Informática UFPE
Cidade Universitária - CEP 50740-540
Recife/PE - Brazil

  CIn-UFPE