2026-07-24T12:05:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23352 2025-06-25T13:23:37Z ddc:004 open_access

Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness (Artifact) Carrott, Pedro Ayoun, Sacha-Élie Raad, Azalea Rust bug detection static analysis program logics under-approximation This artifact is a companion to the paper "Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness". It contains the Rocq formalisation of the RISL program logic, the RUXtBelt semantic model and the inadequacy theorem of RUXt. It also contains the OCaml prototype for RUXt, along with the case studies discussed in the paper. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pedro Carrott and Sacha-Élie Ayoun and Azalea Raad 2025 Is Part Of DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.11.2.9 urn:nbn:de:0030-drops-233529 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.9 eng https://creativecommons.org/licenses/by/4.0/legalcode