2023/02/10 by Roberto Bagnara, Abramo Bagnara, Bagnara, Roberto +3 · 3 voices
Computer Science · #Logic, programming, and type systems #Security and Verification in Computing #Software Reliability and Analysis Research #cs.CR #cs.PL #cs.SE
paper · pdf · doi:10.48550/arxiv.2302.05331
openalex publication_date 2023/02/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
C-rusted is an innovative technology whereby C programs can be (partly) annotated so as to express: ownership, exclusivity and shareability of language, system and user-defined resources; dynamic properties of objects and the way they evolve during program execution; nominal typing and subtyping. The (partially) annotated C programs can be translated with unmodified versions of any compilation toolchain capable of processing ISO C code. The annotated C program parts can be validated by static analysis: if the static analyzer flags no error, then the annotations are provably coherent among themselves and with respect to annotated C code, in which case said annotated parts are provably exempt from a large class of logic, security, and run-time errors.