Write a Blog >>
ASE 2021
Mon 15 - Fri 19 November 2021 Australia

This program is tentative and subject to change.

Wed 17 Nov 2021 08:40 - 09:00 at Koala - Verification

Signal temporal logic (STL) is widely used to specify and analyze properties of cyber-physical systems with continuous behaviors. But STL model checking is still quite limited; existing STL model checking methods are either incomplete or very inefficient. This paper presents a new SMT-based model checking algorithm for verifying STL properties of cyber-physical systems. We propose a novel technique to reduce the STL bounded model checking problem to the satisfiability of a first-order logic formula over reals, which can be solved using state-of-the-art SMT solvers. Our algorithm is based on a new theoretical result, presented in this paper, to build a small but complete discretization of continuous signals, which preserves the bounded satisfiability of STL. Our modular translation method allows an efficient STL model checking algorithm that is refutationally complete for bounded signals, and that is much more scalable than the previous refutationally complete algorithm.

This program is tentative and subject to change.

Wed 17 Nov

Displayed time zone: Hobart change

08:00 - 09:00
VerificationResearch Papers at Koala
08:00
20m
Talk
Distribution Models for Falsification and Verification of DNNs
Research Papers
Felipe Toledo , David Shriver University of Virginia, Sebastian Elbaum University of Virginia, Matthew B Dwyer University of Virginia
Pre-print
08:20
20m
Talk
SATune: A Study-Driven Auto-Tuning Approach for Configurable Software Verification Tools
Research Papers
Ugur Koc University of Maryland, College Park, Austin Mordahl The University of Texas at Dallas, Shiyi Wei The University of Texas at Dallas, Jeffrey S. Foster Tufts University, Adam Porter University of Maryland
08:40
20m
Talk
Efficient SMT-Based Model Checking for Signal Temporal Logic
Research Papers
Jia Lee POSTECH, Geunyeol Yu Pohang University of Science and Technology (POSTECH), Kyungmin Bae Pohang University of Science and Technology (POSTECH)