Christine Rizkallah

According to our database, Christine Rizkallah authored at least 35 papers between 2011 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

Formally Verified Suffix Array Construction.

Louis Cheung, Christine Rizkallah

Arch. Formal Proofs, 2024

A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras.

Vincent Jackson, Toby Murray, Christine Rizkallah

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations.

Raphael Douglas Giles, Vincent Jackson, Christine Rizkallah

Proceedings of the 51st International Colloquium on Automata, Languages, and Programming, 2024

2023

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., January, 2023

2022

Property-Based Testing: Climbing the Stairway to Verification.

Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser, Gabriele Keller

Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, 2022

Overcoming restraint: composing verification of foreign functions with cogent.

Louis Cheung, Liam O'Connor, Christine Rizkallah

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

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

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code.

Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua M. Cohen, Stephanie Weirich

J. Funct. Program., 2021

Overcoming Restraint: Modular Refinement using Cogent's Principled Foreign Function Interface.

Louis Cheung, Liam O'Connor, Christine Rizkallah

CoRR, 2021

2018

Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report).

Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich

Proc. ACM Program. Lang., 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.

Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich

CoRR, 2018

A Formal Equational Theory for Call-By-Push-Value.

Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Bringing Effortless Refinement of Data Layouts to Cogent.

Liam O'Connor, Zilin Chen, Partha Susarla, Christine Rizkallah, Gerwin Klein, Gabriele Keller

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Modeling, 2018

Total Haskell is reasonable Coq.

Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

Rank Maximal Equal Contribution: A Probabilistic Social Choice Function.

Haris Aziz, Pang Luo, Christine Rizkallah

Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018

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

Incompatibility of Efficiency and Strategyproofness in the Random Assignment Setting with Indifferences.

Haris Aziz, Pang Luo, Christine Rizkallah

CoRR, 2016

Compositional Security-Preserving Refinement for Concurrent Imperative Programs.

Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah

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

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 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

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency.

June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah

Proceedings of the Interactive Theorem Proving - 7th International Conference, 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

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference.

Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

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, Toby C. Murray, Gerwin Klein, Gernot Heiser

Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, 2016

2015

Verification of program computations.

Christine Rizkallah

PhD thesis, 2015

2014

Glivenko and Kuroda for Simple Type Theory.

Chad E. Brown, Christine Rizkallah

J. Symb. Log., 2014

A Framework for the Verification of Certifying Computations.

Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah

J. Autom. Reason., 2014

Verification of Certifying Computations through AutoCorres and Simpl.

Lars Noschinski, Christine Rizkallah, Kurt Mehlhorn

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

2013

An Axiomatic Characterization of the Single-Source Shortest Path Problem.

Christine Rizkallah

Arch. Formal Proofs, 2013

From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction.

Chad E. Brown, Christine Rizkallah

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2011

An Introduction to Certifying Algorithms.

Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah, Pascal Schweitzer

it Inf. Technol., 2011

Maximum Cardinality Matching.

Christine Rizkallah

Arch. Formal Proofs, 2011

Verification of Certifying Computations.

Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011