I am a graduate student in computer science at the University of Illinois at Urbana-Champaign. I started in Summer 2005 and I am studying formal methods with José Meseguer.
Before starting my studies at the University of Illinois I completed my Diplom studies at the University of Karlsruhe, Germany in the group of Peter H. Schmitt. There, I was involved in the KeY Project.
If you need to contact me, the easiest way to do that is by email to "rsasse" at the domain "uiuc.edu". You can also visit me at my office:
2111 Siebel Center
201 N Goodwin Ave
Urbana, IL 61801
phone: +1-(217)-333-5219
Publications
-
Effectively Checking the Finite Variant PropertyIn RTA 2008: Rewriting Techniques and Applications
-
Variant Narrowing and Equational UnificationIn 7th International Workshop on Rewriting Logic and its Applications, 2008
-
A Systematic Approach to Uncover Security Flaws in GUI LogicIn IEEE Symposium on Security and Privacy, Oakland, California, May 2007
-
Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics6th International Workshop on Rewriting Logic and its Applications , WRLA, Vienna, Austria, April 2006, ENTCS, Elsevier
-
Automatic Validation of Transformation Rules for Java Verification against a Rewriting Semantics12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR, Montego Bay, Jamaica, December 2005, LNCS 3835, Springer
Projects
- Systematic GUI Logic Flaw Analysis
- In this project my work is partially as a graduate research assistant, that part is funded by the National Science Foundation, and partially as a summer research intern at Microsoft Research. This work addresses GUI logic flaws in web browsers, analyses them systematically and leads to having the thus uncovered flaws fixed by the browser vendor. The systematic analysis is performed on a model of the implementation for the most part but is also done on the actual implementation for some part. You can download the technical report from MSR here (local mirror).
- Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics
- My work in this project is as a graduate research assistant, it is funded by the National Science Foundation. This project develops an experimental tool for the verification of properties of a sequential imperative subset of the Java language. It uses an equational semantics of that fragment and develops and implements a compositional Hoare logic for it. The long-term goal of this project is to use extensible and modular rewriting logic semantics of programming languages to develop similarly extensible and modular Hoare logics on which generic program verification tools can be based. This project is documented in the WRLA '06 paper and in a technical report. There is also the project website with more detail and the actual tool. I gave a talk about this work at WRLA'06.
- Taclets vs. Rewriting Logic - Relating Semantics of Java
- This was my Diplomarbeit done at the University of Karlsruhe. It focuses on the validation of program transformation rules, in the form of taclets, against a semantics of Java, given in Rewriting Logic. The full work is available from the library in Karlsruhe as Technical Report 2005-16 or directly here as PDF Version. I gave a talk about the related paper at LPAR-12. The code used in this project is available from the project website (local mirror). A summary in German is also available as PDF.
- Proof Obligations for Correctness of Modifies Clauses
- This was my Studienarbeit done at the University of Karlsruhe. It exposed a way on how to create proof obligations, within the KeY framework, to check the correctness of modifies clauses. It is available as PDF.
