arXiv subjects

Christine Rizkallah

Publications and source records attributed to Christine Rizkallah.

12 recordsLinked to original sources

arXiv2026

Optimising Metamath Proofs for Human Working Memory

Mathematical proofs vary in legibility. While most proof optimisation techniques seek to minimise proof size, the strategic reordering of inferences can reduce the working memory demand of proof checking without altering overall size. Metamath serves as a prime case study for this approach: its verification architecture requires proof steps to be ordered in a manner that prioritises algorithmic efficiency over readability. In this paper, we introduce algorithms to minimise both peak and cumulative memory consumption, applying the latter as a novel proxy for sustained human cognitive effort. We achieve this by representing proofs as directed acyclic graphs and modelling their execution as a pebbling game. Finding an optimal ordering via brute force is computationally infeasible, so we use heuristics to provide approximations. We apply these algorithms across Metamath's ZFC set theory library and present case studies demonstrating how automated reordering systematically improves the presentation of formal mathematics.

cs.LO↗

arXiv2026

From Empirical Evaluation to Context-Aware Enhancement: Repairing Regression Errors with LLMs

[...] Since then, various APR approaches, especially those leveraging the power of large language models (LLMs), have been rapidly developed to fix general software bugs. Unfortunately, the effectiveness of these advanced techniques in the context of regression bugs remains largely unexplored. This gap motivates the need for an empirical study evaluating the effectiveness of modern APR techniques in fixing real-world regression bugs. In this work, we conduct an empirical study of APR techniques on regression bugs. To facilitate our study, we introduce RegressionBug4APR, a high-quality benchmark of Java and Python regression bugs integrated into a framework designed to facilitate APR research. The current benchmark includes 200 regression bugs collected from widely used real-world GitHub repositories. We begin by conducting an in-depth analysis of the benchmark, demonstrating its diversity and quality. Building on this foundation, we empirically evaluate the capabilities of APR to regression bugs by assessing both traditional APR tools and advanced LLM-based APR approaches. Our experimental results show that classical APR tools fail to repair any bugs, while LLM-based APR approaches exhibit promising potential. Motivated by these results, we investigate impact of incorporating bug-inducing change information into LLM-based APR approaches for fixing regression bugs. We further conduct an ablation study to disaggregate the contribution of each contextual element within the bug-inducing change information. Our results highlight that this context-aware enhancement significantly improves the performance of LLM-based APR, yielding 1.6x more successful repairs compared to using LLM-based APR without such context. Moreover, our findings are consistent across both Java and Python benchmarks, providing preliminary evidence for the generalizability of our findings.

cs.SE↗

arXiv2026

Uniqueness is Separation

Value independence is enormously beneficial for reasoning about software systems at scale. These benefits carry over into the world of formal verification. Reasoning about programs algebraically is a simple affair in a proof assistant, whereas programs with unconstrained mutation necessitate much more complex techniques, such as Separation Logic, where invariants about memory safety, aliasing, and state changes must be established by manual proof. Uniqueness type systems allow programs to be compiled to code that uses mutation for efficiency, while retaining a semantics that enjoys value independence for reasoning. The restrictions of these type systems, however, are often too onerous for realistic software. Thus, most uniqueness type systems include some "escape hatch" where the benefits of value independence for reasoning are lost, but the restrictions of uniqueness types are lifted. To formally verify a system with such mixed guarantees, the value independence guarantees from uniqueness types must be expressed in terms of imperative, mutable semantics. In other words, we ought to express value independence as an assertion in Separation Logic.

cs.PL↗

arXiv2021

Overcoming Restraint: Composing Verification of Foreign Functions with Cogent

Cogent is a restricted functional language designed to reduce the cost of developing verified systems code. Because of its sometimes-onerous restrictions, such as the lack of support for recursion and its strict uniqueness type system, Cogent provides an escape hatch in the form of a foreign function interface (FFI) to C code. This poses a problem when verifying Cogent programs, as imported C components do not enjoy the same level of static guarantees that Cogent does. Previous verification of file systems implemented in Cogent merely assumed that their C components were correct and that they preserved the invariants of Cogent's type system. In this paper, we instead prove such obligations. We demonstrate how they smoothly compose with existing Cogent theorems, and result in a correctness theorem of the overall Cogent-C system. The Cogent FFI constraints ensure that key invariants of Cogent's type system are maintained even when calling C code. We verify reusable higher-order and polymorphic functions including a generic loop combinator and array iterators and demonstrate their application to several examples including binary search and the BilbyFs file system. We demonstrate the feasibility of verification of mixed Cogent-C systems, and provide some insight into verification of software comprised of code in multiple languages with differing levels of static guarantees.

cs.PL↗

arXiv2021

Overcoming Restraint: Composing Verification of Foreign Functions with Cogent

cs.PL↗

arXiv2018

Structural Operational Semantics for Control Flow Graph Machines

