View: session overviewtalk overviewside by side with other conferences

09:00 | Beyond Nash Equilibrium: Solution Concepts for the 21st Century SPEAKER: Joseph Halpern ABSTRACT. Nash equilibrium is the most commonly-used notion of equilibrium in game theory. However, it suffers from numerous problems. Some are well known in the game theory community; for example, the Nash equilibrium of repeated prisoner's dilemma is neither normatively nor descriptively reasonable. However, new problems arise when considering Nash equilibrium from a computer science perspective: for example, Nash equilibrium is not robust (it does not tolerate "faulty" or "unexpected" behavior), it does not deal with coalitions, it does not take computation cost into account, and it does not deal with cases where players are not aware of all aspects of the game. In this talk, I discuss solution concepts that try to address these shortcomings of Nash equilibrium. This talk represents joint work with various collaborators, including Ittai Abraham, Danny Dolev, Rica Gonen, Rafael Pass, and Leandro Rego. No background in game theory will be presumed. |

10:45 | Towards binary circuit models that faithfully reflect physical (un)solvability SPEAKER: Matthias Függer ABSTRACT. Binary circuit models are high-level abstractions intended to reflect the behavior of digital circuits, while restricting signal values to 0 and 1. Such models play an important role in assessing the correctness and performance characteristics of digital circuit designs: (i) modern circuit design relies on fast digital timing simulation tools and, hence, on accurate binary-valued circuit models that faithfully model signal propagation, even throughout a complex design, and (ii) binary circuit models provide a level of abstraction that is amenable to formal analysis. |

11:15 | Mechanical Verification of a Constructive Proof for FLP SPEAKER: Christina Rickmann ABSTRACT. We present a formalization of Völzer's paper "A constructive proof for FLP" using the interactive theorem prover Isabelle/HOL. We focus on the main differences between our proof and Völzer's and summarize necessary design decisions in our formal approach. |

11:45 | Having SPASS with Pastry and TLA+ SPEAKER: Noran Azmy ABSTRACT. Peer-to-peer protocols are becoming more and more popular for modern internet applications. While such protocols typically come with certain correctness and performance guarantees, verification attempts using formal methods invariably discover inconsistencies. We are interested in using the SPASS theorem prover for the verification of peer-to-peer protocols, that are modeled in the specification language TLA+. In addition to the specification language, TLA+ comes with its own verification tools: an interactive proof written in the TLA+ proof language consists of steps, or proof obligations, that are processed by TLA+'s own proof manager, and passed to one of several back-end provers such as Zenon or Isabelle/TLA. In 2013, Tianxiang Lu already made the first steps in the case of the protocol Pastry, where the author's attempt at formal verification reveals that the full protocol is incorrect with respect to a safety property which he calls “correct delivery”. His final proof of correctness is for a restricted version of the protocol and seriously lacks automation, due to the inability of current back-end provers to tackle proof obligations from this class of problems, which typically contain a mixture of uninterpreted functions, modular integer arithmetic, and set theory with the cardinality operator. Our ultimate goal is to create a SPASS back end for TLA+ that is better capable of solving this kind of proof obligations. This includes (1) the development of an efficient and effective translation from the strongly untyped, higher order TLA+ to a typed, first-order input language for SPASS, and (2) incorporating theory reasoning, typed reasoning and other necessary techniques into SPASS itself. In this paper, we give the first insights from running the current version of SPASS on the proof obligations from Lu's proof using a prototype, untyped translation. We also devise a modification to the current translation that achieves an impressive improvement in the way SPASS deals with the particularly problematic CHOOSE operator of TLA+. |

12:15 | Concurrent Data Structures: Semantics and (Quantitative) Relaxation SPEAKER: Ana Sokolova ABSTRACT. tbd |

14:30 | On Checking Correctness of Concurrent Data Structures SPEAKER: Ahmed Bouajjani ABSTRACT. We address the issue of checking the correctness of implementations of libraries of concurrent/distributed data structures. We present results concerning the verification of linearizability in the context of shared-memory concurrent data structures, and eventual consistency in the context of replicated, distributed data structures. This talk is based on joint work with Michael Emmi, Constantin Enea, and Jad Hamza. |