Opening, Keynote: Bounded STL Model Checking for Hybrid Systems
summary
Introduces a bounded STL model checking approach that reduces STL satisfiability to first‑order SMT: a STLmc bounded SMT checker encodes K variable “change points”, applies syntactic separation + signal discretization, and produces an SMT query whose satisfiability implies a counterexample with at most K variable points. The implementation supports nonlinear ODE solvers (dReal) and Z3 for linear cases, offers epsilon‑robustness (strengthening/weakening), is sound up to the given bounds, and scales on common hybrid‑system benchmarks (ODE cases slower with dReal).
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:47Hybrid systems and STL basics
- 8:31STL verification challenges
- 15:30Bounded model checking with SMT
- 24:49Encoding hybrid systems in SMT
- 31:00Syntactic separation for STL
- 43:15Generating SMT encoding
- 53:21Robustness and implementation
- 58:02Demo with counterexamples
- 1:00:20Experimental evaluation
- 1:01:02Summary and future work
- 1:02:48Q&A
related talks
20mFormal Analysis of Networked PLC Controllers Interacting with Physical Environments
30mInput-based Three-Valued Abstraction Refinement
30mOSVVM: Methodology, Library, and Models
21mDeductive Verification of Parameterized Embedded Systems modeled in SystemC
01h 00mDealing with Embedded Limitations
24mBioScript: Programming Safe Chemistry on Laboratories-on-a-Chip
01h 11mC++ in the World of Embedded Systems
05mModern C++ in Embedded OS Dev