arXiv subjects

Remi Delmas

Publications and source records attributed to Remi Delmas.

4 recordsLinked to original sources

arXiv2026

Verifying the Rust Standard Library

Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic checks under Miri, but lacks static verification. We present what is, to the best of our knowledge, the largest verification campaign reported for a software library: an open, crowdsourced effort that integrates complementary verification tools into the continuous integration of a verification repository forked from the Rust standard library. We analyze the campaign's effectiveness, discuss the practical value of machine-checked proofs for a subset of undefined behaviors (e.g., out-of-bounds access, null and dangling pointer dereferences, and use of uninitialized memory), and frame the remaining obstacles as open challenges for the formal-methods community.

cs.LO↗

arXiv2026

Teaching LLMs Program Semantics via Symbolic Execution Traces

We introduce an evaluation framework of 500 C verification tasks across five property types (memory safety, overflow, termination, reachability, data races) built on SV-COMP 2025, and evaluate 14 models across six families. We find that high overall accuracy masks a critical weakness: while most models reliably confirm properties hold, violation detection varies widely and degrades sharply with program length. To close this gap, we train on formal verification artifacts: running the Soteria symbolic execution engine on generic open-source C code and using the resulting traces for continued pretraining of Qwen3-8B. Just ${\sim}$3,000 bug traces combined with chain-of-thought reasoning at inference time improve violation detection by over 17 percentage points, producing one of the most balanced accuracy profiles among evaluated models. On violation detection, the trained 8B model outperforms the 4$\times$ larger Qwen3-32B without thinking and approaches it in overall accuracy. The interaction between trace training and chain-of-thought is superadditive: neither alone provides meaningful gains, but their combination does. Improvements transfer across all five property types, including ones the training traces do not target. Our 28 configurations confirm the gains stem from trace semantics, not code volume, and that trace curation and format matter.

cs.SE↗

arXiv2025

ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis

Large language models have become proficient at generating functional code, but ensuring the output truly matches the programmer's intent remains difficult. Testing improves trust, yet for safety-critical applications, formal verification provides the only true guarantees through machine-checked proofs. However, verified code remains scarce compared to mainstream languages or mathematical theorem proving, limiting LLM capabilities in this domain. We present ATLAS, an automated pipeline that synthesizes verified programs to address this data bottleneck. Applied to the TACO dataset of Python solutions to LeetCode-style problems, ATLAS generates 2.7K verified Dafny programs, each with high-quality specifications and machine-checked proofs. Through task decomposition, we extract 19K training examples. Fine-tuning Qwen 2.5 7B Coder on this data improves performance from 32.4% to 56.9% on DafnyBench and from 15.8% to 65.8% on DafnySynthesis, demonstrating that synthetic data generation is a viable path to scaling LLM capabilities for formal verification.

cs.SE↗

arXiv2008

Algorithmic Based Fault Tolerance Applied to High Performance Computing

We present a new approach to fault tolerance for High Performance Computing system. Our approach is based on a careful adaptation of the Algorithmic Based Fault Tolerance technique (Huang and Abraham, 1984) to the need of parallel distributed computation. We obtain a strongly scalable mechanism for fault tolerance. We can also detect and correct errors (bit-flip) on the fly of a computation. To assess the viability of our approach, we have developed a fault tolerant matrix-matrix multiplication subroutine and we propose some models to predict its running time. Our parallel fault-tolerant matrix-matrix multiplication scores 1.4 TFLOPS on 484 processors (cluster jacquard.nersc.gov) and returns a correct result while one process failure has happened. This represents 65% of the machine peak efficiency and less than 12% overhead with respect to the fastest failure-free implementation. We predict (and have observed) that, as we increase the processor count, the overhead of the fault tolerance drops significantly.

cs.DC↗