Host: Alberto Griggio

Sessions

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