Uniqueness types for efficient and verifiable aliasing-free embedded systems programming

DOI10.1007/978-3-030-34968-4_3MaRDI QIDQ6536347zbMATH OpenFDO

Authors Tuur Benoit, Bart Jacobs

Publication date 19 April 2024

zbMATH Keywords

formal verificationuniqueness types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Alias burying: Unique variables without destructive reads
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• Cogent: uniqueness types and certifying compilation
• A formally-verified alias analysis
• Uniqueness logic

Cites work

• scientific article; zbMATH DE number 4030948 (Why is no real title available?)
• scientific article; zbMATH DE number 48517 (Why is no real title available?)
• Building high integrity applications with SPARK
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Linear logic
• Practical affine types

This page was built for publication: Uniqueness types for efficient and verifiable aliasing-free embedded systems programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536347)