Write a Blog >>
APLAS 2020
Mon 30 November - Wed 2 December 2020
Tue 1 Dec 2020 10:30 - 11:00 at online - Program Analysis and Verification Chair(s): Benjamin Delaware

Stream Runtime Verification (SRV) is a formal dynamic analysis technique that generalizes runtime verification algorithms from temporal logics like LTL to stream monitoring, allowing the computation of richer verdicts than Booleans (including quantitative and arbitrary data), while preserving explicit time offsets and future references. In this paper we study the problem of implementing an SRV engine that is easily extensible to arbitrary data types, and we propose a solution as a Haskell embedded domain specific language.

In spite of the theoretical clean separation in SRV between temporal dependencies and data computations, previous engines include ad-hoc implementations of a few data types, requiring complex changes in the tools to incorporate new data types.

We propose here an SRV language called hLola that borrows general Haskell types and embeds them transparently into an eDSL. This novel technique, which we call lift deep embedding, allows for example, the use of higher-order functions to implement static stream parameterization. We describe the Haskell implementation of hLola and illustrate simple extensions implemented using libraries, which would require long and error-prone additions in other ad-hoc SRV formalisms.

Tue 1 Dec

Displayed time zone: Osaka, Sapporo, Tokyo change

10:30 - 12:00
Program Analysis and VerificationResearch Papers at online
Chair(s): Benjamin Delaware Purdue University
10:30
30m
Talk
Declarative Stream Runtime Verification (hLola)
Research Papers
Martin Ceresa UNR - CIFASIS - CONICET, Felipe Gorostiaga IMDEA Software Institute, César Sánchez IMDEA Software Institute
11:00
30m
Talk
A Set-Based Context Model for Program Analysis
Research Papers
Zachary Palmer Swarthmore College, Scott F. Smith The Johns Hopkins University, Leandro Facchinetti The Johns Hopkins University, Ayaka Yorihiro Cornell University, Ke Wu Johns Hopkins University
11:30
30m
Talk
Formal Verification of Atomicity Requirements for Smart Contracts
Research Papers
Ning Han Capital Normal University, Ximeng Li Capital Normal University, Guohui Wang Capital Normal University, Beijing, China, Zhiping Shi Capital Normal University, Yong Guan Capital Normal University, Beijing, China