Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

workshop_5 [2014/06/29 14:47]
paulin [Lectures and abstract]
workshop_5 [2014/07/03 18:25] (current)
paulin [Planning]
Line 18: Line 18:
 ===== Planning ===== ===== Planning =====
 ^   ​Monday 7 July  ^^^ ^   ​Monday 7 July  ^^^
-|09h30-10h30 |                  |Registration and Introduction |+|09h30-10h30 |   ​Registration and Introduction ​ ||
 |10h30-11h30 |Andreas Abel      |Coinduction in Agda using Copatterns and Sized Types | |10h30-11h30 |Andreas Abel      |Coinduction in Agda using Copatterns and Sized Types |
 |11h30-12h15 |Stephanie Weirich |Combining Proofs and Programs in a Dependently Typed Language | |11h30-12h15 |Stephanie Weirich |Combining Proofs and Programs in a Dependently Typed Language |
 |14h00-14h45 |Brigitte Pientka ​ |Programming logical relations proofs | |14h00-14h45 |Brigitte Pientka ​ |Programming logical relations proofs |
-|14h45-15h30 |Tarmo Uustalu ​    ​|Precise qualification of effects with dependently typed monads | +|14h45-15h45 |Arthur Charguéraud |Interactive verification of stateful higher-order programs using characteristic formulae |
-|16h00-17h00 ​|Arthur Charguéraud |Interactive verification of stateful higher-order programs using characteristic formulae |+
 ^   ​Tuesday 8 July  ^^^ ^   ​Tuesday 8 July  ^^^
 |09h30-10h30 |Nobuko Yoshida |Idioms for Interaction and their applications in large distributed systems |  |09h30-10h30 |Nobuko Yoshida |Idioms for Interaction and their applications in large distributed systems | 
-|11h00-11h45 |Martin Hofmann ​|Abstract ​effects ​and proof-relevant logical relations ​|  +|11h00-11h45 |Tarmo Uustalu ​    |Precise qualification of effects ​with dependently typed monads ​
-|11h45-12h30 |Greg Morrisett |Engineering Challenges for Modeling Languages |+|11h45-12h30 |Greg Morrisett |Engineering Challenges for Modeling Languages ​(cancelled) ​|
 ^   ​Wednesday 9 July  ^^^ ^   ​Wednesday 9 July  ^^^
 |09h30-10h30 |Amal Ahmed |Compositional Compiler Verification for a Multi-language World | |09h30-10h30 |Amal Ahmed |Compositional Compiler Verification for a Multi-language World |
Line 33: Line 32:
 |11h45-12h30 |David Pichardie ​ |Atomicity Refinement for Verified Compilation | |11h45-12h30 |David Pichardie ​ |Atomicity Refinement for Verified Compilation |
 |14h30-15h15 |Steve Zdancewic |Vellvm: Verifying Transformations of the LLVM IR | |14h30-15h15 |Steve Zdancewic |Vellvm: Verifying Transformations of the LLVM IR |
-|15h15-16h00 |Francesco Zappa-Nardelli |Concurrency ​and compiler correctness ​|+|15h15-16h00 |Francesco Zappa-Nardelli |Concurrency: Still Tricky ​|
 |16h30-17h30 |Xavier Leroy  |Verified static analyses | |16h30-17h30 |Xavier Leroy  |Verified static analyses |
 +|18h00| ​ Cocktail ​ ||
 ^   ​Thursday 10 July  ^^^ ^   ​Thursday 10 July  ^^^
 |09h30-10h30| Derek Dreyer |GPS: Navigating weak memory with ghosts, protocols, and separation | |09h30-10h30| Derek Dreyer |GPS: Navigating weak memory with ghosts, protocols, and separation |
Line 43: Line 43:
 |16h30-17h30| Peter Sewell ​ |Before Certification:​ Engineering Validatable Models | |16h30-17h30| Peter Sewell ​ |Before Certification:​ Engineering Validatable Models |
 ^  Friday 11 July  ^^^ ^  Friday 11 July  ^^^
