Postdoc at Carnegie Mellon University in Corina Pasareanu's group at the Silicon Valley campus.
My main research interest is software analysis. In particular, I am interested in analysing consumption of resources such as time, memory and energy. Within the ISSTAC project, we use the Symbolic PathFinder extension SPF-WCA to infer bounds on worst-case time and space complexity of Java programs. The goal is to identify security vulnerabilities (both denial-of-service and side-channel based attacks). These inferred bounds can then be verified with our tool JayHorn, a light-weight prover for Java.
Before joining CMU-SV, I was with the Open University of the Netherlands and Radboud University Nijmegen. My PhD at Radboud University was advised by Marko van Eekelen and concerned software analysis methods for resource-sensitive systems. This includes not only resource analysis, but also functional correctness and security. I worked on two projects at Radboud University: Go-Green, developing a green, self-learning, user-centric home automation system, and CHARTER, which developed a chain of tools for the generation of safe, correct and resource-efficient software for the aeronautical, automotive and surveillance industry.
During my PhD, I have co-developed an automated analysis for energy consumption of software (given a set of hardware models). This analysis is implemented in the tool ECAlogic. Results on loop-bound analysis and heap and stack space usage analysis for Java software are implemented in the tool ResAna.
NASA Research Park
Building 19, Room 1006
Moffett Field, CA 94035
NASA Formal Methods 2017
Scientific peer-reviewed publications
- Quantified Heap Invariants for Object-Oriented Programs
Temesghen Kahsai, Rody Kersten, Philipp Ruemmer and Martin Schäf
To appear at the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2017).
- Symbolic Complexity Analysis using Context-preserving Histories
Kasper Luckow, Rody Kersten and Corina Pasareanu
To appear at the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017).
- Resource Contracts for Java
Rody Kersten, Martin Schäf and Temesghen Kahsai
In Proceedings of the Java PathFinder Workshop 2016, ACM SIGSOFT Software Engineering Notes, 2016.
- Using Dependent Types to define Energy Augmented Semantics of Programs
Bernard van Gastel, Rody Kersten, Marko van Eekelen
In Proceedings of the Fourth International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA'15).
- Improving Coverage of Test-Cases Generated by Symbolic PathFinder for Programs with Loops
Rody Kersten, Suzette Person, Neha Rungta and Oksana Tkachuk
In Proceedings of the Java PathFinder Workshop 2014, ACM SIGSOFT Software Engineering Notes, 2015.
- ECAlogic: Hardware-Parametric Energy-Consumption Analysis of Algorithms
Marc Schoolderman, Jascha Neutelings, Rody Kersten and Marko van Eekelen
In Proceedings of the 13th Foundations of Aspect-Oriented Languages Workshop, pages 19-22, 2014.
- A Hoare Logic for Energy Consumption Analysis
Rody Kersten, Paolo Parisen Toldin, Bernard van Gastel and Marko van Eekelen
In Proceedings of the Third International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA'13), LNCS 8552, pages 93-109, 2014.
- ResAna: A Resource Analysis Toolset for (Real-Time) Java [Wiley Online Library]
Rody Kersten, Bernard van Gastel, Olha Shkaravska, Manuel Montenegro and Marko van Eekelen
Journal of Concurrency and Computation: Practice and Experience, Vol. 26, Number 14, Pages 2432-2455. Wiley, 2014.
- Using Model-Checking to Reveal a Vulnerability of Tamper-Evident Pairing
Rody Kersten, Bernard van Gastel, Manu Drijvers, Sjaak Smetsers and Marko van Eekelen
In Proceedings of the 5th NASA Formal Methods Symposium, LNCS 7871, pages 63-77. Springer, May 2013.
- Making Resource Analysis Practical for Real-Time Java
Rody Kersten, Olha Shkaravska, Bernard van Gastel, Manuel Montenegro and Marko van Eekelen
In JTRES'12: Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems, ACM Digital Proceedings Series, 2012.
- Test-Based Inference of Polynomial Loop-Bound Functions
Olha Shkaravska, Rody Kersten and Marko van Eekelen
In PPPJ'10: Proceedings of the 8th International Conference on the Principles and Practice of Programming in Java, pages 99-108, 2010.
- Soundness Proof for a Hoare Logic for Energy Consumption Analysis
Paolo Parisen Toldin, Rody Kersten, Bernard van Gastel, and Marko van Eekelen
Technical report ICIS--R13009, Radboud University Nijmegen, October 2013.
- Ranking Functions for Loops with Disjunctive Exit-Conditions
Rody Kersten and Marko van Eekelen
In Ricardo Peña (ed.) Proceedings of the 2th International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA2011). Madrid, Spain. Tech. Rep. SIC-08/11. Dept. Computer Systems and Computing Universidad Complutense de Madrid. pp. 111-126. May 2011.
- JayHorn: A framework for verifying Java programs
Temesghen Kahsai, Rody Kersten, Philipp Rümmer, Huascar Sanchez, Martin Schäf
At CAV '16, July 2016, Toronto, Ontario, Canada.
- Big Energy Data for Software Engineering
Christoph Bockisch, Jeroen Keiren, Bernard van Gastel, Rody Kersten, Marko van Eekelen
At ECOOP '15, July 2015, Prague, Czech Republic.
- Go-Green: Greener house through a self-learning, privacy-aware, user-centric, energy-aware, wireless monitoring and control system
At An Innovative Truth IV, June 2012, Beatrix Theater, Utrecht, The Netherlands.
- Software Analysis Methods for Resource-Sensitive Systems
Rody Kersten, July 2015.