Concurrency and Objects Matter! Disentangling the Fabric of Real Operational Processes to Create Digital Twins -- Qualitative-Quantitative Reasoning: thinking informally about formal things -- Model Checking and Machine Learning Joining Forces in Uppaal -- Databases and Distributed Transactions Some Aspects of the Database Resilience -- On the Correctness Problem for Serializability -- Efficient Model Checking Methods A Set Automaton to Locate All Pattern Matches in a Term -- Groote Accelerating SpMV Multiplication in Probabilistic Model Checkers using GPUs -- A divide & conquer approach to conditional stable model checking -- Formalization and Verification in Coq and Isabelle Certifying Choreography Compilation -- Mechanically Verified Theory of Contracts -- A Complete Semantics of K and Its Translation to Isabelle -- Quantum Computing A New Connective in Natural Deduction, and its Application to Quantum Computing -- Security and Privacy An Incentive Mechanism for Trading Personal Data in Data Markets -- Palamidessi Assessing Security of Crypto-Currencies with Attack-Defense Trees: Proof of Concept and Future Directions -- Compositional Analysis of Protocol Equivalence in the Applied π-calculus using Quasi-Open Bisimilarity -- Card-based Cryptographic Protocols with a Standard Deck of Cards Using Private Operations -- Ono Normalising Lustre Preserves Security -- Synthesis and Learning Learning Probabilistic Automata using Residuals -- Deductive Synthesis of Sorting Algorithms in Theorema -- Reactive Synthesis from Visibly Register Pushdown Automata -- Systems Calculi and Analysis ComplexityParser: an automatic tool for certifying poly-time complexity of Java programs -- A Calculus for Attribute-based Memory Updates -- A Proof Method for Local Sufficient Completeness of Term Rewriting Systems.