-|09h30-10h30|Nick Benton-Andrew Kennedy |Generating Certified x86 Code in a Proof Assistant | +|09h00-10h00| Nick Benton-Andrew Kennedy |Generating Certified x86 Code in a Proof Assistant | 
-|11h00-11h45|Adam Chlipala ​ |Bedrock: A Foundational Proof-Carrying Code Platform with Functional Correctness Proofs | +|10h00-10h45| Adam Chlipala ​ |Bedrock: A Foundational Proof-Carrying Code Platform with Functional Correctness Proofs | 
-|11h45-12h30|Dan Ghica |Compiling functional programs to distributed architectures using abstract machine nets | +|11h15-12h00| Dan Ghica |Compiling functional programs to distributed architectures using abstract machine nets |  
 +|12h00-12h45| Martin Hofmann |Abstract effects and proof-relevant logical relations ​
  
  
Line 61: Line 62:
     * The foundational proof-carrying code (FPCC) paradigm involves distributing software modules with proofs that they adhere to specifications of interest to end users.  When those specifications are detailed enough to fall under the umbrella of functional correctness,​ constructing the proofs presents a serious engineering challenge.  As with software engineering,​ it becomes important to find abstraction and modularity techniques that facilitate reuse of work across many code + proof packages. In my talk, I will give an overview of Bedrock, a project to design and implement a practical trusted core of a FPCC platform, plus an ecosystem of example tools targeting it.  Bedrock supports modular verification of assembly code via a notion of code + proof package inspired by the XCAP program logic.  We have built higher-level language implementations (for an extensible C-like language, a language with an integrated notion of mutable abstract data types, and a DSL for database-backed XML web services) and associated reasoning tools (automation for higher-order separation logic and for reasoning about abstract data types at a higher level).  The infrastructure has been used to do a complete modular verification of isolation properties for a software stack starting from simple nonblocking network operations and culminating in a multi-threaded,​ database-backed web service that has been deployed on mobile robots, and our ongoing work focuses on increasing the strength of such theorems while experimenting with higher-level programming notations, including general mathematical specifications via program synthesis.     * The foundational proof-carrying code (FPCC) paradigm involves distributing software modules with proofs that they adhere to specifications of interest to end users.  When those specifications are detailed enough to fall under the umbrella of functional correctness,​ constructing the proofs presents a serious engineering challenge.  As with software engineering,​ it becomes important to find abstraction and modularity techniques that facilitate reuse of work across many code + proof packages. In my talk, I will give an overview of Bedrock, a project to design and implement a practical trusted core of a FPCC platform, plus an ecosystem of example tools targeting it.  Bedrock supports modular verification of assembly code via a notion of code + proof package inspired by the XCAP program logic.  We have built higher-level language implementations (for an extensible C-like language, a language with an integrated notion of mutable abstract data types, and a DSL for database-backed XML web services) and associated reasoning tools (automation for higher-order separation logic and for reasoning about abstract data types at a higher level).  The infrastructure has been used to do a complete modular verification of isolation properties for a software stack starting from simple nonblocking network operations and culminating in a multi-threaded,​ database-backed web service that has been deployed on mobile robots, and our ongoing work focuses on increasing the strength of such theorems while experimenting with higher-level programming notations, including general mathematical specifications via program synthesis.
   * Derek Dreyer (Max-Planck Institute for Software Systems), GPS: Navigating weak memory with ghosts, protocols, and separation   * Derek Dreyer (Max-Planck Institute for Software Systems), GPS: Navigating weak memory with ghosts, protocols, and separation
-    * Compilers and CPUs routinely transform code in ways that are invisible to sequential code, but observable concurrently. ​ These transformations weaken the abstraction of shared memory, for example allowing different threads to observe writes in different orders, which complicates the already-difficult task of reasoning about +    * Compilers and CPUs routinely transform code in ways that are invisible to sequential code, but observable concurrently. ​ These transformations weaken the abstraction of shared memory, for example allowing different threads to observe writes in different orders, which complicates the already-difficult task of reasoning about concurrency. Worse still, they render impotent our most effective weaponry: the sophisticated formal methods that have been developed to tame concurrency almost universally assume a strong (sequentially consistent) memory model. This talk will present GPS, a new program logic that provides a full-fledged suite of modern verification techniques for reasoning under a weak memory model. ​  GPS includes a form of ghost state, rely-guarantee "​protocols",​ and separation logic --a combination that has been very fruitful for reasoning under strong memory. ​ The logic is specifically geared for reasoning about the recent C/C++11 memory model. ​ We demonstrate its effectiveness by applying it to challenging examples drawn from the Linux kernel, as well as lock-free data structures. ​ We will also briefly discuss the proof of soundness for GPS, which has been formalized in the Coq proof assistant.
-concurrency. Worse still, they render impotent our most effective weaponry: the sophisticated formal methods that have been developed to tame concurrency almost universally assume a strong (sequentially consistent) memory model. This talk will present GPS, a new program logic that provides a full-fledged suite of modern verification techniques for reasoning under a weak memory model. ​  GPS includes a form of ghost state, rely-guarantee "​protocols",​ and separation logic --a combination that has been very fruitful for reasoning under strong memory. ​ The logic is specifically geared for reasoning about the recent C/C++11 memory model. ​ We demonstrate its effectiveness by applying it to challenging examples drawn from the Linux kernel, as well as lock-free data structures. ​ We will also briefly discuss the proof of soundness for GPS, which has been formalized in the Coq proof assistant.+
   * Philippa Gardner (Imperial College, London), Abstract Disjointness,​ Abstract Atomicity and Abstract Connectivity   * Philippa Gardner (Imperial College, London), Abstract Disjointness,​ Abstract Atomicity and Abstract Connectivity
   * Dan Ghica (University of Birmingham),​ Compiling functional programs to distributed architectures using abstract machine nets   * Dan Ghica (University of Birmingham),​ Compiling functional programs to distributed architectures using abstract machine nets
