Update: A Zoom link has been sent to all registered participants. If you would still like to attend please contact Xiaohong (email@example.com) or Maryam (firstname.lastname@example.org)
Displayed time zone: Chicago, IL, USA (GMT-5)
9:20 a.m. – 9:30 a.m.: Opening at SPIN, Chair: Grigore Rosu
9:30 a.m. – 10:30 a.m.: Invited Talk by Gul Agha, Chair: Ylies Falcone
Title: Verifying Concurrent Systems: Logics, Methods and the Problem of Scale
Abstract: Verification and validation methods are important tools for debugging concurrent systems. Much as we need a variety of tools to strengthen a physical structure, we need to deploy multiple formal models, logics
and reasoning methods to reduce bugs in concurrent systems. These methods can be characterized in terms of the scale at which they analyze temporal and spatial properties of a system. I will discuss the advantages and limitations of logics and reasoning methods at different scales–ranging from Statistical Model Checking and Euclidean Model Checking for at probabilistic verification of global behaviors, to decentralized runtime verification and targeted test generation for localized properties.
Talk Session 1: Chair: Christian Schilling
- 10:30 a.m. – 10:50 a.m.: “Bounded-Memory Runtime Enforcement” by Saumya Shankar, Antoine Rollet, Srinivas Pinisetty and Yliès Falcone.
- 10:50 a.m. – 11:10 a.m.: “Monitoring Cyber-Physical Systems using a Tiny Twin to Prevent Cyber-Attacks” by Fereidoun Moradi, Maryam Bagheri, Hanieh Rahmati, Hamed Yazdi, Sara Abbaspour Asadollah and Marjan Sirjani.
- 11:10 a.m. – 11:30 a.m.: “Automated Consistency Analysis for Legal Contracts” by Martin Kölbl, Alan Khoja, Stefan Leue and Rüdiger Wilhelmi.
- 11:30 a.m. – 11:50 a.m.: “Solving String Theories involving Regular Membership Predicates Using SAT” by Mitja Kulczynski, Kevin Lotz, Dirk Nowotka and Danny Bøgsted Poulsen.
11:50 a.m. – 1:00 p.m.: Lunch break
1:00 p.m. – 2:00 p.m.: Invited Talk by Sistla Prasad
Title: Automated Methods for Verification of Differential Privacy
Abstract: Differential privacy is a technique developed to preserve individuals’ privacy while performing statistical computations on databases containing private information. The differential privacy framework trades accuracy for privacy. In the framework, a differential privacy mechanism mediates data exchange between the database and data analyst. When the mechanism returns the answer to an analyst’s query, it introduces random noise in the query result before forwarding it to the analyst. Designing correct differential privacy mechanisms is subtle and error-prone, and even relatively minor tweaks to correct mechanisms can lead to loss of privacy.
In this talk, we present fully automated methods for verifying privacy and accuracy claims of Differential Privacy Mechanisms (DPM). We consider two different methods. In the first method, the DPM of interest is described as a program in a simple programming language that allows constructs for sampling from continuous probability distributions (such as Laplace etc.). In this method, the verification problem is reduced to the problem of checking validity of a formula in a fragment of first order theory of reals with exponentiation, which is known to be decidable. A tool implementing this technique has been built and employs Mathematica to check the formulas that are generated by the tool. This tool has been used to check the correctness as well as incorrectness of the claims of some well known DPMs presented in the literature. This tool has also been extended to check the accuracy claims of DPMs.
The second method uses an automata model in which some of the DPMs, presented in the literature, can be translated into. We give efficient algorithms, using simple graph algorithms, to check the privacy claims of the DPMs represented in this automata model. We show that this method is sound and complete for DPMs that can be translated into these automata.
Talk Session 2: Chair: Marjan Sirjani
- 2:00 p.m. – 2:20 p.m.: “Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signal” by Shiraj Arora, Rene Rydhof Hansen, Kim Guldstrand Larsen, Axel Legay and Danny Bøgsted Poulsen.
- 2:20 p.m. – 2:40 p.m.: “SpecRepair: Counter-Example Guided Safety Repair of Deep Neural Networks” by Fabian Bauer-Marquart, David Boetius, Stefan Leue and Christian Schilling.
- 2:40 p.m. – 3:00 p.m.: “Verifying the SHA-3 Implementation from OpenSSL with the Software Analysis Workbench” by Parker Hanson, Benjamin Winters, Eric Mercer and Brett Decker.
- 3:00 p.m. – 3:20 p.m.: “Synthesis of Rigorous Floating-Point Predicates” by Thanh Son Nguyen, Zvonimir Rakamaric and Ben Jones.
3:20 p.m. – 3:30 p.m.: Closing of SPIN 2022 by TBA