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

zbMATH Keywords

aliasingtype systemsprogram verificationrefinement typesmutable referencesfractional ownershipsstrong updates

Mathematics Subject Classification ID

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

• Dafny
• SLAM
• Haskell
• SMT-LIB
• Spec#
• z3
• ESC/Java
• ASTREE
• Viper
• LiquidHaskell

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