Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 17:00 - 17:15 at VMCAI - Applications Chair(s): Rayna Dimitrova

Esterel is an imperative synchronous language that has found success in many safety-critical applications. Its precise semantics makes it natural for programming and reasoning. Existing techniques tackle either one of its main challenges: correctness checking or temporal veri- fication. To resolve the issues simultaneously, we propose a new solution via a Hoare-style forward verifier and a term rewriting system (T.r.s) on Synced Effects. The first contribution is, by deploying a novel effects logic, the verifier computes the deterministic program behaviour via construction rules at the source level, defining program evaluation syntactically. As a second contribution, by avoiding the complex translation from LTL formulas to Esterel programs, our purely algebraic T.r.s efficiently checks the temporal properties described by the expressive Synced Effects. We prototype this logic, prove its correctness and show our method’s feasibility using experimental results.

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30: ApplicationsVMCAI at VMCAI
Chair(s): Rayna DimitrovaCISPA Helmholtz Center for Information Security
17:00 - 17:15
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
Yahui SongNational University of Singapore, Wei-Ngan ChinNational University of Singapore
Media Attached
17:15 - 17:30
A Design of GPU-Based Quantitative Model Checking
YoungMin KwonSUNY Korea, Eunhee Kim2e Consulting Corp.
Media Attached