Meeting 67

Host: Alberto Griggio
Location: Trento, Italy
Dates: 9–13 October 2023

Talks

Mon, Oct 9

• Peter Müller, Proving Information Flow Security for Concurrent Programs
• Manfred Broy, Interaction, Concurrency, Nondeterminism, Time, Composition, Distribution, Abstraction: An Interface Centric Approach. Practical and Theoretical Consequences
• Shankar, The Kernel of Truth
• Rustan Leino, Tracked Regions

Tue, Oct 10

• Thomas Wies, Complete Multiparty Session Type Projection with Automata
• Stefano Tonetta, Safety Questions
• Joost-Pieter Katoen, Deductive Verification of Probabilistic Programs
• Bertrand Meyer, Requirements Engineering: The PEGS Approach

Wed, Oct 11

• Alberto Bombardelli, Compositional reasoning over asynchronous systems: a temporal logic-based approach
• Gianluca Redondi, Towards Verification of Railway Logic with Dafny and a Parameterized Model Checker
• Stefan Merz, Validating Traces of Distributed Systems Against TLA+ Specifications
• Joost-Pieter Katoen, Deductive Verification of Probabilistic Programs (continued)
• Shankar, Robust Proof and Code Generation

Thu, Oct 12

• Brijesh Dongol, Correctly Combining Concurrent and Persistent Transactional Memory
• Anna Becchi, Comparing legacy and modern implementations: migrating from analogical to software-based Railway Interlocking Systems
• Rustan Leino, Ghost Constructors
• Bertrand Meyer and Li Huang, Roaming the proof-test border
• Members’ Meeting

Fri, Oct 13

• Alberto Griggio, Formal verification in industry: a case study in automotive
• Stephan Merz, Towards an automatic proof of the Bakery Algorithm
• Alessandro Cimatti, A retrospective application of formal methods to safety critical software