ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
DOI10.1007/978-3-030-44914-8_25OpenAlexW3021257004MaRDI QIDQ5041118
Naoki Kobayashi, Kohei Suenaga, Atsushi Igarashi, John Toman, Ren Siqi
Publication date: 13 October 2022
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2002.07770
aliasingtype systemsprogram verificationrefinement typesmutable referencesfractional ownershipsstrong updates
Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- Predicate Abstraction for Linked Data Structures
- Refinement types for Haskell
- Dependent types and multi-monadic effects in F*
- Compositional and Lightweight Dependent Type Inference for ML
- Widening for Control-Flow
- Dafny: An Automatic Program Verifier for Functional Correctness
- Deadlock-Free Channels and Locks
- A calculus with polymorphic and polyvariant flow types
- Quantified Heap Invariants for Object-Oriented Programs
- RustHorn: CHC-Based Verification for Rust Programs
- Low-level liquid types
- Permission accounting in separation logic
- Programming Languages and Systems
- Abstract Refinement Types
- A modular, polyvariant and type-based closure analysis
- Hybrid type checking
- Pick your contexts well
- HoIce: an ICE-based non-linear Horn clause solver
This page was built for publication: ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
