Verifiable abstractions for contract-oriented systems
DOI10.1016/J.JLAMP.2015.10.005zbMATH Open1353.68194OpenAlexW2199920120MaRDI QIDQ347375FDOQ347375
Authors: Massimo Bartoletti, Maurizio Murgia, Alceste Scalas, Roberto Zunino 
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
- Title not available (Why is that?)
- A semantic deconstruction of session types
- A theory of agreements and protection
- A theory of design-by-contract for distributed multiparty interactions
- An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0
- CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements
- Choreographies, logically
- Choreography synthesis as contract agreement
- Combining behavioural types with security analysis
- Compliance and subtyping in timed session types
- Compliance in behavioural contracts: a brief survey
- Contract-oriented computing in CO\(_2\)
- Deadlock-freedom-by-design, multiparty asynchronous global programming
- Global Progress in Dynamically Interleaved Multiparty Sessions
- Lending Petri nets and contracts
- Linear type theory for asynchronous session types
- Maude: specification and programming in rewriting logic
- Modelling and verifying contract-oriented systems in Maude
- Multiparty asynchronous session types
- Multiparty compatibility in communicating automata: characterisation and synthesis of global session types
- On global types and multi-party sessions
- On the realizability of contracts in dishonest systems
- Propositions as sessions
- Session types as intuitionistic linear propositions
- Subtyping for session types in the pi calculus
- Synthesising Choreographies from Local Session Types
- The Maude LTL model checker
- Twenty years of rewriting logic
- Using higher-order contracts to model session types (extended abstract)
Cited In (11)
- 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
- On the realizability of contracts in dishonest systems
- Runtime verification of contracts with Themulus
- Modelling and verifying contract-oriented systems in Maude
- Contract-oriented computing in CO\(_2\)
- Honesty by typing
- Probabilistic Contracts for Component-Based Design
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)
