### Improving Safety-Critical Systems by Visual Analysis

Yi Yang, Patric Keller, Yarden Livnat & Peter Liggesmeyer
The importance analysis provides a means of analyzing the contribution of potential low-level system failures to identify and assess vulnerabilities of safety-critical systems. Common approaches attempt to enhance the system safety by addressing vulnerabilities using an iterative analysis process, while considering relevant constraints, e.g., cost, for optimizing the improvements. Typically, data regarding the analysis process is presented across several views with few interactive associations among them. Consequently, this hampers the identification of meaningful information supporting...

Andrew V. Jones

### Building and Documenting Workflows with Python-Based Snakemake

Johannes Köster & Sven Rahmann
Snakemake is a novel workflow engine with a simple Python-derived workflow definition language and an optimizing execution environment. It is the first system that supports multiple named wildcards (or variables) in input and output filenames of each rule definition. It also allows to write human-readable workflows that document themselves. We have found Snakemake especially useful for building high-throughput sequencing data analysis pipelines and present examples from this area. Snakemake exemplifies a generic way to implement...

### CFD Simulation of Liquid-Liquid Extraction Columns and Visualization of Eulerian Datasets

Mark W. Hlawitschka, Fang Chen, Hans-Jörg Bart & Bernd Hamann
In this joint work, a complete framework for modeling, simulating and visualizing multiphase fluid flow within an extraction column is presented. We first present a volume-of-fluid simulation, which is able to predict the surface of the droplets during coalescence. However, a fast and efficient model is needed for the simulation of a liquid-liquid extraction column due to the high number of occurring droplets. To simulate the velocity and droplet size in a DN32 extraction column,...

### A Bilevel Mixed Integer Linear Programming Model for Valves Location in Water Distribution Systems

Andrea Peano, Maddalena Nonato, Marco Gavanelli, Stefano Alvisi & Marco Franchini
The positioning of valves on the pipes of a Water Distribution System (WDS) is a core decision in the design of the isolation system of a WDS. When closed, valves permit to isolate a small portion of the network, so called a sector, which can be de-watered for maintenance purposes at the cost of a supply disruption. However, valves have a cost so their number is limited, and their position must be chosen carefully in...

### Safety Verification of Communicating One-Counter Machines

Alexander Heußner, Tristan Le Gall & Grégoire Sutre
In order to verify protocols that tag messages with integer values, we investigate the decidability of the reachability problem for systems of communicating one-counter machines. These systems consist of local one-counter machines that asynchronously communicate by exchanging the value of their counters via, a priori unbounded, FIFO channels. This model extends communicating finite-state machines (CFSM) by infinite-state local processes and an infinite message alphabet. The main result of the paper is a complete characterization of...

### HandSpy - a system to manage experiments on cognitive processes in writing

Carlos Monteiro & José Paulo Leal
Experiments on cognitive processes require a detailed analysis of the contribution of many participants. In the case of cognitive processes in writing these experiments require special software tools to collect gestures performed with a pen or a stylus, and recorded with special hardware. These tools produce different kinds of data files in binary and proprietary formats that need to be managed on a workstation file system for further processing with generic tools, such as spreadsheets...

### Static Analysis for Checking Data Format Compatibility of Programs

Large software systems are developed by composing multiple programs. If the programs manipulate and exchange complex data, such as network packets or files, it is essential to establish that they follow compatible data formats. Most of the complexity of data formats is associated with the headers. In this paper, we address compatibility of programs operating over headers of network packets, files, images, etc. As format specifications are rarely available, we infer the format associated with...

### Semantic Data Management (Dagstuhl Seminar 12171)

Grigoris Antoniou, Oscar Corcho, Karl Aberer, Elena Simperl & Rudi Studer
This report documents the program and the outcomes of Dagstuhl Seminar 12171 "Semantic Data Management". The purpose of the seminar was to have a fruitful exchange of ideas between the semantic web, database systems and information retrieval communities, organised across four main themes: scalability, provenance, dynamicity and search. Relevant key questions cutting across all of these themes were: (i) how can existing DB and IR solutions be adapted to manage semantic data; and (ii) are...

### Sharing Distributed Knowledge on the Web (Invited Talk)

Serge Abiteboul
To share information, we propose to see the Web as a knowledge base consisting of distributed logical facts and rules. Our objective is to help Web users finding information, as well as controlling their own, using automated reasoning over this knowledge base towards improving the quality of service and of data. For this, we introduce Webdamlog, a Datalog-style language with rule delegation. We mention the implementation of a system to support this language as well...

### A Concurrent Logical Relation

Lars Birkedal, Filip Sieczkowski & Jacob Thamsborg
We present a logical relation for showing the correctness of program transformations based on a new type-and-effect system for a concurrent extension of an ML-like language with higher-order functions, higher-order store and dynamic memory allocation. We show how to use our model to verify a number of interesting program transformations that rely on effect annotations. In particular, we prove a Parallelization Theorem, which expresses when it is sound to run two expressions in parallel instead...

### Visualization of CHR through Source-to-Source Transformation

In this paper, we propose an extension of Constraint Handling Rules (CHR) with different visualization features. One feature is to visualize the execution of rules applied on a list of constraints. The second feature is to represent some of the CHR constraints as objects and visualize the effect of CHR rules on them. To avoid changing the compiler, our implementation is based on source-to-source transformation.

### Knowledge Spaces and the Completeness of Learning Strategies