Compilers use control flow graph (CFG) representations of low-level programs because they are suited to program analysis and optimizations. However, formalizing the behavior and metatheory of CFG programs is non-trivial: CFG programs don't compose well, their semantics depends on auxiliary state, and, as a consequence, they do not enjoy a simple equational theory that can be used for reasoning about the correctness of program transformations. Lambda-calculus-based intermediate representations, in contrast, have well-understood operational semantics and metatheory, including rich equational theories, all of which makes them amenable to formal verification. This paper establishes a tight equivalence between (a variant of) Levy's call-by-push-value (CBPV) calculus and a control flow graph machine whose instructions are in static single assignment (SSA) form. The correspondence is made precise via a series of abstract machines that align the transitions of the structural operational semantics of the CBPV language with the computation steps of the SSA form. The target machine, which is derived from the CBPV language, accurately captures the execution model of control flow graphs, including direct jumps, mutually recursive code blocks, and multi-argument function calls, and the closure-free subset is similar to the SSA intermediate representations found in modern compilers such as LLVM and GCC. The definitions of all the language/abstract machine semantics and the theorems relating them are fully verified in Coq.

cs.PL↗

arXiv2018

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

Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell's containers library into Coq, and verify it against specifications that we derive from a variety of sources including type class laws, the library's test suite, and interfaces from Coq's standard library. Our work shows that it is feasible to verify mature, widely-used, highly optimized, and unmodified Haskell code. We also learn more about the theory of weight-balanced trees, extend hs-to-coq to handle partiality, and -- since we found no bugs -- attest to the superb quality of well-tested functional code.

cs.PL↗

arXiv2017

Total Haskell is Reasonable Coq

We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hs-to-coq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies -- a lawful Monad instance, "Hutton's razor", and an existing data structure library -- and prove their correctness. These examples show that this approach is viable: both that hs-to-coq applies to existing Haskell code, and that the output it produces is amenable to verification.

cs.PL↗

arXiv2017

Rank Maximal Equal Contribution: a Probabilistic Social Choice Function

When aggregating preferences of agents via voting, two desirable goals are to incentivize agents to participate in the voting process and then identify outcomes that are Pareto efficient. We consider participation as formalized by Brandl, Brandt, and Hofbauer (2015) based on the stochastic dominance (SD) relation. We formulate a new rule called RMEC (Rank Maximal Equal Contribution) that satisfies the strongest notion of participation and is also ex post efficient. The rule is polynomial-time computable and also satisfies many other desirable fairness properties. The rule suggests a general approach to achieving ex post efficiency and very strong participation.

cs.GT↗

arXiv2016

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

A fundamental resource allocation setting is the random assignment problem in which agents express preferences over objects that are then randomly allocated to the agents. In 2001, Bogomolnaia and Moulin presented the probabilistic serial (PS) mechanism that is an anonymous, neutral, Pareto optimal, and weak strategyproof mechanism when the preferences are considered with respect to stochastic dominance. The result holds when agents have strict preferences over individual objects. It has been an open problem whether there exists a mechanism that satisfies the same properties when agents may have indifference among the objects. We show that for this more general domain, there exists no extension of PS that is ex post efficient and weak strategyproof. The result is surprising because it does not even require additional symmetry or fairness conditions such as anonymity, neutrality, or equal treatment of equals. Our result further demonstrates that the lack of weak SD-strategyproofness of the extended PS mechanism of Katta and Sethuraman (2006) is not a design flaw of extended PS but is due to an inherent incompatibility of efficiency and strategyproofness of PS in the full preference domain.

cs.GT↗

arXiv2016

COGENT: Certified Compilation for a Functional Systems Language

We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions. The language is suited for layered systems code with minimal sharing such as file systems or network protocol control code. For a well-typed COGENT program, the compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly implements this embedding. The aim is for proof engineers to reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. We describe the formal verification stages of the compiler, which include automated formal refinement calculi, a switch from imperative update semantics to functional value semantics formally justified by the linear type system, and a number of standard compiler phases such as type checking and monomorphisation. The compiler certificate is a series of language-level meta proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.

cs.PL↗

arXiv2013

A Framework for the Verification of Certifying Computations

Formal verification of complex algorithms is challenging. Verifying their implementations goes beyond the state of the art of current automatic verification tools and usually involves intricate mathematical theorems. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for such a witness is usually much simpler than the original algorithm - yet it is all the user has to trust. The verification of checkers is feasible with current tools and leads to computations that can be completely trusted. We describe a framework to seamlessly verify certifying computations. We use the automatic verifier VCC for establishing the correctness of the checker and the interactive theorem prover Isabelle/HOL for high-level mathematical properties of algorithms. We demonstrate the effectiveness of our approach by presenting the verification of typical examples of the industrial-level and widespread algorithmic library LEDA.

cs.LO↗