Christine Rizkallah

Senior Lecturer

School of Computing and Information Systems
The University of Melbourne

Email: first name (dot) last name (at) unimelb.edu.au
Office: Office 2307, Level 2, Melbourne Connect
Address: 700 Swanston Street,
Carlton, VIC 3053,
Australia

My research ambition is to create techniques and tools that ease the use of interactive theorem provers for verifying code from various domains by focusing on one domain at a time. In particular, I am interested in developing domain-specific languages with type-systems that enforce desired properties and with verified or certifying compilers that reduce the effort required for formally verifying software systems.

So far, most of my work focused on using interactive theorem proving to establish new results or to formalize and verify existing results from the following research areas: algorithms, programming languages, security, systems, logic, and social choice theory. As demonstrated by my wide-ranging publication record, I enjoy interdisciplinary research and I am often keen to collaborate on solving problems that arise in various areas.

Publications Teaching Supervision Employment Community Service

News

Jul 2023:
I will be giving a keynote talk next month at ICFP'23 about our Cogent and Dargent language approach to reducing the effort required for trustworthy system development.
Mar 2023:
Dr. Zilin Chen has successfully completed his PhD. Congratulations to Zilin on the PhD completion!
Dec 2022:
Selene, Zoey, Raphael, Zilin and myself are all attending SPLASH'22. Zilin is presenting our Cogent property based testing work at SLE'22. Selene, Raphael, and Zoey are presenting their work on memory safety at the poster session, termination algorithms (poster session, student competition), and effective cost models (doctoral symposium), respectively. Raphael won the first place SPASH'22 student competition award in the undergrad category.
Nov 2022:
Our Dargent data-layout specification language with automatically verified refinements down to the bit-level will appear at POPL'23.
Sep 2022:
Our Cogent property-based testing framework will appear at SLE'22. The artefact associated with our paper won a distinguished artefact award, thanks to Zilin Chen.
Jan-Jun 2022:
Louis, Vincent, Selene, and Zoey have all decided to leave UNSW and they have all successfully transferred their PhD candidature to the the University of Melbourne. We have all had a smooth transition, thanks to everyone, at the University of Melbourne, who was involved in the process.
Dec 2021:
I have decided to leave UNSW and to move to the University of Melbourne as a senior lecturer. I am very pleased with this decision.
Dec 2021:
Zoey Chen and Selene Linares successfully passed their PhD confirmation reviews.
June 2021:
I am glad to announce that Louis Cheung and Vincent Jackson have concluded their research assistant positions and started their PhD with me. I'm looking forward to the switch.
Mar 2021:
Zoey Chen and Selene Linares have started their PhD with me. It's my pleasure to welcome them to the team.
Recent and upcoming service:
POPL'24, TyDe'24, CPP'23 (PC), CoqPL@POPL'23 (PC), PLMW@POPL'22 (organizing committee), PriSC@POPL'22 (PC), ESOP'22 (PC), ICFP'21 (PC) .

Education and Employment

Since December 2021:
Senior Lecturer at the University of Melbourne, Melbourne, Australia
April 2018 - December 2021:
Lecturer at the University of New South Wales, Sydney, Australia
June 2016 - March 2018:
Postdoc at the University of Pennsylvania, Philadelphia, USA
Working on the DeepSpec project
November 2014 - May 2016:
Researcher at Data61 (formerly NICTA) and Conjoint Lecturer at the University of New South Wales, Sydney, Australia
July 2010 - September 2015:
PhD student 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: Prof. Dr. Kurt Mehlhorn)
October 2007 - December 2009:
Master student in Computer Science at the Universität des Saarlandes, Saarbrücken, Germany (with an 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)

Current Postdocs and Students

PhD Students

Louis Cheung (co-supervised by Alistair Moffat)
Selene Linares (co-supervised by Peter Schachte)
Vincent Jackson (co-supervised by Toby Murray)
Zoey Chen (co-supervised by Johannes Åman Pohjola)

Research Assistants, Masters and Undergrad Projects and Interns

Jakob Schuster (undergrad project)
Dion Sean Hansen (exchange student from Aalborg University, Denmark)
Raphael Douglas Giles (light part-time RA work since 2021)

Former Postdocs and Students

Postdocs

Ambroise Lafont (till January 2022, followed by a postdoc at the University of Cambridge)
Craig McLaughlin (till December 2021, followed by another UNSW postdoc)
Amos Robinson (till June 2019 followed by a researcher position at Ghost Autonomy)

PhD Students

