Skip to main content

Christine Rizkallah

Christine Rizkallah
Researcher

Research Interests

Higher-Order Logic - Interactive Theorem Proving - Formal Verification

Contact Details

Email:Christine.Rizkallah@data61.csiro.au
Web:http://www.mpi-inf.mpg.de/~crizkall/

More contact information is available at the Contact page.

Photo of Christine Rizkallah

Publication List

Projects

Past

Qualifications

2010 - 2015: Ph. D. in Computer Science at the Universität des Saarlandes and the Max-Planck-Institut für Informatik, Saarbrücken, Germany Title of PhD Thesis: Verification of Program Computations Supervisor: Kurt Mehlhorn

October 2007 - December 2009: Master studies in Computer Science at the Universität des Saarlandes, Saarbrücken, Germany (with IMPRS-CS scholarship from the Max-Planck-Institut für Informatik) Title of Master's Thesis: Proof Representations for Higher Order Logic Supervisors: Prof. Dr. Gert Smolka, Dr. Chad E. Brown

October 2003 - October 2007: Bachelor studies in Computer Science at the German University in Cairo, Cairo, Egypt Title of Bachelor's Thesis: X2-Planner: A Hierarchical Task Network Planner for Real Time Gaming Applications Supervisors: Prof. Dr. Slim Abdennadher, Dr. Thorsten Maier (Thesis done at Xaitment Gmbh, Saarbrücken, Germany)

Publications

Data61 Papers

2017

Abstract PDF Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong
COMPLX: A verification framework for concurrent imperative programs
International Conference on Certified Programs and Proofs, pp. 138-150, Paris, France, January, 2017

2016

Abstract PDF Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein
Refinement through restraint: Bringing down the cost of verification
International Conference on Functional Programming, Nara, Japan, September, 2016
Abstract PDF June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah
Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
International Conference on Interactive Theorem Proving, pp. 52-68, Nancy, France, August, 2016
Abstract PDF Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein
A framework for the automatic formal verification of refinement from Cogent to C
International Conference on Interactive Theorem Proving, Nancy, France, August, 2016

NICTA Papers

2016

Abstract PDF Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah
Compositional verification and refinement of concurrent value-dependent noninterference
IEEE Computer Security Foundations Symposium, pp. 417-431, Lisbon, Portugal, June, 2016
Abstract PDF Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein and Gernot Heiser
Cogent: verifying high-assurance file system implementations
International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 175-188, Atlanta, GA, USA, April, 2016

2014

Abstract PDF Liam O'Connor-Davis, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah
CDSL version 1: Simplifying verification with linear types
Technical Report, NICTA, October, 2014