Languages, Systems, and Data Seminar (Fall 2022)

Time: Fridays, noon - 1:05pm (PT)
Location: The Internet / The LSD Lab (Engineering 2, Room 398)
Organizers: Lindsey Kuper and Tyler Sorensen


The Languages, Systems, and Data Seminar meets weekly to discuss interesting topics in the areas of programming languages, systems, databases, formal methods, security, software engineering, verification, architecture, and beyond. Our goal is to encourage interactions and discussions between students, researchers, and faculty with interests in these areas. The seminar is open to everyone interested. Participating UCSC students should register for the 2-credit course CSE 280O (let the organizers know if you’re an undergrad and need a permission code).

For fall 2022, we will continue to host the LSD Seminar in a hybrid fashion. Anyone can attend on Zoom, and local folks can gather in person in the lab. Speakers can join either in person or on Zoom, whichever is convenient.

Talks will be advertised on the ucsc-lsd-seminar-announce (for anyone) and lsd-group (for UCSC-affiliated people) mailing lists.

Date Speaker Title
Sept. 23 None Lab social event and introductions
Sept. 30 Andrew Quinn TBD
Oct. 7 Liting Hu TBD
Oct. 14 Gan Shen TBD
Oct. 21 Tania Lorido Botran TBD
Oct. 28 Priyanka Mondal TBD
Nov. 4 Yahui Song Automated Temporal Verification with Extended Regular Expressions
Nov. 11 No meeting (Veterans Day)
Nov. 18 Abel Nieto TBD
Nov. 25 No meeting (Thanksgiving)
Dec. 2 Celeste Hollenbeck TBD

Sept. 30

Speaker: Andrew Quinn

Title: TBD

Abstract: TBD

Bio: TBD

Oct. 7

Speaker: Liting Hu

Title: TBD

Abstract: TBD

Bio: TBD

Oct. 14

Speaker: Gan Shen

Title: TBD

Abstract: TBD

Bio: TBD

Oct. 21

Speaker: Tania Lorido Botran

Title: TBD

Abstract: TBD

Bio: TBD

Oct. 28

Speaker: Priyanka Mondal

Title: TBD

Abstract: TBD

Bio: TBD

Nov. 4

Speaker: Yahui Song

Title: Automated Temporal Verification with Extended Regular Expressions

Abstract: Existing approaches to temporal verification have either sacrificed modularity in favor of achieving automation or vice-versa. To exploit the best of both worlds, we present a new framework to ensure temporal properties via Hoare-style verifiers and term rewriting systems (TRSs).

The leading technique of temporal verification is automata-based model checking, which has possible insufficiencies: (i) it requires a manual modeling stage and needs to be bounded when encountering non-terminating traces; (ii) to conveniently deploy existing inclusion-checkers for automata, the expressiveness power is limited by the finite-state automata; and (iii) there is always a gap between the verified logic and the actual implementation from the program.

To tackle these issues, we propose a framework that conducts local temporal verification, which leads to a modular and compositional verification strategy, where temporal reasoning can be combined to reason about the overall program. Meanwhile, we propose various effect logics to be the temporal specification languages, which are essentially extended regular expressions (REs), pushing the expressiveness boundary of the most deployed linear temporal logic (LTL). Furthermore, the proposed framework devises purely algebraic TRS to check the inclusions for the novel logics, avoiding the complex translation into automata.

We demonstrate the applicability of the proposed framework and various REs-based temporal logics in different domains; presents the corresponding prototype systems, case studies, experimental results, and necessary proofs.

Bio: Yahui Song is a 5th year PhD Student at the National University of Singapore (NUS), supervised by Associate Professor Chin Wei Ngan. Her interests are automated program verification and programming language design. Her current works are dedicated to more expressive and efficient temporal verification.

Nov. 18

Speaker: Abel Nieto

Title: TBD

Abstract: TBD

Bio: TBD

Dec. 2

Speaker: Celeste Hollenbeck

Title: TBD

Abstract: TBD

Bio: TBD


Archive