Stefano Berardi & Ugo De'Liguoro
We propose a theory of learning aimed to formalize some ideas underlying Coquand's game semantics and Krivine's realizability of classical logic. We introduce a notion of knowledge state together with a new topology, capturing finite positive and negative information that guides a learning strategy. We use a leading example to illustrate how non-constructive proofs lead to continuous and effective learning strategies over knowledge spaces, and prove that our learning semantics is sound and complete w.r.t....

### Extending the Path Analysis Technique to Obtain a Soft WCET

Paul Keim, Amanda Noyes, Andrew Ferguson, Joshua Neal & Christopher Healy
This paper discusses an efficient approach to statically compute a WCET that is "soft" rather than "hard". The goal of most timing analysis is to determine a guaranteed WCET; however this execution time may be far above the actual distribution of observed execution times. A WCET estimate that bounds the execution time 99% of the time may be more useful for a designer in a soft real-time environment. This paper discusses an approach to measure...

### AI meets Formal Software Development (Dagstuhl Seminar 12271)

Alan Bundy, Dieter Hutter, Cliff B. Jones & J Strother Moore
This report documents the program and the outcomes of Dagstuhl Seminar 12271 AI meets Formal Software Development''. This seminar brought together researchers from formal methods and AI. The participants addressed the issue of how AI can aid the formal software development process, including modelling and proof. There was a pleasing number of participants from industry and this made it possible to ground the discussions on industrial-scale problems.

### Verification of Dependable Software using SPARK and Isabelle

Stefan Berghofer
We present a link between the interactive proof assistant Isabelle/HOL and the SPARK/Ada tool suite for the verification of high-integrity software. Using this link, we can tackle verification problems that are beyond reach of the proof tools currently available for Spark. To demonstrate that our methodology is suitable for real-world applications, we show how it can be used to verify an efficient library for big numbers. This library is then used as a basis for...

### Satisfiability: where Theory meets Practice (Invited Talk)

Inês Lynce
Propositional Satisfiability (SAT) is a keystone in the history of computer science. SAT was the first problem shown to be NP-complete in 1971 by Stephen Cook. Having passed more than 40 years from then, SAT is now a lively research field where theory and practice have a natural intermixing. In this talk, we overview the use of SAT in practical domains, where SAT is thought in a broad sense, i.e. including SAT extensions such as...

### Optimal Freight Train Classification using Column Generation

Markus Bohlin, Florian Dahms, Holger Flier & Sara Gestrelius
We consider planning of freight train classification at hump yards using integer programming. The problem involves the formation of departing freight trains from arriving trains subject to scheduling and capacity constraints. To increase yard capacity, we allow the temporary storage of early freight cars on specific mixed-usage tracks. The problem has previously been modeled using a direct integer programming model, but this approach did not yield lower bounds of sufficient quality to prove optimality. In...

### Scheduling with Setup Costs and Monotone Penalties

Rohit Khandekar, Kirsten Hildrum, Deepak Rajan & Joel Wolf
We consider single processor preemptive scheduling with job-dependent setup times. In this model, a job-dependent setup time is incurred when a job is started for the first time, and each time it is restarted after preemption. This model is a common generalization of preemptive scheduling, and actually of non-preemptive scheduling as well. The objective is to minimize the sum of any general non-negative, non-decreasing cost functions of the completion times of the jobs -- this...

Stefan Ravizza & Penny Holborn

### A Quantitative Study of Social Organisation in Open Source Software Communities

Marcelo Serrano Zanetti, Emre Sarigöl, Ingo Scholtes, Claudio Juan Tessone & Frank Schweitzer
The success of open source projects crucially depends on the voluntary contributions of a sufficiently large community of users. Apart from the mere size of the community, interesting questions arise when looking at the evolution of structural features of collaborations between community members. In this article, we discuss several network analytic proxies that can be used to quantify different aspects of the social organisation in social collaboration networks. We particularly focus on measures that can...

### Reinterpreting Compression in Infinitary Rewriting

Jeroen Ketema
Departing from a computational interpretation of compression in infinitary rewriting, we view compression as a degenerate case of standardisation. The change in perspective comes about via two observations: (a) no compression property can be recovered for non-left-linear systems and (b) some standardisation procedures, as a "side-effect", yield compressed reductions.

### CHR for Social Responsibility

Veronica Dahl, Bradley Coleman, J. Emilio Miralles & Erez Maharshak
Publicly traded corporations often operate against the public's interest, serving a very limited group of stakeholders. This is counter-intuitive, since the public as a whole owns these corporations through direct investment in the stock-market, as well as indirect investment in mutual, index, and pension funds. Interestingly, the public's role in the proxy voting process, which allows shareholders to influence their company's direction and decisions, is essentially ignored by individual investors. We speculate that a prime...

### Imperative Programming in Sets with Atoms

Mikolaj Bojanczyk & Szymon Torunczyk
We define an imperative programming language, which extends while programs with a type for storing atoms or hereditarily orbit-finite sets. To deal with an orbit-finite set, the language has a loop construction, which is executed in parallel for all elements of an orbit-finite set. We show examples of programs in this language, e.g. a program for minimising deterministic orbit-finite automata.

### Controlling In-Vehicle Systems with a Commercial EEG Headset: Performance and Cognitive Load

Daniel Cernea, Peter-Scott Olech, Achim Ebert & Andreas Kerren
Humans have dreamed for centuries to control their surroundings solely by the power of their minds. These aspirations have been captured by multiple science fiction creations, such as the Neuromancer novel by William Gibson or the Brainstorm cinematic movie, to name just a few. Nowadays, these dreams are slowly becoming reality due to a variety of brain-computer interfaces (BCI) that detect neural activation patterns and support the control of devices by brain signals. An important...

• 2012
447

• Text
447