Invited Papers
RoboWorld: Where Can My Robot Work?
Validating Safety Arguments with Lean
Run-time Analysis and Testing
Runtime Enforcement with Reordering, Healing, and Suppression
Monitoring First-Order Interval Logic
Exhaustive Property Oriented Model-based Testing With Symbolic Finite State Machines
nfer
A Tool for Event Stream Abstraction
Mining Shape Expressions with ShapeIt
Security and Privacy
Refining Privacy-Aware Data Flow Diagrams
Hybrid Information Flow Control for Low-level Code
Upper Bound Computation of Information Leakages for Unbounded Recursion
On the Security and Safety of AbU Systems
Parallel Composition/CSP and Probabilistic Reasoning
Parallelized sequential composition and hardware weak memory models
Checking Opacity and Durable Opacity with FDR
Translation of CCS into CSP, Correct up toStrong Bisimulation
Probabilistic BDI Agents: Actions, Plans, and Intentions
A Debugger for Probabilistic Programs
Verification and Synthesis
Verification of Programs with Exceptions through Operator-Precedence Automata
Counterexample Classification
Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines
Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL synthesis
TACoS: A Tool for MTL Controller Synthesis
Emerging Domains
Lightweight Nontermination Inference with CHCs
A Denotational Semantics of Solidity in Isabelle/HOL
Configuration Space Exploration for Digital Printing Systems
Bit-precise Verification of Discontinuity Errors Under Fixed-point Arithmetic
Machine Learning and Cyber-Physical Systems
OSIP: Tightened Bound Propagation for the Verification of ReLU Neural Networks
Active Model Learning of Stochastic Reactive Systems
Mixed-Neighborhood, Multi-Speed Cellular Automata for Safety-Aware Pedestrian Prediction.