Follow us:
  • Follow us on Facebook
  • Follow us on Twitter
  • Follow us on Linked In
Student Login

  New Student Signup  |  Lost Password

Declarative Rewrite Rules Compiler and Proofs (C++ or Python)

Oracle Labs #2

Return to List

Closed Posted: 11 May 17. Closes: 05 Jun 17 Available: Semester 2 (Jul - Nov)

UPDATE 8/6: a student has been appointed to this project.


Semester 2 2017 + summer vacation + Semester 1 2018 

Note: students must be able to enrol in thesis/project spread across Semester 2 + 1; as well available whole of summer vacation. These are requirements for this project.

This project will suit final year / Masters students in Software Engineering / Computer Science / IT - with strong programming skills (ideally Python or C++) and a very solid understanding of data structures and algorithms (Grade 6 or 7 in relevant subject/s). A strong interest in Program Analysis and software engineering principles is also needed.

The successful applicant will receive a $9,000 scholarship + academic credit (24cps - QUT; 4 units - UQ).  You must be available to work on the project onsite for 2 days/week during semester 2 + 1; plus 5 days/week over the entire summer vacation period.

APPLICANTS NOTE: you must include your academic transcript/s inside your resume (undergrad + Masters if applicable) - before Oracle Labs will consider your application. Also include your student number.

Location: Brisbane CBD QLD
Categories: Information Technology, Electrical Engineering

Project Background / Description

Parfait is a static analysis tool which finds defects in C, C++, and Java programs. Internally, Parfait has representations for expressions of code. Semantically equivalent code could be expressed in multiple ways, but It is important for us that all expressions represented internally are in a canonical form. Using a canonical form makes expressions much better to work with. We currently have hand written imperative code to perform canonicalization. Replacing this with a declarative approach would simplify the code, be less error prone, and enable us to better asses the correctness of the canonicalization.


Oracle offers a comprehensive and fully integrated stack of cloud applications, platform services, and engineered systems.  With more than 400,000 customers—including 100 of the Fortune 100—in more than 145 countries, Oracle provides a complete technology stack both in the cloud and in the data centre.

Oracle’s industry-leading cloud-based and on-premises solutions give customers complete deployment flexibility and unmatched benefits including application integration, advanced security, high availability, scalability, energy efficiency, powerful performance, and low total cost of ownership.

For more information about Oracle, visit

Oracle Labs

Oracle Labs is the research division of Oracle.  It focuses on applied research to produce new technologies of interest to the company.

Oracle Labs Australia (, based in Brisbane, specialises in Program Analysis in a variety of domains, including bug-checking, productivity tools, security analysis, testing, and more. The Brisbane team hit the headlines with its research on static code analysis that lead to scalable and precise bug-checking algorithms embedded in the Parfait tool.

How Oracle helps CEED students

We link you up with an experienced supervisor on the Brisbane team. They will work closely with you, helping you grow your skills-really practical skills you can put to work in real-world situations.

Objectives / Tasks / Project Outcomes

  • Scope the project based on the group’s interests/strengths and the requirements of Oracle Labs
  • Study rewrite rules, proof tools
  • Design and implement a tool which takes a declarative rewrite specification as input and complies it to C++ code implementing the rewrites.
  • Use a proof assistant tool (such as Isabelle) to perform proofs on the declarative specification (with some auxiliary information) for properties such as correctness, convergence, and completeness.
  • Generate test cases for the C++ implementation generated from the declarative specification, leveraging work with the proof tools to generate expected results.
  • Write a detailed report on work done
  • Give a presentation to the group on work done

Skills / Experience Required

  • Interest in formal methods
  • Experience with C++ or Python would be ideal
  • Excellent academic results
  • Excellent problem-solving skills
  • Strong interest in Program Analysis and software engineering principles
  • Strong understanding of data structures and algorithms
  • Experience with Unix-based systems
  • Ability to work independently and in small groups

Return to List

Subscribe to e-newsletter