Verifiable abstractions for contract-oriented systems
DOI10.1016/J.JLAMP.2015.10.005zbMATH Open1353.68194OpenAlexW2199920120MaRDI QIDQ347375FDOQ347375
Alceste Scalas, Roberto Zunino, Massimo Bartoletti, Maurizio Murgia
Publication date: 30 November 2016
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlamp.2015.10.005
Recommendations
Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Maude: specification and programming in rewriting logic
- On the Realizability of Contracts in Dishonest Systems
- Modelling and Verifying Contract-Oriented Systems in Maude
- Multiparty asynchronous session types
- A Semantic Deconstruction of Session Types
- Contract-Oriented Computing in CO2
- Title not available (Why is that?)
- A Theory of Agreements and Protection
- Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types
- CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements
- Subtyping for session types in the pi calculus
- Combining behavioural types with security analysis
- Twenty years of rewriting logic
- Compliance and Subtyping in Timed Session Types
- The Maude LTL model checker
- An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0
- Propositions as sessions
- On global types and multi-party sessions
- Synthesising Choreographies from Local Session Types
- Deadlock-freedom-by-design
- Lending Petri Nets and Contracts
- Choreographies, Logically
- Using Higher-Order Contracts to Model Session Types (Extended Abstract)
- Compliance in Behavioural Contracts: A Brief Survey
- Global Progress in Dynamically Interleaved Multiparty Sessions
- A Theory of Design-by-Contract for Distributed Multiparty Interactions
- Session Types as Intuitionistic Linear Propositions
- Title not available (Why is that?)
- Linear type theory for asynchronous session types
Cited In (8)
- Input urgent semantics for asynchronous timed session types
- Session-based concurrency in Maude: executable semantics and type checking
- Composition of synchronous communicating systems
- Probabilistic contracts for component-based design
- A fixed-points based framework for compliance of behavioural contracts
- Runtime verification of contracts with Themulus
- Probabilistic Contracts for Component-Based Design
- Honesty by Typing
Uses Software
This page was built for publication: Verifiable abstractions for contract-oriented systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q347375)