Line 76: Line 76:
     * We consider the verified compilation of high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory synchronization and automatic memory management. Our development is framed in the context of the Total Store Order relaxed memory model. Ensuring complier correctness is challenging because high-level actions are translated into sequences of non-atomic actions with compiler-injected snippets of racy code; the behavior of this code depends not only on the actions of other threads,​ but also on out-of-order reorderings performed by the processor. A naïve proof of correctness would require reasoning over all possible thread interleavings,​ an impractical and non-scalable exercise. In this work we address this challenge with a refinement-based proof methodology that precisely relates concurrent code expressed at different abstraction levels, cognizant throughout of the relaxed memory semantics of the underlying processor. Our technique allows the compiler writer to reason compositionally about the atomicity of low-level concurrent code used to implement managed services. We validate the effectiveness of our approach by demonstrating the verified compilation of some non-trivial components of a realistic concurrent garbage collector.     * We consider the verified compilation of high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory synchronization and automatic memory management. Our development is framed in the context of the Total Store Order relaxed memory model. Ensuring complier correctness is challenging because high-level actions are translated into sequences of non-atomic actions with compiler-injected snippets of racy code; the behavior of this code depends not only on the actions of other threads,​ but also on out-of-order reorderings performed by the processor. A naïve proof of correctness would require reasoning over all possible thread interleavings,​ an impractical and non-scalable exercise. In this work we address this challenge with a refinement-based proof methodology that precisely relates concurrent code expressed at different abstraction levels, cognizant throughout of the relaxed memory semantics of the underlying processor. Our technique allows the compiler writer to reason compositionally about the atomicity of low-level concurrent code used to implement managed services. We validate the effectiveness of our approach by demonstrating the verified compilation of some non-trivial components of a realistic concurrent garbage collector.
   * Brigitte Pientka (Mc Gill), Programming logical relations proofs ​   * Brigitte Pientka (Mc Gill), Programming logical relations proofs ​
 +    * We will survey Beluga, a dependently typed programming and proof environment. It supports specifying formal systems in the logical framework LF and directly supports common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. Moreover, Beluga allows embedding LF objects together with their surrounding context in programs and supports recursive types to state properties about LF objects and their contexts. Concentrating on a weak normalization proof, ​ I will highlight several key aspects of Beluga and its design, in particular ​ the power to support first-class substitutions and logical relations proofs. Taken together these examples demonstrate the elegance and conciseness of Beluga for specifying, verifying and validating proofs.
   * Peter Sewell (University of Cambridge), Before Certification:​ Engineering Validatable Models   * Peter Sewell (University of Cambridge), Before Certification:​ Engineering Validatable Models
   * Tarmo Uustalu (Tallin University of Technology),​ Precise qualification of effects with dependently typed monads   * Tarmo Uustalu (Tallin University of Technology),​ Precise qualification of effects with dependently typed monads
