Christine Rizkallah

Lecturer

Dr Christine Rizkallah is a Lecturer with the School of Computer Science and Engineering. Christine's research interests include:

  • Formal methods: software verification, interactive theorem proving (Coq and Isabelle/HOL), proof theory.
  • Programming languages: certifying and verified compilers, type theory, equational theories.
  • Security: information-flow control, memory safety, secure compilation.

Webpage: http://www.cse.unsw.edu.au/~crizkallah/ 

publications

Journal articles
add
Breitner J; Spector-Zabusky A; Li Y; Rizkallah C; Wiegley J; Cohen J; Weirich S, 2021, 'Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code', Journal of Functional Programming, http://dx.doi.org/10.1017/S0956796820000283
2021
Breitner J; Spector-Zabusky A; Li Y; Rizkallah C; Wiegley J; Weirich S, 2018, 'Ready, Set, Verify! Applying hs-to-coq to Real-World Haskell Code (Experience Report)', PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES, vol. 2, http://dx.doi.org/10.1145/3236784
2018
Aziz H; Luo P; Rizkallah C, 2017, 'Incompatibility of efficiency and strategyproofness in the random assignment setting with indifferences', Economics Letters, vol. 160, pp. 46 - 49, http://dx.doi.org/10.1016/j.econlet.2017.08.010
2017
Brown CE; Rizkallah C, 2014, 'Glivenko and kuroda for simple type theory', Journal of Symbolic Logic, vol. 79, pp. 485 - 495, http://dx.doi.org/10.1017/jsl.2013.10
2014
Alkassar E; Böhme S; Mehlhorn K; Rizkallah C, 2014, 'A framework for the verification of certifying computations', Journal of Automated Reasoning, vol. 52, pp. 241 - 273, http://dx.doi.org/10.1007/s10817-013-9289-2
2014
Alkassar E; Boehme S; Mehlhorn K; Rizkallah C; Schweitzer P, 2011, 'An Introduction to Certifying Algorithms', IT-INFORMATION TECHNOLOGY, vol. 53, pp. 287 - 293, http://dx.doi.org/10.1524/itit.2011.0655
2011
Garbuzov D; Mansky W; Rizkallah C; Zdancewic S, 'Structural Operational Semantics for Control Flow Graph Machines', Structural Operational Semantics for Control Flow Graph Machines, http://arxiv.org/abs/1805.05400v1
O'Connor L; Rizkallah C; Chen Z; Amani S; Lim J; Nagashima Y; Sewell T; Hixon A; Keller G; Murray T; Klein G, 'COGENT: Certified Compilation for a Functional Systems Language', COGENT: Certified Compilation for a Functional Systems Language, http://arxiv.org/abs/1601.05520v1
Cheung L; O'Connor L; Rizkallah C, 'Overcoming Restraint: Modular Refinement using Cogent's Principled Foreign Function Interface', , http://arxiv.org/abs/2102.09920v2
Conference Papers
add
Aziz H; Luo P; Rizkallah C, 2018, 'Rank Maximal Equal Contribution: a Probabilistic Social Choice Function', in THIRTY-SECOND AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE / THIRTIETH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE / EIGHTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, ASSOC ADVANCEMENT ARTIFICIAL INTELLIGENCE, New Orleans, LA, pp. 909 - 915, presented at 32nd AAAI Conference on Artificial Intelligence / 30th Innovative Applications of Artificial Intelligence Conference / 8th AAAI Symposium on Educational Advances in Artificial Intelligence, New Orleans, LA, 02 February 2018 - 07 February 2018, http://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000485488900111&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=891bb5ab6ba270e68a29b250adbe88d1
2018
Rizkallah C; Garbuzov D; Zdancewic S, 2018, 'A Formal Equational Theory for Call-By-Push-Value', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Oxford, United Kingdom, pp. 523 - 541, presented at International Conference on Interactive Theorem Proving, Oxford, United Kingdom, 09 July 2018 - 12 July 2018, http://dx.doi.org/10.1007/978-3-319-94821-8_31
2018
O’Connor L; Chen Z; Susarla P; Rizkallah C; Klein G; Keller G, 2018, 'Bringing effortless refinement of data layouts to COGENT', in Margaria T; Steffen B (ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer, Cham, Limassol, Cyprus, pp. 134 - 149, presented at International Symposium on Leveraging Applications of Formal Methods : ISoLA 2018, Limassol, Cyprus, 05 November 2018 - 09 November 2018, http://dx.doi.org/10.1007/978-3-030-03418-4_9
2018
Aziz H; Luo P; Rizkallah C, 2018, 'Rank maximal equal contribution: A probabilistic social choice function', in 32nd AAAI Conference on Artificial Intelligence, AAAI 2018, AAAI Press, New Orleans, Louisiana, pp. 910 - 916, presented at The Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18), New Orleans, Louisiana, 02 February 2018 - 07 February 2018, https://aaai.org/ocs/index.php/AAAI/AAAI18/paper/view/16560/15774
2018
Spector-Zabusky A; Breitner J; Rizkallah C; Weirich S, 2018, 'Total Haskell is reasonable Coq', in CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018, pp. 14 - 27, http://dx.doi.org/10.1145/3167092
2018
Amani S; Andronick J; Bortin M; Lewis C; Rizkallah C; Tuong J, 2017, 'COMPLX: A verification framework for concurrent imperative programs', in CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2017, pp. 138 - 150, http://dx.doi.org/10.1145/3018610.3018627
2017
Murray T; Sison R; Pierzchalski E; Rizkallah C, 2016, 'Compositional verification and refinement of concurrent value-dependent noninterference', in Proceedings - IEEE Computer Security Foundations Symposium, IEEE, Lisbon, PORTUGAL, presented at IEEE 29th Computer Security Foundations Symposium (CSF), Lisbon, PORTUGAL, 27 June 2016 - 01 July 2016, http://dx.doi.org/10.1109/CSF.2016.36
2016
O'Connor L; Chen Z; Rizkallah C; Amani S; Lim J; Murray T; Nagashima Y; Sewell T; Klein G, 2016, 'Refinement through restraint: bringing down the cost of verification', in Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ACM, presented at ICFP'16: ACM SIGPLAN International Conference on Functional Programming, 18 September 2016 - 24 September 2016, http://dx.doi.org/10.1145/2951913.2951940
2016
Amani S; Hixon A; Chen Z; Rizkallah C; Chubb P; O'Connor L; Beeren J; Nagashima Y; Lim J; Sewell T; Tuong J; Keller G; Murray T; Klein G; Heiser G, 2016, 'COGENT: Verifying High-Assurance File System Implementations', in OPERATING SYSTEMS REVIEW, ASSOC COMPUTING MACHINERY, Atlanta, GA, pp. 175 - 188, presented at 21st International Conference on Architectural Support for Programming Languages and Operating Systems, Atlanta, GA, 02 April 2016 - 06 April 2016, http://dx.doi.org/10.1145/2872362.2872404
2016
Andronick J; Lewis C; Matichuk D; Morgan C; Rizkallah C, 2016, 'Proof of OS scheduling behavior in the presence of interrupt-induced concurrency', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Nancy, France, pp. 52 - 68, presented at International Conference on Interactive Theorem Proving 2016, Nancy, France, 22 August 2016 - 27 August 2016, http://dx.doi.org/10.1007/978-3-319-43144-4_4
2016
Rizkallah C; Lim J; Nagashima Y; Sewell T; Chen Z; O Connor L; Murray T; Keller G; Klein G, 2016, 'A framework for the automatic formal verification of refinement from COGENT to C', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Nancy, France, pp. 323 - 340, presented at 7th International Conference, ITP 2016, Nancy, France, 22 August 2016 - 25 August 2016, http://dx.doi.org/10.1007/978-3-319-43144-4_20
2016
Amani S; Hixon A; Chen Z; Rizkallah C; Chubb P; O'Connor L; Beeren J; Nagashima Y; Lim J; Sewell T; Tuong J; Keller G; Murray T; Klein G; Heiser G, 2016, 'COGENT: Verifying high-assurance file system implementations', in International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS, Atlanta, GA, USA, pp. 175 - 188, presented at 21st International Conference on Architectural Support for Programming Languages and Operating Systems, Atlanta, GA, USA, 02 April 2016 - 06 April 2016, http://dx.doi.org/10.1145/2872362.2872404
2016
O'Connor L; Chen Z; Rizkallah C; Amani S; Lim J; Murray T; Nagashima Y; Sewell T; Klein G, 2016, 'Refinement Through Restraint: Bringing down the cost of Verification', in International Conference on Functional Programming, ACM New York NY, USA, Nara, Japan, pp. 89 - 102, presented at International Conference on Functional Programming, Nara, Japan, 19 September 2016 - 21 September 2016, http://dx.doi.org/10.1145/2951913.2951940
2016
Noschinski L; Rizkallah C; Mehlhorn K, 2014, 'Verification of certifying computations through AutoCorres and Simpl', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 46 - 61, http://dx.doi.org/10.1007/978-3-319-06200-6_4
2014
Alkassar E; Böhme S; Mehlhorn K; Rizkallah C, 2011, 'Verification of certifying computations', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 67 - 82, http://dx.doi.org/10.1007/978-3-642-22110-1_7
2011