Zilin Chen (supervised with Gabriele Keller).
Towards a Practical High-Assurance Systems Programming Language, 2023.
(followed by a researcher position at Ghost Autonomy)
Liam O'Connor (supervised with Gabriele Keller).
Type Systems for Systems Types, 2019.
(followed by a faculty position at the University of Edinburgh)

Honours Students

Oscar Downing.
Enhancements to the Cogent Property-Based Testing Framework, 2021.
Seung Hoon (Simon) Park (co-supervised by Johannes Åman Pohjola).
Interaction Trees in Isabelle/HOL, 2021.
(followed by a full-time RA position at the University of Oxford)
Harrison Scott.
Towards a Verified Compiler from Cogent to LLVM, 2021.
Declan Warn (final thesis marked by Carroll Morgan).
Extending the Debugging Capabilities of the Cogent Compiler, 2021.
Blaise Paradeza.
Refinement types for Cogent, 2020.
James Treloar (co-advised by Craig McLaughlin).
Linear Frank, 2020.
Lucy Qiu.
Termination Checker for Recursive Types in Cogent, 2020.
Luka Kerr.
Extending a Purely Functional Language to Enable Low-Level Systems Programming, 2020.
Vincent Jackson.
Extensionality Translations for Polymorphic Higher-Order Logic, 2020.
Vivian Dang.
Information-Flow Security for Cogent, 2020.
Alexander Hodges.
Property Based Testing of C Code from Haskell, 2019.
Emmet Murray.
Recursive Types For Cogent, 2019.
Louis Cheung.
Verifying C Data Types for Cogent, 2019.
Sahan Fernando.
Extending Cogent's Data-Description Language with Layout Polymorphism, 2019.

Course-Work Master Students

William Walters.
Exploring Differential Privacy and Robustness in Machine Learning, 2022.
Jack Drury (co-supervised by Carroll Morgan).
Formalisation and Proofs about Kuifje: A Quantitative Information Flow Aware Language, 2021.
Zhanlin Shang.
An LLVM Backend of the Cogent Compiler, 2020.

Research Assistants and Interns

Tingchen Xie (Data61 intern, then UNSW Taste of Research intern in 2021)
Raphael Douglas Giles (UNSW Taste of Research intern in 2021)
Termination of Recursive Functions by Lexicographic Orders of Linear Combinations,
Won first prize, student research competition (undergrad) SPLASH, 202022.
Seung Hoon (Simon) Park (part-time RA till August 2021, then fulltime RA at the University of Oxford)
Zander Zhuang (Data61 intern till February 2021)
Vincent Jackson (full-time RA till May 2021)
Louis Cheung (full-time RA till November 2020)
Nelson Chen (part-time RA till November 2020)
Gray Yao (UNSW Taste of Research intern till March 2020)
Emmet Murray (part-time RA till February 2020, then at Microsoft)
Zoey Chen (Data61 intern till February 2020)
Ryan Barry (part-time RA till October 2019, then full-time RA at Data61, CSIRO)
Gretchen Forbush (part-time RA till May 2019)
Matthew Di Meglio (part-time RA till November 2018)
Pang Luo (full-time RA till 2016)
Japheth Lim (full-time RA till 2016)
Yutaka Nagashima (full-time RA till 2016, then a PhD student at the Czech Technical University in Prague)

Teaching

Lecturer for COMP30026: Models of Computation at UniMelb (Semester 2, 2022)
Together with Bach Le
Lecturer for COMP90048: Declarative Programming at UniMelb (Semester 1, 2022)
Together with Peter Schachte
Lecturer for COMP3141: Software System Design and Implementation at UNSW (Term 2, 2021)
Together with Curtis Millar
Lecturer for COMP3161: Concepts in Programming Languages at UNSW (Term 3, 2020)
Together with Liam O'Connor
Lecturer for COMP4161: Advanced topics in Software Verification at UNSW (Term 3, 2020)
Together with Gerwin Klein, Miki Tanaka, and Johannes Åman Pohjola
Lecturer for COMP2111: System Modelling and Design at UNSW (Term 1, 2020)
Together with Paul Hunter
Lecturer for COMP3161: Concepts in Programming Languages at UNSW (Term 3, 2019)
Together with Liam O'Connor
Lecturer for COMP4161: Advanced topics in Software Verification at UNSW (Term 3, 2019)
Together with June Andronick, Miki Tanaka, and Johannes Åman Pohjola
Lecturer for COMP3141: Software System Design and Implementation at UNSW (Term 2, 2019)
Together with Liam O'Connor
Lecturer for COMP4161: Advanced topics in Software Verification at UNSW (Winter 2018)
Together with Gerwin Klein, June Andronick, and Miki Tanaka
Guest lecturer (two lectures) and TA for CIS500: Software Foundations at the University of Pennsylvania (Fall 2016)
Lecturer for COMP4161: Advanced topics in Software Verification at UNSW (Winter 2015)
Together with Gerwin Klein, June Andronick, and Toby Murray
Lecturer for Seminar on Social Choice Theory at Universität des Saarlandes (Winter 2012/2013)
Together with Rob van Stee
TA for Graph Theory at Universität des Saarlandes (Summer 2011)

