![Loading...](https://link.springer.com/static/c4a417b97a76cc2980e3c25e2271af3129e08bbe/images/pdf-preview/spacer.gif)
-
Chapter and Conference Paper
A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees
In this paper, we propose a novel algorithm to learn a Büchi automaton from a teacher who knows an \(\omega \) -regula...
-
Chapter and Conference Paper
CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation
CPArec is a tool for verifying recursive C programs via source-to-source program transformation. It uses a recursion-free program analyzer CPAChecker as a black box and computes function summar...
-
Chapter and Conference Paper
Commutativity of Reducers
In the Map-Reduce programming model for data parallel computation, a reducer computes an output from a list of input values associated with a key. The inputs however may not arrive at a reducer in a fixed orde...
-
Chapter and Conference Paper
BULL: A Library for Learning Algorithms of Boolean Functions
We present the tool BULL (Boolean fUnction Learning Library), the first publicly available implementation of learning algorithms for Boolean functions. The tool is implemented in C with interfaces to C++, JAVA...
-
Chapter and Conference Paper
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO
We introduce Memorax, a tool for the verification of control state reachability (i.e., safety properties) of concurrent programs manipulating finite range and integer variables and running on top of weak memory m...
-
Chapter and Conference Paper
Counter-Example Guided Fence Insertion under TSO
We give a sound and complete fence insertion procedure for concurrent finite-state programs running under the classical TSO memory model. This model allows “write to read” relaxation corresponding to the addition...
-
Chapter and Conference Paper
Learning Boolean Functions Incrementally
Classical learning algorithms for Boolean functions assume that unknown targets are Boolean functions over fixed variables. The assumption precludes scenarios where indefinitely many variables are needed. It a...
-
Chapter and Conference Paper
Automated Assume-Guarantee Reasoning through Implicit Learning
We propose a purely implicit solution to the contextual assumption generation problem in assume-guarantee reasoning. Instead of improving the L * algorithm — a learning algorithm for finite automa...
-
Chapter and Conference Paper
When Simulation Meets Antichains
We describe a new and more efficient algorithm for checking universality and language inclusion on nondeterministic finite word automata (NFA) and tree automata (TA). To the best of our knowledge, the antichai...
-
Chapter and Conference Paper
Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing
There are two main classes of methods for checking universality and language inclusion of Büchi-automata: Rank-based methods and Ramsey-based methods. While rank-based methods have a better worst-case complexi...
-
Chapter and Conference Paper
HAVE: Detecting Atomicity Violations via Integrated Dynamic and Static Analysis
The reality of multi-core hardware has made concurrent programs pervasive. Unfortunately, writing correct concurrent programs is difficult. Atomicity violation, which is caused by concurrently executing code u...
-
Chapter and Conference Paper
Learning Minimal Separating DFA’s for Compositional Verification
Algorithms for learning a minimal separating DFA of two disjoint regular languages have been proposed and adapted for different applications. One of the most important applications is learning minimal contextu...
-
Chapter and Conference Paper
GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
This paper reports extensions to the GOAL tool that enable it to become a research tool for omega automata and temporal logic. The extensions include an expanded collection of translation, simplification, and ...
-
Chapter and Conference Paper
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
Recent studies have suggested the applicability of learning to automated compositional verification. However, current learning algorithms fall short when it comes to learning liveness properties. We extend the au...
-
Chapter and Conference Paper
In-Vehicle Information System Used in Complex and Low Traffic Situations: Impact on Driving Performance and Attitude
This paper describes a study where drivers’ responses to an in-vehicle information system were tested in high and low density traffic. There were 17 participants in a study that was run using a driving simulat...
-
Chapter and Conference Paper
A Real-Time Gesture Tracking and Recognition System Based on Particle Filtering and Ada-Boosting Techniques
A real-time gesture tracking and recognition system based on particle filtering and Ada-Boosting techniques is presented in this paper. The particle filter, which is a flexible simulation-based method and suit...
-
Chapter and Conference Paper
Using Personas and Scenarios as an Interface Design Tool for Advanced Driver Assistance Systems
When looking at the traditional way of conducting human factors research within the active safety area, focus often tends to be on drivers’ cognitive capacities like; situation awareness, workload and behaviou...
-
Chapter and Conference Paper
An Improved Genetic Algorithm for Web Services Selection
An improved genetic algorithm is presented to select optimal web services composite plans from a lot of composite plans on the basis of global Quality-of-Service (QoS) constraints. The relation matrix coding s...
-
Chapter and Conference Paper
Listen! There Are Other Road Users Close to You – Improve the Traffic Awareness of Truck Drivers
As the amount of good transportation on road is increasing the accidents involving heavy trucks and other road users are also increasing. To make the truck driver aware of other road users close to the truck i...
-
Chapter and Conference Paper
Investigating the Use and Adoption of Self-service Technology in China
Self-service technology use and adoption can be seen as an evolutionary process. From a conceptual perspective, evolution delivers the growing advantages of self-service. From a practical perspective, evolutio...