Concise outlines for a complex logic: a proof outline checker for TaDA
From MaRDI portal
Publication:6145023
DOI10.1007/s10703-023-00427-warXiv2010.07080OpenAlexW4385418050MaRDI QIDQ6145023
Malte Schwerhoff, Felix A. Wolf, Peter Müller
Publication date: 8 January 2024
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2010.07080
formal methodssoftware verificationseparation logicautomated verificationfine-grained concurrencyprogram verifier
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Unnamed Item
- Unnamed Item
- Verification of sequential and concurrent programs
- An axiomatic proof technique for parallel programs
- An abstraction technique for describing concurrent program behaviour
- Starling: lightweight concurrency verification with views
- Automating deductive verification for weak-memory programs
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- A Program Logic for C11 Memory Fences
- CoLoSL: Concurrent Local Subjective Logic
- Modular Termination Verification for Non-blocking Concurrency
- Iris
- The Relationship Between Separation Logic and Implicit Dynamic Frames
- Views
- Caper
- Tackling Real-Life Relaxed Concurrency with FSL++
- Dafny: An Automatic Program Verifier for Functional Correctness
- Modular Safety Checking for Fine-Grained Concurrency
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- ReLoC
- Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
- Separation logic and abstraction
- CONCUR 2004 - Concurrency Theory
- CONCUR 2004 - Concurrency Theory
- Impredicative Concurrent Abstract Predicates
- Communicating State Transition Systems for Fine-Grained Concurrent Resources
This page was built for publication: Concise outlines for a complex logic: a proof outline checker for TaDA