Line 83: Line 84:
     * Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, Omega). ​ Here, we combine these two approaches into a single dependently-typed language, called Zombie. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness,​ and a call-by-value programming language that guarantees type safety but not termination. ​ The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can require logical proofs as arguments; and certain program values, including proofs computed at runtime, may be used as evidence by the logic. ​ This language allows programmers to work with total and partial functions uniformly, providing a smooth path from functional programming to dependently-typed programming.     * Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, Omega). ​ Here, we combine these two approaches into a single dependently-typed language, called Zombie. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness,​ and a call-by-value programming language that guarantees type safety but not termination. ​ The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can require logical proofs as arguments; and certain program values, including proofs computed at runtime, may be used as evidence by the logic. ​ This language allows programmers to work with total and partial functions uniformly, providing a smooth path from functional programming to dependently-typed programming.
   * Hongseok Yang (University of Oxford), Replicated Data Types: Specification,​ Verification,​ Optimality. Joint work with Sebastian Burckhardt at Microsoft Research Redmond, Alexey Gotsman at IMDEA Software Institute and Marek Zawirski at INRIA & UPMC-LIP6.   * Hongseok Yang (University of Oxford), Replicated Data Types: Specification,​ Verification,​ Optimality. Joint work with Sebastian Burckhardt at Microsoft Research Redmond, Alexey Gotsman at IMDEA Software Institute and Marek Zawirski at INRIA & UPMC-LIP6.
-    * Geographically distributed systems often rely on replicated eventually consistent data stores to achieve availability and performance. To resolve conflicting updates at different replicas, researchers and practitioners have proposed specialized consistency protocols, called replicated data types, that implement objects such as registers, counters, sets or lists. Reasoning about replicated data types has however not been on par with comparable work on abstract data types and concurrent data types, lacking specifications,​ correctness proofs, and optimality results. +    * Geographically distributed systems often rely on replicated eventually consistent data stores to achieve availability and performance. To resolve conflicting updates at different replicas, researchers and practitioners have proposed specialized consistency protocols, called replicated data types, that implement objects such as registers, counters, sets or lists. Reasoning about replicated data types has however not been on par with comparable work on abstract data types and concurrent data types, lacking specifications,​ correctness proofs, and optimality results. In this talk, I will explain our framework for specifying replicated data types using relations over events and verifying their implementations using replication-aware simulations. The framework has been applied to existing implementations of data types with nontrivial conflict-resolution strategies and optimizations (last-writer-wins register, counter, multi-value register and observed-remove set). If time permits, I will also explain a novel technique for obtaining lower bounds on the worst-case space overhead of data type implementations and show how it can be used to prove optimality of the implementations of well-known data types.
-In this talk, I will explain our framework for specifying replicated data types using relations over events and verifying their implementations using replication-aware simulations. The framework has been applied to existing implementations of data types with nontrivial conflict-resolution strategies and optimizations (last-writer-wins register, counter, multi-value register and observed-remove set). If time permits, I will also explain a novel technique for obtaining lower bounds on the worst-case space overhead of data type implementations and show how it can be used to prove optimality of the implementations of well-known data types.+
   * Nobuko Yoshida (Imperial College, London), Idioms for Interaction and their applications in large distributed systems   * Nobuko Yoshida (Imperial College, London), Idioms for Interaction and their applications in large distributed systems
     * We shall first talk how Kohei Honda invented the idea of session types. We shall then talk how Robin Milner, Honda and Yoshida started collaborations with industry to develop a web service protocol description language called Scribble and discovered the theory of multiparty session types through the collaborations. ​      We then give a summary of our recent research developments on multiparty session types for verifying distributed and concurrent ​ programs, and our collaborations with industry partners and a  major, long-term, NSF-funded project (Ocean Observatories ​     Initiatives) to provide an ultra large-scale cyberinfrustracture (OOI CI) for 25-30 years of sustained ocean measurements to study    climate variability,​ ocean circulation and ecosystem dynamics. We talk about the recent developments in Scribble and the runtime session monitoring framework currently used in the OOI CI.     * We shall first talk how Kohei Honda invented the idea of session types. We shall then talk how Robin Milner, Honda and Yoshida started collaborations with industry to develop a web service protocol description language called Scribble and discovered the theory of multiparty session types through the collaborations. ​      We then give a summary of our recent research developments on multiparty session types for verifying distributed and concurrent ​ programs, and our collaborations with industry partners and a  major, long-term, NSF-funded project (Ocean Observatories ​     Initiatives) to provide an ultra large-scale cyberinfrustracture (OOI CI) for 25-30 years of sustained ocean measurements to study    climate variability,​ ocean circulation and ecosystem dynamics. We talk about the recent developments in Scribble and the runtime session monitoring framework currently used in the OOI CI.
workshop_5.1404046054.txt.gz · Last modified: 2014/06/29 14:47 by paulin
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0