Henrique Rebęlo
M.Sc. in Computer Engineering, University of Pernambuco, 2008.
Home Papers Talks Projects CV Current Positions PhD Student in Computer Science Informatics Center, UFPE Federal University of Pernambuco In cooperation with: - University of Central Florida (UCF), School of Electrical Engineering & Computer Science (EECS), USA MSR Intern, Microsoft Research, USA (2010) 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 Best Demo Award - In the 24th International Conf. on Software Engineering and Knowledge Engineering (SEKE 2012), San Francisco Bay, USA, July 1-3, 2012. MSR Internship - Selected as one of Microsoft Research Latin American Interns in the Research in Software Engineering (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 Association for Computing Machinery (ACM) (No. 0779302), member since: 2008. IEEE Computer Society (No. 90648774), member since: 2009. Brazilian Computer Society (SBC) (No. 15540), student member since: 2005. 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 Tel - +55 (81) 2126 8430 ext. 4770
Home
Papers
Talks
Projects
CV
Informatics Center, UFPE Federal University of Pernambuco In cooperation with:
- University of Central Florida (UCF), School of Electrical Engineering & Computer Science (EECS), USA MSR Intern, Microsoft Research, USA (2010)
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.
Centro de Informática UFPE Cidade Universitária - CEP 50740-540 Recife/PE - Brazil Tel - +55 (81) 2126 8430 ext. 4770
