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.