APLAS 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Mon 5 Dec 2022 14:00 - 14:30 at Seminar Room G007 - Testing and Verification Chair(s): Jonathan Aldrich

Although effect handlers offer a versatile abstraction for user-defined effects, they produce complex and less restricted execution traces due to the composable non-local control flow mechanisms. This paper is interested in the temporal behaviors of effect sequences, such as unhandled effects, termination of the communication, safety, fairness, etc. Specifically, we propose a novel effects logic ContEffs, to write precise and modular specifications for programs in the presence of user-defined effect handlers and primitive effects. As a second contribution, we devise a forward verifier together with a fixpoint calculator to infer the behaviors of such programs. Lastly, our automated verification framework provides a purely algebraic term-rewriting system (TRS) as the back-end solver, efficiently checking the entailments between ContEffs assertions.

To demonstrate the feasibility of our proposals, we prototype a verification system where zero-shot, one-shot, and multi-shot continuations coexist; prove its correctness; present experimental results; and report on case studies.

Mon 5 Dec

Displayed time zone: Auckland, Wellington change

13:30 - 15:00
Testing and VerificationAPLAS at Seminar Room G007
Chair(s): Jonathan Aldrich Carnegie Mellon University
13:30
30m
Talk
RHLE: Modular Deductive Verification of Relational ∀∃ Properties
APLAS
Robert Dickerson Purdue University, Qianchuan Ye Purdue University, Michael K. Zhang Purdue University, Benjamin Delaware Purdue University
14:00
30m
Talk
Automated Temporal Verification for Algebraic Effects
APLAS
Yahui Song National University of Singapore, Darius Foo National University of Singapore, Wei-Ngan Chin National University of Singapore
14:30
30m
Talk
Model-based Fault Classification for Automotive Software
APLAS
Mike Becker TU Braunschweig, Roland Meyer TU Braunschweig, Tobias Runge TU Braunschweig, Ina Schaefer KIT, Sören van der Wall PhD Student, Sebastian Wolff New York University