DROPS

Volume

OASIcs, Volume 43

2014 Imperial College Computing Student Workshop

ICCSW 2014, September 25-26, 2014, London, United Kingdom

Editors: Rumyana Neykova and Nicholas Ng

Document

Artifact

DOI: 10.4230/DARTS.8.2.9

Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact)

Authors: Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract

This artifact contains a version of MultiCrusty, a Rust library designed for writing and checking communication protocols following the Affine Multiparty Session Types theory introduced in our ECOOP'22 paper. MultiCrusty can work, and should be used, with Scribble [Yoshida et al., 2014] and kMC [{Julien} {Lange} and {Nobuko} {Yoshida}, 2019]: with the former tool, users can write correct global protocols and project them onto local Rust types defined within MultiCrusty, this approach is qualified as top-down; while the latter tool allows to check local Rust types written by users, this approach is qualified as bottom-up. Our artifact contains those three tools, their respective source files, as well as the different examples and benchmarks introduced in our paper, all together within a Docker image.

Cite as

Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{lagaillardie_et_al:DARTS.8.2.9,
  author =	{Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
  title =	{{Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact)}},
  pages =	{9:1--9:16},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.9},
  URN =		{urn:nbn:de:0030-drops-162075},
  doi =		{10.4230/DARTS.8.2.9},
  annote =	{Keywords: Rust language, affine multiparty session types, failures, cancellation}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2022.4

Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types

Authors: Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract

Communicating systems comprise diverse software components across networks. To ensure their robustness, modern programming languages such as Rust provide both strongly typed channels, whose usage is guaranteed to be affine (at most once), and cancellation operations over binary channels. For coordinating components to correctly communicate and synchronise with each other, we use the structuring mechanism from multiparty session types, extending it with affine communication channels and implicit/explicit cancellation mechanisms. This new typing discipline, affine multiparty session types (AMPST), ensures cancellation termination of multiple, independently running components and guarantees that communication will not get stuck due to error or abrupt termination. Guided by AMPST, we implemented an automated generation tool (MultiCrusty) of Rust APIs associated with cancellation termination algorithms, by which the Rust compiler auto-detects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanism for communication, synchronisation and propagation of the notifications of cancellation for arbitrary processes. We have implemented several usecases, including popular application protocols (OAuth, SMTP), and protocols with exception handling patterns (circuit breaker, distributed logging).

