FTSCS 2022
who it's for
formal methods researchers, verification engineers, theorem prover users, embedded systems engineers, robotics software engineers, PLC developers, security analysts
topics
witness validator and verifier composition; parametric timed automata reachability; Maude with SMT symbolic analysis; statecharts to SMV and C refinement; timed opacity controller synthesis; narrowing-guided symbolic reachability; Isabelle/HOL memory isolation proofs; rewriting modulo SMT for PLC ST; synchronous language with refinement types; formal probabilistic risk assessment (BWR); DeepSEA smart contract verification; active corner collision avoidance certificates
| title | author | length |
|---|---|---|
| Cooperative Verification: Towards Reliable Safety-Critical Systems | Dirk Beyer | 01h 00m |
Field has 76 distinct Java/C verifiers and more than 40 entrants in recent competitions, so the proposal is to treat verification engines as composable… | ||
| Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata | Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, Laure Petrucci, Fredrik Rømming | 29m |
Rewriting-logic encoding of parametric timed automata yields a Maude-with-SMT symbolic reachability procedure that is proven sound and complete for PTA… | ||
| Q: A Sound Verification Framework for Statecharts and Their Implementations | Samuel D. Pollard, Robert C. Armstrong, John Bender, Geoffrey C. Hulette, Raheel S. Mahmood, Karla Morris, Blake C. Rawlings, Jon M. Aytac | 29m |
The Q Framework compiles Stateflow-style statecharts into SMV and generates ACSL contracts for a constrained C subset, proving a refinement relation between… | ||
| strategFTO: Untimed Control for Timed Opacity | Étienne André, Shapagat Bolat, Engel Lefaucheux, Dylan Marinho | 29m |
A prototype strategFTO prototype implements an algorithm that decides untimed control for timed opacity and shows the control problem is not harder than full… | ||
| Symbolic Reachability Analysis of Distributed Systems using Narrowing and Heuristic Search | Byeongjee Kang, Kyungmin Bae | 27m |
Proposes a narrowing-based reachability method guided by a heuristic scoring function (G for path cost plus H for error likelihood) that targets… | ||
| Proving Memory Access Violations in Isabelle/HOL | Sharar Ahmadi, Brijesh Dongol, Matt Griffin | 28m |
Verifies memory isolation for SmuV and TrustLite by translating compiled C through BAP and BIL into Isabelle/HOL theories, extending the pipeline to produce… | ||
| Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT | Jaeseo Lee, Sangki Kim, Kyungmin Bae | 28m |
Extends ST semantics to model scan cycles, program scheduling and timers so PLC behavior is cyclic and time-aware, then reduces LTL model checking to… | ||
| Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation | Jiawei Chen, José Luiz Vargas de Mendonça, Shayan Jalili, Bereket Ayele, Bereket Ngussie Bekele, Zhemin Qu, Pranjal Sharma, Tigist Shiferaw, Yicheng Zhang, Jean-Baptiste Jeannin | 29m |
A synchronous, stream-based language called MARVeLus combines Zelus-like discrete-time semantics with SMT-decidable refinement types to verify and then compile… | ||
| Formal Probabilistic Risk Assessment of a Nuclear Power Plant | Mohamed Abdelghany, Sofiène Tahar | 25m |
Formalizes a Boiling Water Reactor as a BWR functional block diagram in the HOL4 theorem prover, proves explicit event-class theorems (containment intact/fails… | ||
| Modelling a Blockchain for Smart Contract Verification using DeepSEA | Daniel Britten, Steve Reeves | 23m |
DeepSEA models the blockchain as a state record plus an inductive action type where each call requires a proof that it will succeed; this successful-call… | ||
| Towards a Formalization of the Active Corner Method for Collision Avoidance in PVS | Nishant Kheterpal, Jean-Baptiste Jeannin | 29m |
Automatic construction of a quantifier‑free explicit safe region for a convex polygon moving along a piecewise planar trajectory, together with a… | ||
| nothing matches | ||