Mon 24 Aug 2020 23:30 - 23:45 at ICFP Asia 1 - Asia 1 Chair(s): Adam Chlipala
Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To modularly manage this complexity, network middleware has been traditionally built in layered stacks of components. We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal Logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to the operational semantics for stacks of distributed components. We successfully apply TLC to compose and verify a stack of fundamental distributed components.
Mon 24 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
11:30 - 13:00: New York 1ICFP Program at ICFP NY 1 Chair(s): Adam ChlipalaMassachusetts Institute of Technology | |||
11:30 - 11:45 Talk | Stable Relations and Abstract Interpretation of Higher-Order Programs ICFP Program DOI Media Attached File Attached | ||
11:45 - 12:00 Talk | Higher-Order Demand-Driven Symbolic Evaluation ICFP Program Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University DOI Media Attached | ||
12:00 - 12:15 Talk | Sparcl: A Language for Partially-Invertible Computation ICFP Program DOI Media Attached | ||
12:15 - 12:30 Talk | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs ICFP Program Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina DOI Media Attached | ||
12:30 - 12:45 Talk | TLC: Temporal Logic of Distributed Components ICFP Program Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside DOI Media Attached | ||
12:45 - 13:00 Talk | Effect Handlers, Evidently ICFP Program Ningning XieMicrosoft Research, USA, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Daniel HillerströmThe University of Edinburgh, Philipp SchusterUniversity of Tübingen, Germany, Daan LeijenMicrosoft Research, USA DOI Media Attached |
22:30 - 00:00: Asia 1ICFP Program at ICFP Asia 1 Chair(s): Adam ChlipalaMassachusetts Institute of Technology | |||
22:30 - 22:45 Talk | Stable Relations and Abstract Interpretation of Higher-Order Programs ICFP Program DOI Media Attached File Attached | ||
22:45 - 23:00 Talk | Higher-Order Demand-Driven Symbolic Evaluation ICFP Program Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University DOI Media Attached | ||
23:00 - 23:15 Talk | Sparcl: A Language for Partially-Invertible Computation ICFP Program DOI Media Attached | ||
23:15 - 23:30 Talk | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs ICFP Program Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina DOI Media Attached | ||
23:30 - 23:45 Talk | TLC: Temporal Logic of Distributed Components ICFP Program Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside DOI Media Attached | ||
23:45 - 00:00 Talk | Effect Handlers, Evidently ICFP Program Ningning XieMicrosoft Research, USA, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Daniel HillerströmThe University of Edinburgh, Philipp SchusterUniversity of Tübingen, Germany, Daan LeijenMicrosoft Research, USA DOI Media Attached |