Write a Blog >>
Wed 21 Jun 2017 16:20 - 16:45 at Auditorium, Vertex Building - Analysis and Synthesis Chair(s): Anders Møller

Properties such as the absence of errors or bounds on mailbox sizes are hard to deduce statically for actor-based programs. This because actor-based programs exhibit several sources of unboundedness, in addition to the non-determinism that is inherent to the concurrent execution of actors. We present a static technique based on abstract interpretation to soundly reason about the possible executions of an actor-based program in a finite amount of time. We use our technique to statically verify the absence of errors in actor-based programs, and to compute upper bounds on the actors’ mailboxes. Sound abstraction of these mailboxes is crucial to the precision of any such technique. We provide several mailbox abstractions and categorize them according to the extent to which they preserve message ordering, and to the extent to which they preserve the multiplicity of messages in a mailbox. We formally prove the soundness of each mailbox abstraction, and empirically evaluate their precision and performance trade-offs on a corpus of benchmark programs. The results show that our technique can statically verify the absence of errors for more benchmark programs than the state-of-the-art analysis.

Wed 21 Jun

ecoop-2017-papers
15:30 - 17:10: ECOOP Research Papers - Analysis and Synthesis at Auditorium, Vertex Building
Chair(s): Anders MøllerAarhus University
ecoop-2017-papers15:30 - 15:55
Talk
Mikaël MayerEPFL, Switzerland, Jad HamzaLIAFA, Université Paris Diderot, Viktor KuncakEPFL, Switzerland
Link to publication Media Attached
ecoop-2017-papers15:55 - 16:20
Talk
Shiyou HuangTexas A&M University, Jeff HuangTexas A&M University
Link to publication Media Attached
ecoop-2017-papers16:20 - 16:45
Talk
Quentin StiévenartVrije Universiteit Brussel, Belgium, Jens NicolayVrije Universiteit Brussel, Belgium, Wolfgang De MeuterVrije Universiteit Brussel, Coen De RooverVrije Universiteit Brussel
Link to publication Pre-print Media Attached
ecoop-2017-papers16:45 - 17:10
Talk
Jeff HuangTexas A&M University, Arun Krishnakumar RajagopalanTexas A&M University
Link to publication Media Attached