20 citations · 67 across the 17 of their papers we have counts for
17 papers
A model of actors and grey failures
Laura Bocchi, Julien Lange, Simon Thompson +1
Existing models for the analysis of concurrent processes tend to focus on fail-stop failures, where processes are either working or permanently stopped, and their state (working/st…
Proceedings 15th Interaction and Concurrency Experience
Clément Aubert, Cinzia Di Giusto, Larisa Safina +1
This volume contains the proceedings of ICE'22, the 15th Interaction and Concurrency Experience, which was held as an hybrid event in Lucca, Italy, and as a satellite event of DisC…
Provable GPU Data-Races in Static Race Detection
Dennis Liew, Tiago Cogumbreiro, Julien Lange
We extend the theory behind the Faial tool-chain, which can soundly prove that CUDA programs (aka, kernels) are data-race free using specialized behavioral types called memory acce…
kmclib: Automated Inference and Verification of Session Types
Keigo Imai, Julien Lange, Rumyana Neykova
Theories and tools based on multiparty session types offer correctness guarantees for concurrent programs that communicate using message-passing. These guarantees usually come at t…
A Session Subtyping Tool (Extended Version)
Lorenzo Bacchiani, Mario Bravetti, Julien Lange +1
Session types are becoming popular and have been integrated in several mainstream programming languages. Nevertheless, while many programming languages consider asynchronous fifo c…
Fair Asynchronous Session Subtyping
Mario Bravetti, Julien Lange, Gianluigi Zavattaro
Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component wi…
Featherweight Go
Robert Griesemer, Raymond Hu, Wen Kokke +5
We describe a design for generics in Go inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. Whereas subtyping in Java is nominal, in Go it is structura…
Bounded verification of message-passing concurrency in Go using Promela and Spin
Nicolas Dilley, Julien Lange
This paper describes a static verification framework for the message-passing fragment of the Go programming language. Our framework extracts models that over-approximate the messag…
A Sound Algorithm for Asynchronous Session Subtyping and its Implementation
Mario Bravetti, Marco Carbone, Julien Lange +2
Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a ver…
Verifying Asynchronous Interactions via Communicating Session Automata
Julien Lange, Nobuko Yoshida
This paper proposes a sound procedure to verify properties of communicating session automata (CSA), i.e., communicating automata that include multiparty session types. We introduce…
Fencing off Go: Liveness and Safety for Channel-based Programming (extended version)
Julien Lange, Nicholas Ng, Bernardo Toninho +1
Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) program…
Multiparty Compatibility for Concurrent Objects
Roly Perera, Julien Lange, Simon J. Gay
Objects and actors are communicating state machines, offering and consuming different services at different points in their lifecycle. Two complementary challenges arise when progr…
Characteristic Formulae for Session Types (extended version)
Julien Lange, Nobuko Yoshida
Subtyping is a crucial ingredient of session type theory and its applications, notably to programming language implementations. In this paper, we study effective ways to check whet…
Choreography Synthesis as Contract Agreement
Julien Lange, Alceste Scalas
We propose a formal model for distributed systems, where each participant advertises its requirements and obligations as behavioural contracts, and where multiparty sessions are st…
Synthesising Choreographies from Local Session Types (extended version)
Julien Lange, Emilio Tuosto
Designing and analysing multiparty distributed interactions can be achieved either by means of a global view (e.g. in choreography-based approaches) or by composing available compu…
A Modular Toolkit for Distributed Interactions
Julien Lange, Emilio Tuosto
We discuss the design, architecture, and implementation of a toolkit which supports some theories for distributed interactions. The main design principles of our architecture are f…
Amending Contracts for Choreographies
Laura Bocchi, Julien Lange, Emilio Tuosto
Distributed interactions can be suitably designed in terms of choreographies. Such abstractions can be thought of as global descriptions of the coordination of several distributed…