Community Service

Organizing committee member

Programming Languages Mentoring Workshop (PLMW@POPL), 2022.

Program committee (PC) member

External review committee (ERC) member

Artifact evaluation committee (AEC) member

45th ACM SIGPLAN Symposium on Principles of Programming Languages conference (POPL), 2019.

Reviewer

ACM Transactions on Programming Languages and Systems journal (TOPLAS), 2018.

Publications [ Google Scholar]

Journal Articles

Z. Chen, A. Lafont, L. O'Connor, G. Keller, C. McLaughlin, V. Jackson, and C. Rizkallah.
Dargent: A Silver Bullet for Verified Data Layout Refinement.
Proceedings of the ACM on Programming Languages (PACMPL 7 (POPL)), volume 7, pages 1369-1395, 2023.
L. O'Connor, Z. Chen, C. Rizkallah, V. Jackson, S. Amani, G. Klein, T. Murray, T. Sewell, and G. Keller.
Cogent: Uniqueness Types and Certifying Compilation.
Journal of Functional Programming (JFP), Special Issue on Secure Compilation, volume 31, 2022.
J. Breitner, A. Spector-Zabusky, Y. Li, C. Rizkallah, J. Wiegley, J. Cohen, S. Weirich.
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code.
Journal of Functional Programming (JFP), volume 31, E5, 2021.
J. Breitner, A. Spector-Zabusky, Y. Li, C. Rizkallah, J. Wiegley, S. Weirich.
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code (Experience Report).
Proceedings of the ACM on Programming Languages (PACMPL 2 (ICFP)), volume 2, pages 89:1-89:16, 2018.
H. Aziz, P. Luo, C. Rizkallah.
Incompatibility of Efficiency and Strategyproofness in the Random Assignment Setting with Indifferences.
Economics Letters, volume 160, pages 46-49, 2017.
E. Alkassar, S. Böhme, K. Mehlhorn, and C. Rizkallah.
A Framework for the Verification of Certifying Computations.
Journal of Automated Reasoning (JAR), volume 52(3), pages 241-273 (2014).
Preliminary version published in CAV 2011.
Chad E. Brown and Christine Rizkallah.
Glivenko and Kuroda for Simple Type Theory.
Journal of Symbolic Logic. 79(2), pages 485-495 (2014)

Articles in Refereed Conference Proceedings

Z. Chen, C. Rizkallah, L. O'Connor, P. Susarla, G. Klein, G. Heiser, and G. Keller.
Property-Based Testing: Climbing the Stairway to Verification.
Software Language Engineering (SLE), pages 84-97, 2022.
L. Cheung, L. O'Connor, and C. Rizkallah.
Overcoming Restraint: Composing Verification of Foreign Functions with Cogent.
Certified Programs and Proofs (CPP), pages 13-26, 2022.
C. Rizkallah, D. Garbuzov, and S. Zdancewic.
A Formal Equational Theory for Call-By-Push-Value.
Interactive Theorem Proving (ITP), pages 523-541, 2018.
( formalisation)
A. Spector-Zabusky, J. Breitner, C. Rizkallah, and S. Weirich.
Total Haskell is Reasonable Coq.
Certified Programs and Proofs (CPP), pages 14-27, 2018.
H. Aziz, P. Luo, and C. Rizkallah.
Rank Maximal Equal Contribution: a Probabilistic Social Choice Function.
AAAI Conference on Artificial Intelligence (AAAI), pages 910-916, 2018.
L. O'Connor, Z. Chen, P. Susarla, C. Rizkallah, G. Klein, and G. Keller.
Bringing Effortless Refinement of Data Layouts to Cogent.
International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), pages 134-149, 2018.
S. Amani, J. Andronick, M. Bortin, C. Lewis, C. Rizkallah, and J. Tuong.
Complx: A Verification Framework for Concurrent Imperative Programs.
Certified Programs and Proofs (CPP), pages 138-150, 2017.
L. O'Connor, Z. Chen, C. Rizkallah, S. Amani, J. Lim, T. Sewell, Y. Nagashima, T. Murray, and G. Klein.
Refinement Through Restraint: Bringing Down the Cost of Verification.
ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 89-102, 2016.
C. Rizkallah, J. Lim, Y. Nagashima, T. Sewell, Z. Chen, L. O'Connor, T. Murray, G. Keller, and G. Klein.
A Framework for the Automatic Formal Verification of Refinement from Cogent to C.
Interactive Theorem Proving (ITP), 323-340, 2016.
J. Andronick, C. Lewis, D. Matichuk, C. Morgan, and C. Rizkallah.
Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency.
Interactive Theorem Proving (ITP), pages 52-68, 2016.
T. Murray, R. Sison, E. Pierzchalski, and C. Rizkallah.
Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference.
IEEE Computer Security Foundations Symposium (CSF), pages 417-431, 2016.
S. Amani, A. Hixon, Z. Chen, C. Rizkallah, P. Chubb, L. O'Connor, J. Beeren, Y. Nagashima, J. Lim, T. Sewell, J. Tuong, G. Keller, T. Murray, G. Klein, and G. Heiser.
Cogent: Verifying High-Assurance File System Implementations.
ACM International Conference on Architectural Support for Programming Languages and
Operating Systems (ASPLOS), pages 175-188, 2016.
L. Noschinski, C. Rizkallah, and K. Mehlhorn.
Verification of Certifying Computations through AutoCorres and Simpl.
NASA Formal Methods (NFM), volume 8430 of LNCS, pages 46-61. Springer, 2014.
E. Alkassar, S. Böhme, K. Mehlhorn, and C. Rizkallah.
Verification of Certifying Computations.
Computer Aided Verification (CAV), volume 6806 of LNCS, pages 67-82. Springer, 2011.

