Aurea Bílý


Last Name

Bílý

First Name

Aurea

ORCID

0000-0002-9284-9161

Organisational unit

03653 - Müller, Peter / Müller, Peter

Filters

20252
Reset filters

Search Results

Publications 1 - 2 of 2
  • Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
    Item type: Conference Paper
    Grannan, Zachary; Bílý, Aurea; Fiala, Jonáš; et al. (2025)
    Proceedings of the ACM on Programming Languages
    Rust’s novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully understanding, extracting and exploiting these guarantees is subtle and challenging: existing models for Rust’s type checking either support a smaller idealised language disconnected from real-world Rust code, or come with severe limitations in terms of precise modelling of Rust borrows, composite types storing them, function signatures and loops. In this paper, we present Place Capability Graphs: a novel model of Rust’s type-checking results, which lifts these limitations, and which can be directly calculated from the Rust compiler’s own programmatic representations and analyses. We demonstrate that our model supports over 97% of Rust functions in the most popular public crates, and show its suitability as a general-purpose basis for verification and program analysis tools by developing promising new prototype versions of the existing Flowistry and Prusti tools.
  • A Refinement Methodology for Distributed Programs in Rust
    Item type: Conference Paper
    Bílý, Aurea; Pereira, João C.; Müller, Peter (2025)
    Proceedings of the ACM on Programming Languages
    Refinement relates an abstract system model to a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Top-down refinement techniques that automatically generate executable code generally produce implementations with sub-optimal performance. Bottom-up refinement allows one to reason about existing, efficient implementations, but imposes strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools. In this paper, we present a novel bottom-up refinement methodology that removes these limitations. Our methodology uses the familiar notion of guarded transition systems to express abstract models, but combines guards with a novel notion of \emph{locally-inductive invariants} to relate the abstract model \emph{locally} to concrete state. This approach is much more flexible than standard coupling invariants; in particular, it supports a wide range of program structures, data representations, and proof structures. We integrate our methodology as a library into Rust, leveraging the Rust type system to reason about ownership of guards. This integration allows one to use our methodology with an off-the-shelf Rust verification tool. It also facilitates practical applications, as we demonstrate on a number of substantial case studies including a concurrent implementation of Memcached.
Publications 1 - 2 of 2