Cite as

Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{lagaillardie_et_al:LIPIcs.ECOOP.2022.4,
  author =	{Lagaillardie, Nicolas and Neykova, Rumyana and Yoshida, Nobuko},
  title =	{{Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{4:1--4:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.4},
  URN =		{urn:nbn:de:0030-drops-162324},
  doi =		{10.4230/LIPIcs.ECOOP.2022.4},
  annote =	{Keywords: Rust language, affine multiparty session types, failures, cancellation}
}

Document

Artifact

DOI: 10.4230/DARTS.6.2.18

Multiparty Session Programming with Global Protocol Combinators (Artifact)

Authors: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract

In the paper "Multiparty Session Programming with Global Protocol Combinators", we introduce a library, ocaml-mpst for programming with global combinators - a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language. This artifact is the source code of ocaml-mpst, with all the examples and benchmarks discussed in the paper.

Cite as

Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming with Global Protocol Combinators (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 18:1-18:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{imai_et_al:DARTS.6.2.18,
  author =	{Imai, Keigo and Neykova, Rumyana and Yoshida, Nobuko and Yuen, Shoji},
  title =	{{Multiparty Session Programming with Global Protocol Combinators (Artifact)}},
  pages =	{18:1--18:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Imai, Keigo and Neykova, Rumyana and Yoshida, Nobuko and Yuen, Shoji},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.6.2.18},
  URN =		{urn:nbn:de:0030-drops-132159},
  doi =		{10.4230/DARTS.6.2.18},
  annote =	{Keywords: Multiparty Session Types, Communication Protocol, Concurrent and Distributed Programming, OCaml}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2020.9

Multiparty Session Programming With Global Protocol Combinators

Authors: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract

Multiparty Session Types (MPST) is a typing discipline for communication protocols. It ensures the absence of communication errors and deadlocks for well-typed communicating processes. The state-of-the-art implementations of the MPST theory rely on (1) runtime linearity checks to ensure correct usage of communication channels and (2) external domain-specific languages for specifying and verifying multiparty protocols. To overcome these limitations, we propose a library for programming with global combinators - a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. We formalise global combinators and prove a sound realisability of global combinators - a well-typed global combinator derives a set of local types, by which typed endpoint programs can ensure type and communication safety. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language. We compare our implementation to untyped and continuation-passing style implementations, and demonstrate its expressiveness by implementing a plethora of protocols. We show our library can interoperate with existing libraries and services, implementing DNS (Domain Name Service) protocol and the OAuth (Open Authentication) protocol.

Cite as

Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming With Global Protocol Combinators. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 9:1-9:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{imai_et_al:LIPIcs.ECOOP.2020.9,
  author =	{Imai, Keigo and Neykova, Rumyana and Yoshida, Nobuko and Yuen, Shoji},
  title =	{{Multiparty Session Programming With Global Protocol Combinators}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{9:1--9:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.9},
  URN =		{urn:nbn:de:0030-drops-131662},
  doi =		{10.4230/LIPIcs.ECOOP.2020.9},
  annote =	{Keywords: Multiparty Session Types, Communication Protocol, Concurrent and Distributed Programming, OCaml}
}

Document

Complete Volume

DOI: 10.4230/OASIcs.ICCSW.2014

OASIcs, Volume 43, ICCSW'14, Complete Volume

Authors: Rumyana Neykova and Nicholas Ng

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

OASIcs, Volume 43, ICCSW'14, Complete Volume

Cite as

2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Proceedings{neykova_et_al:OASIcs.ICCSW.2014,
  title =	{{OASIcs, Volume 43, ICCSW'14, Complete Volume}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014},
  URN =		{urn:nbn:de:0030-drops-47809},
  doi =		{10.4230/OASIcs.ICCSW.2014},
  annote =	{Keywords: Languages and Compilers, Parallel Architectures, Applicative (Functional) Programming, Parallel Programming, Requirements/Specifications Software/Program Verification, Concurrent Programming, Complexity Measures and Classes, Specifying and Verifying and Reasoning about Programs,}
}

Document

Front Matter

DOI: 10.4230/OASIcs.ICCSW.2014.i

Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Rumyana Neykova and Nicholas Ng

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

Frontmatter, Table of Contents, Preface, Workshop Organization

Cite as

2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. i-xiii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{neykova_et_al:OASIcs.ICCSW.2014.i,
  author =	{Neykova, Rumyana and Ng, Nicholas},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{i--xiii},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.i},
  URN =		{urn:nbn:de:0030-drops-47647},
  doi =		{10.4230/OASIcs.ICCSW.2014.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}

Document

DOI: 10.4230/OASIcs.ICCSW.2014.1

From academia to industry: The story of Google DeepMind

Authors: Shane Legg

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

Shane Legg left academia to cofound DeepMind Technologies in 2010, along with Demis Hassabis and Mustafa Suleyman. Their vision was to bring together cutting edge machine learning and systems neuroscience in order to create artificial agents with general intelligence. Following investments from a number of famous technology entrepreneurs, including Peter Thiel and Elon Musk, they assembled a team of world class researchers with backgrounds in systems neuroscience, deep learning, reinforcement learning and Bayesian statistics. In early 2014 DeepMind made international business headlines after it was acquired by Google. In this talk Shane covers some of the history behind DeepMind, his experience making the transition from academia to industry, how Google DeepMind performs research and finally some demos of the artificial agents that are under development.

Cite as

Shane Legg. From academia to industry: The story of Google DeepMind. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{legg:OASIcs.ICCSW.2014.1,
  author =	{Legg, Shane},
  title =	{{From academia to industry: The story of Google DeepMind}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{1--1},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.1},
  URN =		{urn:nbn:de:0030-drops-47650},
  doi =		{10.4230/OASIcs.ICCSW.2014.1},
  annote =	{Keywords: machine learning}
}

Document

DOI: 10.4230/OASIcs.ICCSW.2014.2

You and Your Research and the Elements of Style

Authors: Philip Wadler

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

This talk surveys advice from experts, including Richard Hamming, William Strunk, E. B. White, Donald Knuth, and others, on how to conduct your research and communicate your results.

Cite as

Philip Wadler. You and Your Research and the Elements of Style. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, p. 2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{wadler:OASIcs.ICCSW.2014.2,
  author =	{Wadler, Philip},
  title =	{{You and Your Research and the Elements of Style}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{2--2},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.2},
  URN =		{urn:nbn:de:0030-drops-47669},
  doi =		{10.4230/OASIcs.ICCSW.2014.2},
  annote =	{Keywords: research, communication}
}

Document

DOI: 10.4230/OASIcs.ICCSW.2014.3

History-Based Adaptive Work Distribution

Authors: Evgenij Belikov

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

Exploiting parallelism of increasingly heterogeneous parallel architectures is challenging due to the complexity of parallelism management. To achieve high performance portability whilst preserving high productivity, high-level approaches to parallel programming delegate parallelism management, such as partitioning and work distribution, to the compiler and the run-time system. Random work stealing proved efficient for well-structured workloads, but neglects potentially useful context information that can be obtained through static analysis or monitoring at run time and used to improve load balancing, especially for irregular applications with highly varying thread granularity and thread creation patterns. We investigate the effectiveness of an adaptive work distribution scheme to improve load balancing for an extension of Haskell which provides a deterministic parallel programming model and supports both shared-memory and distributed-memory architectures. This scheme uses a less random work stealing that takes into account information on past stealing successes and failures. We quantify run time performance, communication overhead, and stealing success of four divide-and-conquer and data parallel applications for three different update intervals on a commodity 64-core Beowulf cluster of multi-cores.

Cite as

Evgenij Belikov. History-Based Adaptive Work Distribution. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. 3-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{belikov:OASIcs.ICCSW.2014.3,
  author =	{Belikov, Evgenij},
  title =	{{History-Based Adaptive Work Distribution}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{3--10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.3},
  URN =		{urn:nbn:de:0030-drops-47671},
  doi =		{10.4230/OASIcs.ICCSW.2014.3},
  annote =	{Keywords: Adaptive Load Balancing, Work Stealing, Work Pushing, High-Level Parallel Programming, Context-Awareness}
}

Document

DOI: 10.4230/OASIcs.ICCSW.2014.11

Everything you know is wrong: The amazing time traveling CPU, and other horrors of concurrency

Authors: Ethel Bardsley

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

In this paper, we shall explore weak memory models, their insidious effects, and how it could happen to you! It shall explained how and why both compilers and CPUs rewrite your program to make it faster, the inevitable fallout of this, and what you can do to protect your code. We shall craft a lock, building from a naïve and broken implementation up to a safe and correct form, and study the underlying model that requires these modifications as we go.

Cite as

Ethel Bardsley. Everything you know is wrong: The amazing time traveling CPU, and other horrors of concurrency. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. 11-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{bardsley:OASIcs.ICCSW.2014.11,
  author =	{Bardsley, Ethel},
  title =	{{Everything you know is wrong: The amazing time traveling CPU, and other horrors of concurrency}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{11--18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.11},
  URN =		{urn:nbn:de:0030-drops-47688},
  doi =		{10.4230/OASIcs.ICCSW.2014.11},
  annote =	{Keywords: Concurrency, weak memory, compilers}
}

Document

DOI: 10.4230/OASIcs.ICCSW.2014.19

Identifying and inferring objects from textual descriptions of scenes from books

Authors: Andrew Cropper

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

Fiction authors rarely provide detailed descriptions of scenes, preferring the reader to fill in the details using their imagination. Therefore, to perform detailed text-to-scene conversion from books, we need to not only identify explicit objects but also infer implicit objects. In this paper, we describe an approach to inferring objects using Wikipedia and WordNet. In our experiments, we are able to infer implicit objects such as monitor and computer by identifying explicit objects such as keyboard.

Cite as

Andrew Cropper. Identifying and inferring objects from textual descriptions of scenes from books. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. 19-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{cropper:OASIcs.ICCSW.2014.19,
  author =	{Cropper, Andrew},
  title =	{{Identifying and inferring objects from textual descriptions of scenes from books}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{19--26},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.19},
  URN =		{urn:nbn:de:0030-drops-47690},
  doi =		{10.4230/OASIcs.ICCSW.2014.19},
  annote =	{Keywords: Text-to-Scene Conversion, Natural Language Processing, Artificial Intelligence}
}

Document

DOI: 10.4230/OASIcs.ICCSW.2014.27

Predicate Abstraction in Program Verification: Survey and Current Trends

Authors: Jakub Daniel and Pavel Parízek

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

A popular approach to verification of software system correctness is model checking. To achieve scalability needed for large systems, model checking has to be augmented with abstraction. In this paper, we provide an overview of selected techniques of program verification based on predicate abstraction. We focus on techniques that advanced the state-of-the-art in a significant way, including counterexample-guided abstraction refinement, lazy abstraction, and current trends in the form of extensions targeting, for example, data structures and multi-threading. We discuss limitations of these techniques and present our plans for addressing some of them.

Cite as

Jakub Daniel and Pavel Parízek. Predicate Abstraction in Program Verification: Survey and Current Trends. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. 27-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{daniel_et_al:OASIcs.ICCSW.2014.27,
  author =	{Daniel, Jakub and Par{\'\i}zek, Pavel},
  title =	{{Predicate Abstraction in Program Verification: Survey and Current Trends}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{27--35},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.27},
  URN =		{urn:nbn:de:0030-drops-47706},
  doi =		{10.4230/OASIcs.ICCSW.2014.27},
  annote =	{Keywords: program verification, model checking, predicate abstraction, refinement}
}

Document

DOI: 10.4230/OASIcs.ICCSW.2014.36

Automatic Verification of Data Race Freedom in Device Drivers

Authors: Pantazis Deligiannis and Alastair F. Donaldson

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

Device drivers are notoriously hard to develop and even harder to debug. They are typically prone to many serious issues such as data races. In this paper, we present static pair-wise lock set analysis, a novel sound verification technique for proving data race freedom in device drivers. Our approach not only avoids reasoning about thread interleavings, but also allows the reuse of existing successful sequential verification techniques.

Cite as

Pantazis Deligiannis and Alastair F. Donaldson. Automatic Verification of Data Race Freedom in Device Drivers. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. 36-39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{deligiannis_et_al:OASIcs.ICCSW.2014.36,
  author =	{Deligiannis, Pantazis and Donaldson, Alastair F.},
  title =	{{Automatic Verification of Data Race Freedom in Device Drivers}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{36--39},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.36},
  URN =		{urn:nbn:de:0030-drops-47715},
  doi =		{10.4230/OASIcs.ICCSW.2014.36},
  annote =	{Keywords: Device Drivers, Verification, Concurrency, Data Races}
}

Document

DOI: 10.4230/OASIcs.ICCSW.2014.40

A survey of modelling and simulation software frameworks using Discrete Event System Specification

Authors: Romain Franceschini, Paul-Antoine Bisgambiglia, Luc Touraille, Paul Bisgambiglia, and David Hill

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

Abstract

Discrete Event System Specification is an extension of the Moore machine formalism which is used for modelling and analyzing general systems. This hierarchical and modular formalism is time event based and is able to represent any continuous, discrete or combined discrete and continuous systems. Since its introduction by B.P. Zeigler at the beginning of the eighties, most general modelling formalisms able to represent dynamic systems have been subsumed by DEVS. Meanwhile, the modelling and simulation (M&S) community has introduced various software frameworks supporting DEVS-based simulation analysis capability. DEVS has been used in many application domains and this paper will present a technical survey of the major DEVS implementations and software frameworks. We introduce a set of criteria in order to highlight the main features of each software tool, then we propose a table and discussion enabling a fast comparison of the presented frameworks.

Cite as

Romain Franceschini, Paul-Antoine Bisgambiglia, Luc Touraille, Paul Bisgambiglia, and David Hill. A survey of modelling and simulation software frameworks using Discrete Event System Specification. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. 40-49, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{franceschini_et_al:OASIcs.ICCSW.2014.40,
  author =	{Franceschini, Romain and Bisgambiglia, Paul-Antoine and Touraille, Luc and Bisgambiglia, Paul and Hill, David},
  title =	{{A survey of modelling and simulation software frameworks using Discrete Event System Specification}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{40--49},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Neykova, Rumyana and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.40},
  URN =		{urn:nbn:de:0030-drops-47721},
  doi =		{10.4230/OASIcs.ICCSW.2014.40},
  annote =	{Keywords: DEVS, Framework, Survey, Modelling, Simulation}
}

21 Search Results for "Neykova, Rumyana"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message