Research Interests
 Higher Order Logic
 Interactive Theorem Proving
 Formal Software Verification
Qualifications
 Since June 2016: Postdoc at the University of Pennsylvania funded by the
NSF
Expedition on the Science of Deep Specification grant.
 November 2014  May 2016: Researcher at Data61 (formerly NICTA) and
Conjoint Lecturer at the University of New South Wales
 July 2010  September 2015:
Ph. D. studies in Computer Science at
the Universität
des Saarlandes, Saarbrücken, Germany and
the MaxPlanckInstitut für Informatik
Title of PhD Thesis: Verification of Program Computations (supervisor: Prof. Dr. Kurt Mehlhorn)
 October 2007  December 2009:
Master studies in Computer Science at the
Universität des Saarlandes,
Saarbrücken, Germany (with IMPRSCS
scholarship from the MaxPlanckInstitut
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: X2Planner: 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
Journal Articles
Articles in Refereed Conference Proceedings
 S. Amani, J. Andronick, M. Bortin, C. Lewis, C. Rizkallah, J. Tuong.
Complx: A Verification Framework for Concurrent Imperative Programs.
Certified Programs and Proofs (CPP),pages 138150, 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 89102, 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  7th International Conference (ITP), 323340, 2016.
 J. Andronick, C. Lewis, D. Matichuk, C. Morgan, and C. Rizkallah.
Proof of OS Scheduling Behavior in the Presence of InterruptInduced Concurrency.
Interactive Theorem Proving  7th International Conference (ITP), pages 5268, 2016.
 T. Murray, R. Sison, E. Pierzchalski, and C. Rizkallah.
Compositional Verification and Refinement of Concurrent ValueDependent Noninterference.
IEEE Computer Security Foundations Symposium (CSF), pages 417431, 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 HighAssurance File System Implementations.
ACM International Conference on Architectural Support for Programming Languages and
Operating Systems (ASPLOS), pages 175188, 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 4661. 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 6782. Springer, 2011.
Articles in Refereed Workshop Proceedings
Theses
Refereed Online Journal (Formal Proofs)
 S. Amani, J. Andronick, M. Bortin, C. Lewis, C. Rizkallah, 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 SecurityPreserving 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 SingleSource 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
 H. Aziz, P. Luo, and C. Rizkallah
Rank Maximal Equal Contribution: a Probabilistic Social Choice Function.
Submitted to International Joint Conference on Artificial Intelligence (IJCAI), February 2017.
 H. Aziz, P. Luo, and C. Rizkallah
Incompatibility of Efficiency and Strategyproofness in the
Random Assignment Setting with Indifferences.
Submitted to the Journal of Economics Letters, November 2016.
 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 287293, 2011.