Articles in Refereed Workshop Proceedings

Z.Chen, M. Di Meglio, L. O'Connor, P. Susarla, C. Rizkallah, and G. Keller.
A Data Layout Description Language for Cogent (Extended Abstract) .
Principles of Secure Compilation Workshop (PriSC@POPL), 2019.
H. Aziz, P. Luo, and C. Rizkallah.
Incompatibility of Efficiency and Strategyproofness in the Random Assignment Setting with Indifferences.
Algorithmic Game Theory Workshop (AGT@IJCAI), 2016.
Christine Rizkallah.
A Simpl Shortest Path Checker Verification.
Isabelle Workshop, 2014.
Chad E. Brown and Christine Rizkallah.
From Classical Extensional Higher-Order Tableau to Intuitionistic Intensional Natural Deduction.
Proof Exchange for Theorem Proving Workshop (PxTP@CADE), pages 27-42, 2013.

Theses

C. Rizkallah.
Verification of Program Computations.
Saarland University 2015.
C. Rizkallah.
Proof Representations for Higher-Order Logic.
Saarland University 2009.

Refereed Online Journal (Formal Proofs)

S. Amani, J. Andronick, M. Bortin, C. Lewis, C. Rizkallah, and J. Tuong.
Complx: A Verification Framework for Concurrent Imperative Programs.
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs. November 2016.
T. Murray, R. Sison, E. Pierzchalski, and C. Rizkallah.
Compositional Security-Preserving Refinement for Concurrent Imperative Programs.
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs. June 2016.
T. Murray, R. Sison, E. Pierzchalski, and C. Rizkallah.
A Dependent Security Type System for Concurrent Imperative Programs.
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs. June 2016.
Christine Rizkallah.
An Axiomatic Characterization of the Single-Source Shortest Path Problem.
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs. May 2013.
Christine Rizkallah.
Maximum Cardinality Matching.
In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs. July 2011.

Research Reports

D. Garbuzov, W. Mansky, C. Rizkallah, and S. Zdancewic.
Structural Operational Semantics for Control Flow Graph Machines.
In CoRR abs/1805.05400 2018.
J. Breitner, A. Spector-Zabusky, Y. Li, C. Rizkallah, J. Wiegley, and S. Weirich.
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code.
In CoRR abs/1803.06960 2018.
L. O'Connor, C. Rizkallah, Z. Chen, S. Amani, J. Lim, Y. Nagashima, T. Sewell, A. Hixon,
G. Keller, T. Murray, and G. Klein.
COGENT: Certified Compilation for a Functional Systems Language.
In CoRR abs/1601.05520 2016.
L. O'Connor, G. Keller, S. Amani, T. Murray, G. Klein, Z. Chen, and C. Rizkallah.
CDSL Version 1: Simplifying Verification with Linear Types.
Technical Report, NICTA, October, 2014.
E. Alkassar, S. Böhme, K. Mehlhorn, C. Rizkallah, and P. Schweizer.
An Introduction to Certifying Algorithms.
it - Information Technology, volume 53, pages 287-293, 2011.