Andre Oliveira Maroneze

PhD Candidate in Computer Science at IRISA/INRIA Rennes, France


Short CV

Current Research

My PhD subject is related to Worst-Case Execution Time (WCET) and Verified Compilation. This research is at the intersection of the fields of formal verification (more specifically, mechanical verification with the help of a proof assistant) and static WCET estimation. There are two directions to this research:

  • To formally verify state-of-the-art WCET estimation techniques, proving their soundness;
  • To benefit from the semantics and the framework of a formally verified compiler (namely, the CompCert project) to produce formally verified WCET estimation techniques.

There is a strong concern about the correctness of the obtained results. The analyses are proven correct with respect to the semantics of the compiler’s intermediate representations using the Coq proof assistant.

  • PhD Research
    • The formal development results related to my thesis are available online. This page includes links to the Coq proof scripts.

Past Research

I’ve done a bit of research (or research-related work) on a few different subjects:

  • Document (image) structure analysis: during my Masters’ internship, I worked on a high-level grammar-based formalism to “parse” structured images of documents (such as handwritten letters, tabular forms, musical scores, etc), the DMOS method.
  • Graph visualization techniques: during a short visit at NICTA Canberra, Australia, I participated in the improvement of an interface to visualize large dynamic constraint graphs.
  • Information visualization: during my undergraduate studies in Computer Engineering at UNICAMP, I did some development related to how to best present numeric/qualitative information using colors, shapes, sizes, etc.


  • Formal Verification of a C Value Analysis Based on Abstract Interpretation. S. Blazy, V. Laporte, A. Maroneze, D. Pichardie. Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Online Coq development
  • Formal Verification of Loop Bound Estimation for WCET Analysis. S. Blazy, A. Maroneze, D. Pichardie. Verified Software: Theories, Tools, Experiments - 5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013. Online Coq development
  • Introduction of statistical information in a syntactic analyser for document image recognition. A. Maroneze, B. Coüasnon, A. Lemaitre. Document recognition and Retrieval XVIII - Electronic Imaging (DRR 2011), San Francisco, US. (Best student paper award) Link to the HAL open archive / Presentation slides


As a teaching assistant at University of Rennes, I currently participate/have participated as lab assistant in the following modules:

  • ASI (Architecture of Information Systems)
    • Contents: computer architecture, programming in Scheme and Python
    • Level: L1 (1st year undergraduate)
  • API (Algorithms and Imperative Programming)
    • Contents: Imperative Java programming, basic algorithms
    • Level: L2 (2nd year undergraduate)
  • SYR2 (Systems Programming) [FAQ pour les étudiants (in French)]
    • Contents: Unix system programming in C
    • Level: L3 (3rd year undergraduate)
  • COMP (Compilers) [FAQ pour les étudiants (in French)]
    • Contents: Parsing and code generation, Java and ANTLR programming
    • Level: M1 (1st year Masters)
  • VET (Project in Technology Intelligence)
    • Contents: State-of-the-art and implementation of a security-related project. Chosen subject: Android permissions management
    • Level: M2 SSI (2nd year Masters, specialization in Information Systems Security)
  • BUR (Office Software Suite)
    • Contents: Usage of office software suites (OpenOffice Writer & Calc)
    • Level: L1 (1st year undergraduate)
  • DU-ST (Computer Science for Science & Technology Students)
    • Contents: Applications of computer science for non-CS students (e.g. basic programming, Web development, databases)
    • Level: L1 (1st year undergraduate)