The Road Ahead for Supervisor Synthesis -- Reentrancy? Yes. Reentrancy bug? No -- Graph Transformation Systems: a Semantics Based on (Stochastic) Symmetric Nets -- Modelling and Implementation of Unmanned Aircraft Collision Avoidance -- Randomized Re nement Checking of Timed I/O Automata -- Computing Linear Arithmetic Representation for Reachability Relation of One-counter Automata -- Compiling FL^{res} on Finite Words -- Symbolic Model Checking with Sentential Decision Diagrams -- Probably Approximately Correct Interpolants Generation -- Symbolic Verification of MPI Programs with Non-deterministic Synchronizations -- Learning Safe Neural Network Controllers with Barrier Certificates -- Software Defect-proneness Prediction Based on Package Cohesion and Coupling Metrics.