FTSCS 2023
who it's for
formal methods researchers, safety-critical systems engineers, verification engineers, embedded systems engineers, tool developers, assurance engineers, medical and avionics engineers
topics
bounded STL model checking; STL to SMT encoding; probabilistic risk assessment; parametric CTMC model checking; neural network coverage bounds; Boolean fault tree to QBF; folding SMT canonical narrowing; Maude symbolic reachability; Rust to SPARK bindings; C ABI layout for Rust interop; UPPAAL timed-automata models; UPPAAL SMC probabilistic checking
| title | author | length |
|---|---|---|
| Opening, Keynote: Bounded STL Model Checking for Hybrid Systems | Kyungmin Bae | 01h 07m |
Introduces a bounded STL model checking approach that reduces STL satisfiability to first‑order SMT: a STLmc bounded SMT checker encodes K variable “change… | ||
| Probabilistic Risk Assessment of an Obstacle Detection System for GoA 4 Freight ... | Mario Gleirscher, Anne E. Haxthausen, Jan Peleska | 27m |
Five-step quantitative procedure estimates false negative hazard for a GoA4 freight obstacle detector by composing a fault tree with parameter values from CTMC… | ||
| Solving Queries for Boolean Fault Tree Logic via Quantified SAT | Caz Saaltink, Stefano M. Nicoletti, Matthias Volk, Ernst Moritz Hahn, Mariëlle Stoelinga | 25m |
Provides a concrete BFL-to-QBF translation and a working implementation that uses Python + Z3 backend to check BFL properties, claiming it is the first tool… | ||
| Symbolic analysis by using folding narrowing with irreducibility and SMT constra... | Santiago Escobar, Raúl López-Rueda, Julia Sapiña | 32m |
Claims a new symbolic reachability engine that uses folding SMT canonical narrowing in Maude to turn some infinite narrowing trees into finite graphs… | ||
| Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Li... | Aïssata Maiga, Cyrille Artho, Florian Gilcher, Yannick Moy | 29m |
Implements safe Rust→SPARK bindings for a real BBQueue circular buffer, proving the approach works after iterative fixes and testing. Mirrors Rust types as… | ||
| Formal Verification of a Mechanical Ventilator using UPPAAL | Jaime Cuartas, David Cortés, Joan S. Betancourt, Jesús Aranda, José I. García, Andrés M. Valencia, James Ortiz | 32m |
Presents a formal UPPAAL model of a bare‑bones mechanical ventilator architecture, builds a timed‑automata network and checks 40 models against 14 properties… | ||
| Discussions, Closing | Peter Csaba Ölveczky, Cyrille Artho | 14m |
Workshop organizers report fewer submissions than expected and trace the drop to deadline clustering with related venues and rising AI/ML interest, propose… | ||
| nothing matches | ||