Write a Blog >>
Sun 20 - Fri 25 October 2019 Athens, Greece
Tue 22 Oct 2019 11:00 - 11:30 at Room 3A - Session 1

The actor model is a well-established way to approach to modularly designing and implementing concurrent and/or distributed systems, seeing increasing adoption in industry. But deductive verification tailored to actor programs remains underexplored; general concurrent logics could be used, but the logics are complex and full of features to reason about behaviors the actor model strives to avoid.

We explore a relatively lightweight approach of extending a system for proving {sequential} program correctness with means to prove safety properties of distributed actor programs (currently, assuming no faults). We borrow ideas from hybrid logic, a modal logic for stating assertions are true at a particular point in a model (in this case, a particular actor’s local state). To make such assertions useful, we stabilize them using rely-guarantee-style reasoning over local actor states, and only permit sending stable versions of these assertions to other actors. By carefully restricting the formation of assertions that a proposition is true at a certain actor, we avoid the need for actors to handle each others’ rely-guarantee relations explicitly.

We find that almost all of the required restrictions either fall out of established reference immutability techniques or can be implemented as a Dafny library, and outline the minor additional extensions that would be required for a sound implementation. We use this library to verify an actor variant of a classic rely-guarantee example (lower-bounding a montonic counter).

Tue 22 Oct
Times are displayed in time zone: Beirut change

11:00 - 12:30: Session 1AGERE at Room 3A
11:00 - 11:30
Modal Assertions for Actor Correctness
Colin GordonDrexel University
DOI Pre-print
11:30 - 12:00
Static Local Coordination Avoidance for Distributed Objects
Tim SoethoutING Bank and Centrum Wiskunde & Informatica (CWI), The Netherlands, Tijs van der StormCWI & University of Groningen, Netherlands, Jurgen VinjuCWI, Netherlands
DOI Pre-print Media Attached
12:00 - 12:30
Locations and Session Types in a Language with Higher-Order Reflection
Michael TranDepartment of Computer Science, Aalborg University, Denmark, Alexander Rønning BendixenDepartment of Computer Science, Aalborg University, Denmark, Bjarke Bredow BojesenDepartment of Computer Science, Aalborg University, Denmark, Hans HüttelDepartment of Computer Science, Aalborg University, Stian Lasse LybechDepartment of Computer Science, Aalborg University, Denmark