Caper

DOI10.1007/978-3-662-54434-1_16zbMath1485.68060OpenAlexW4233335757MaRDI QIDQ2988651

Pedro da Rocha Pinto, Kristoffer Just Arndal Andersen, Thomas Dinsdale-Young, Lars Birkedal

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54434-1_16

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ A perspective on specifying and verifying concurrent modules ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ Abstract Specifications for Concurrent Maps

Uses Software

• z3
• VeriFast
• Smallfoot
• E Theorem Prover
• Viper
• Caper
• GitHub
• Algorithm 97

Cites Work

• Unnamed Item
• Resources, concurrency, and local reasoning
• Model theory.
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• CoLoSL: Concurrent Local Subjective Logic
• Iris
• System Description: E 1.8
• Views
• Modular Safety Checking for Fine-Grained Concurrency
• Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
• Compositional shape analysis by means of bi-abduction
• Separation logic and abstraction
• Permission accounting in separation logic
• Programming Languages and Systems
• Impredicative Concurrent Abstract Predicates
• Communicating State Transition Systems for Fine-Grained Concurrent Resources

This page was built for publication: Caper