activity
20112022
most citedBounded verification of message-passing concurrency in Go using Promela and Spin

20 citations · 33 across the 4 of their papers we have counts for

collaborators

7 papers

cs.PL20224 cited

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…

cs.PL2021

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…

cs.PL2020

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…

cs.PL202020 cited

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…

cs.PL20191 cited

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…

cs.PL2016

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…