Formally Verified Suffix Array Construction. - Louis Cheung; Alistair Moffat; Christine Rizkallah (J. Autom. Reason., 1992)

Verification of Certifying Computations. - Eyad Alkassar; Sascha Böhme; Kurt Mehlhorn; Christine Rizkallah (CAV, 2011)

Maximum Cardinality Matching. - Christine Rizkallah (Arch. Formal Proofs, 2011)

An Introduction to Certifying Algorithms. - Eyad Alkassar; Sascha Böhme; Kurt Mehlhorn; Christine Rizkallah; Pascal Schweitzer (it Inf. Technol., 2011)

From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction. - Chad E. Brown; Christine Rizkallah (PxTP@CADE, 2013)

An Axiomatic Characterization of the Single-Source Shortest Path Problem. - Christine Rizkallah (Arch. Formal Proofs, 2013)

Verification of Certifying Computations through AutoCorres and Simpl. - Lars Noschinski; Christine Rizkallah; Kurt Mehlhorn (NASA Formal Methods, 2014)

A Framework for the Verification of Certifying Computations. - Eyad Alkassar; Sascha Böhme; Kurt Mehlhorn; Christine Rizkallah (J. Autom. Reason., 2014)

Glivenko and Kuroda for Simple Type Theory. - Chad E. Brown; Christine Rizkallah (J. Symb. Log., 2014)

Verification of program computations. - Christine Rizkallah (2015)

CoGENT: Verifying High-Assurance File System Implementations. - 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; et al. (ASPLOS, 2016)

Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. - Toby C. Murray; Robert Sison; Edward Pierzchalski; Christine Rizkallah (CSF, 2016)

Refinement through restraint: bringing down the cost of verification. - Liam O'Connor; Zilin Chen; Christine Rizkallah; Sidney Amani; Japheth Lim; Toby C. Murray; Yutaka Nagashima; Thomas Sewell; Gerwin Klein (ICFP, 2016)

Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. - June Andronick; Corey Lewis; Daniel Matichuk; Carroll Morgan; Christine Rizkallah (ITP, 2016)

A Framework for the Automatic Formal Verification of Refinement from Cogent to C. - Christine Rizkallah; Japheth Lim; Yutaka Nagashima; Thomas Sewell; Zilin Chen; Liam O'Connor; Toby C. Murray; Gabriele Keller; Gerwin Klein (ITP, 2016)

COMPLX: A Verification Framework for Concurrent Imperative Programs. - Sidney Amani; June Andronick; Maksym Bortin; Corey Lewis; Christine Rizkallah; Joseph Tuong (Arch. Formal Proofs, 2016)

A Dependent Security Type System for Concurrent Imperative Programs. - Toby C. Murray; Robert Sison; Edward Pierzchalski; Christine Rizkallah (Arch. Formal Proofs, 2016)

Compositional Security-Preserving Refinement for Concurrent Imperative Programs. - Toby C. Murray; Robert Sison; Edward Pierzchalski; Christine Rizkallah (Arch. Formal Proofs, 2016)

Incompatibility of Efficiency and Strategyproofness in the Random Assignment Setting with Indifferences. - Haris Aziz 001; Pang Luo; Christine Rizkallah (CoRR, 2016)

COGENT: Certified Compilation for a Functional Systems Language. - Liam O'Connor; Christine Rizkallah; Zilin Chen; Sidney Amani; Japheth Lim; Yutaka Nagashima; Thomas Sewell; Alex Hixon; Gabriele Keller; Toby C. Murray; Gerwin Klein (CoRR, 2016)

Rank Maximal Equal Contribution: A Probabilistic Social Choice Function. - Haris Aziz 001; Pang Luo; Christine Rizkallah (AAAI, 2018)

Total Haskell is reasonable Coq. - Antal Spector-Zabusky; Joachim Breitner; Christine Rizkallah; Stephanie Weirich (CPP, 2018)

Bringing Effortless Refinement of Data Layouts to Cogent. - Liam O'Connor; Zilin Chen; Partha Susarla; Christine Rizkallah; Gerwin Klein; Gabriele Keller (ISoLA (1), 2018)

A Formal Equational Theory for Call-By-Push-Value. - Christine Rizkallah; Dmitri Garbuzov; Steve Zdancewic (ITP, 2018)

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Stephanie Weirich (CoRR, 2018)

Structural Operational Semantics for Control Flow Graph Machines. - Dmitri Garbuzov; William Mansky; Christine Rizkallah; Steve Zdancewic (CoRR, 2018)

Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Stephanie Weirich (Proc. ACM Program. Lang., 2018)

Overcoming Restraint: Modular Refinement using Cogent's Principled Foreign Function Interface. - Louis Cheung; Liam O'Connor; Christine Rizkallah (CoRR, 2021)

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Joshua M. Cohen; Stephanie Weirich (J. Funct. Program., 2021)

Cogent: uniqueness types and certifying compilation. - Liam O'Connor; Zilin Chen; Christine Rizkallah; Vincent Jackson; Sidney Amani; Gerwin Klein; Toby Murray; Thomas Sewell; Gabriele Keller (J. Funct. Program., 2021)

Overcoming restraint: composing verification of foreign functions with cogent. - Louis Cheung; Liam O'Connor; Christine Rizkallah (CPP, 2022)

Property-Based Testing: Climbing the Stairway to Verification. - Zilin Chen; Christine Rizkallah; Liam O'Connor; Partha Susarla; Gerwin Klein; Gernot Heiser; Gabriele Keller (SLE, 2022)

Dargent: A Silver Bullet for Verified Data Layout Refinement. - Zilin Chen; Ambroise Lafont; Liam O'Connor; Gabriele Keller; Craig McLaughlin; Vincent Jackson; Christine Rizkallah (Proc. ACM Program. Lang., 2023)

T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations. - Raphael Douglas Giles; Vincent Jackson; Christine Rizkallah (ICALP, 2024)

A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. - Vincent Jackson; Toby Murray; Christine Rizkallah (ITP, 2024)

Formally Verified Suffix Array Construction. - Louis Cheung; Christine Rizkallah (Arch. Formal Proofs, 2024)

Formalized Burrows-Wheeler Transform. - Louis Cheung; Alistair Moffat; Christine Rizkallah (CPP, 2025)

Formalised Burrows-Wheeler Transform. - Louis Cheung; Christine Rizkallah (Arch. Formal Proofs, 2025)

From Empirical Evaluation to Context-Aware Enhancement: Repairing Regression Errors with LLMs. - Anh Ho; Thanh Le-Cong; Bach Le 001; Christine Rizkallah (CoRR, 2025)