Publications IIF of last two years

Goto list of all publications.

Years: 2017 | 2016

2017

back to the year overview

Fabian Kuhn, Philipp Schneider
Broadcasting in an Unreliable SINR Model
2017 21st Conference on Principles of Distributed Systems (OPODIS) , pages: 3:1 - 3:21
Jan Horáček, Jan Burchard, Bernd Becker, Martin Kreuzer
Integrating Algebraic and SAT Solvers
2017 International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS) 2017
Jan Horáček, Maël Gay, Bernd Becker, Martin Kreuzer
Integrating Algebraic and SAT Solvers
2017 International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS) 2017
Bast H, Buchhold B
QLever: A Query Engine for Eff€icient SPARQL+Text Search
2017 CIKM
» show abstract« hide abstract
AbstractWe present QLever, a query engine for efficient combined search on a knowledge base and a text corpus, in which named entities from the knowledge base have been identi€ed (that is, recognized and disambiguated). The query language is SPARQL extended by two QLever-speci€fic predicates ql:contains-entity and ql:contains-word, which can express the occurrence of an entity or word (the object of the predicate) in a text record (the subject of the predicate). We evaluate QLever on two large datasets, including FACC (the ClueWeb12 corpus linked to Freebase). We compare against three state-of-the-art query engines for knowledge bases with varying support for text search: RDF-3X, Virtuoso, Broccoli. Query times are competitive and often faster on the pure SPARQL queries, and several orders of magnitude faster on the SPARQL+Text queries. Index size is larger for pure SPARQL queries, but smaller for SPARQL+Text queries.
Mohsen Ghaffari, Juho Hirvonen, Fabian Kuhn, Yannic Maus, Jukka Suomela, Jara Uitto
Improved Distributed Degree Splitting and Edge Coloring
2017 International Symposium on DIStributed Computing (DISC)
» show abstract« hide abstract
AbstractThe degree splitting problem requires coloring the edges of a graph red or blue such that each node has almost the same number of edges in each color, up to a small additive discrepancy. The directed variant of the problem requires orienting the edges such that each node has almost the same number of incoming and outgoing edges, again up to a small additive discrepancy. We present deterministic distributed algorithms for both variants, which improve on their counterparts presented by Ghaffari and Su [SODA'17]: our algorithms are significantly simpler and faster, and have a much smaller discrepancy. This also leads to a faster and simpler deterministic algorithm for $(2+o(1))\Delta$-edge-coloring, improving on that of Ghaffari and Su.
Magnús M. Halldórsson, Fabian Kuhn, Nancy Lynch, Calvin Newport
An Efficient Communication Abstraction for Dense Wireless Networks
2017 31st Symposium on Distributed Computing (DISC) , pages: 25:1 - 25:16
Abdolhamid Ghodselahi, Fabian Kuhn
Dynamic Analysis of the Arrow Distributed Directory Protocol in General Networks
2017 31st Symposium on Distributed Computing (DISC)
» show abstract« hide abstract
AbstractThe Arrow protocol is a simple and elegant protocol to coordinate exclusive access to a shared object in a network. The protocol solves the underlying distributed queueing problem by using path reversal on a pre-computed spanning tree (or any other tree topology simulated on top of the given network). It is known that the Arrow protocol solves the problem with a competitive ratio of O(log D) on trees of diameter D. This implies a distributed queueing algorithm with competitive ratio O(s · log D) for general networks with a spanning tree of diameter D and stretch s. In this work we show that when running the Arrow protocol on top of the well-known probabilistic tree embedding of Fakcharoenphol, Rao, and Talwar [STOC03], we obtain a randomized distributed queueing algorithm with a competitive ratio of O(log n) even on general network topologies. The result holds even if the queueing requests occur in an arbitrarily dynamic and concurrent fashion and even if communication is asynchronous. From a technical point of view, the main of the paper shows that the competitive ratio of the Arrow protocol is constant on a special family of tree topologies, known as hierarchically well separated trees.
Manuela Fischer, Mohsen Ghaffari, Fabian Kuhn
Deterministic Distributed Edge-Coloring via Hypergraph Maximal Matching
2017 58th IEEE Symposium on Foundations of Computer Science (FOCS) , pages: 180 - 191
Daniel Bahrdt, Rick Gelhausen, Stefan Funke, Sabine Storandt
Searching OSM Planet with Context-Aware Spatial Relations
2017 ACM SIGSPATIAL Sigspatial, volume: 1
» show abstract« hide abstract
AbstractWe consider the problem of indexing the complete OpenStreetMap planet data set (> 500GB of raw data) to support complex queries involving both text search as well as context-aware spatial relations. This requires (a) formalization of spatial relations like ’north of’, ’between’, ’near’ depending on the context, and (b) the development of suitable data representations to integrate textual and spatial information for efficient query performance.
Bast H, Brosi P, Storandt S
Efficient Generation of Geographically Accurate Transit Maps
2017
» show abstract« hide abstract
AbstractWe present LOOM (Line-Ordering Optimized Maps), a fully automatic generator of geographically accurate transit maps. The input to LOOM is data about the lines of a given transit network, namely for each line, the sequence of stations it serves and the geographical course the vehicles of this line take. We parse this data from GTFS, the prevailing standard for public transit data. LOOM proceeds in three stages: (1) construct a so-called line graph, where edges correspond to segments of the network with the same set of lines following the same course; (2) construct an ILP that yields a line ordering for each edge which minimizes the total number of line crossings and line separations; (3) based on the line graph and the ILP solution, draw the map. As a naive ILP formulation is too demanding, we derive a new custom-tailored formulation which requires significantly fewer constraints. Furthermore, we present engineering techniques which use structural properties of the line graph to further reduce the ILP size. For the subway network of New York, we can reduce the number of constraints from 229,000 in the naive ILP formulation to about 4,500 with our techniques, enabling solution times of less than a second. Since our maps respect the geography of the transit network, they can be used for tiles and overlays in typical map services. Previous research work either did not take the geographical course of the lines into account, or was concerned with schematic maps without optimizing line crossings or line separations.
Isabel Dahlhausen, Tobias Schubert
Von der Teilnehmendenanalyse zur lernförderlichen Gestaltung: Wie können wir E-Learning lebendiger machen?
2017 16. Internationale ILIAS-Konferenz
Jan Burchard, Maël Gay, Ange-Salomé Messeng Ekossono, Jan Horáček, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia Polian
AutoFault: Towards Automatic Construction of Algebraic Fault Attacks
2017 Fault Diagnosis and Tolerance in Cryptography (FDTC) 2017
» show abstract« hide abstract
AbstractA prototype of the framework AutoFault, which automatically constructs fault-injection attacks for hardware realizations of ciphers, is presented. AutoFault can be used to quickly evaluate the resistance of security-critical hardware blocks to fault attacks and the adequacy of implemented countermeasures. The framework takes as inputs solely the circuit description of the cipher and the fault(s) and produces an algebraic formula that can be handed over to an external solver. In contrast to previous work, attacks constructed by AutoFault do not incorporate any cipher-specific cryptoanalytic derivations, making the framework accessible to users without cryptographic background. We report successful application of AutoFault in combination with a state-of-the-art SAT solver to LED-64 and to small-scale AES. To the best of our knowledge, this is the first time that a state-of-the-art cipher (LED-64) was broken by a fault attack with no prior manual cryptanalysis whatsoever.
Seth Gilbert, Fabian Kuhn, Chaodong Zheng
Communication Primitives in Cognitive Radio Networks
2017 36th ACM Symposium on Principles of Distributed Computing (PODC) , pages: 23 - 32
Mohsen Ghaffari, Fabian Kuhn, Hsin-Hao Su
Distributed MST and Routing in Almost Mixing Time
2017 36th ACM Symposium on Principles of Distributed Computing (PODC) , pages: 131 - 140
Karl Bringmann, Ralph Keusch, Johannes Lengler, Yannic Maus, Anisur Rahaman Molla
Greedy Routing and the Algorithmic Small-World Phenomenon
2017 36th ACM Symposium on Principles of Distributed Computing (PODC)
» show abstract« hide abstract
AbstractThe algorithmic small-world phenomenon, empirically established by Milgram's letter forwarding experiments from the 60s~\cite{milgram1967small}, was theoretically explained by Kleinberg in 2000~\cite{KleinbergModel}. However, from today's perspective his model has several severe shortcomings %drawbacks that limit the applicability to real-world networks. In order to give a more convincing explanation of the algorithmic small-world phenomenon, we study decentralized greedy routing in a more flexible random graph model (geometric inhomogeneous random graphs) which overcomes all previous shortcomings. %has not only theoretically good properties, Apart from exhibiting good properties in theory, it has also been extensively experimentally validated that this model reasonably captures real-world networks. In this model, the greedy routing protocol is purely distributed as each vertex only needs to know information about its direct neighbors. We prove that it succeeds with constant probability, and in case of success almost surely finds an almost shortest path of length $\Theta(\log\log n)$, where our bound is tight including the leading constant. Moreover, we study natural local patching methods which augment greedy routing by backtracking and which do not require any global knowledge. We show that such methods can ensure success probability 1 in an asymptotically tight number of steps. These results also address the question of Krioukov et al.~\cite{krioukov2007compact} whether there are efficient local routing protocols for the internet graph. There were promising experimental studies, but the question remained unsolved theoretically. Our results give for the first time a rigorous and analytical affirmative answer.
Sebastian Brandt, Yuval Emek, Jara Uitto, Roger Wattenhofer
A Tight Lower Bound for the Capture Time of the Cops and Robbers Game
2017 44th International Colloquium on Automata, Languages, and Programming (ICALP)
» show abstract« hide abstract
AbstractFor the game of Cops and Robbers, it is known that in 1-cop-win graphs, the cop can capture the robber in O(n) time, and that there exist graphs in which this capture time is tight. When k >= 2, a simple counting argument shows that in k-cop-win graphs, the capture time is at most O(n^{k + 1}), however, no non-trivial lower bounds were previously known; indeed, in their 2011 book, Bonato and Nowakowski ask whether this upper bound can be improved. In this paper, the question of Bonato and Nowakowski is answered on the negative, proving that the O(n^{k + 1}) bound is asymptotically tight for any constant k >= 2. This yields a surprising gap in the capture time complexities between the 1-cop and the 2-cop cases.
Bast H, Korzen C
A Benchmark and Evaluation for Text Extraction from PDF
2017
» show abstract« hide abstract
AbstractExtracting the body text from a PDF document is an important but surprisingly difficult task. The reason is that PDF is a layout-based format which specifies the fonts and positions of the individual characters rather than the semantic units of the text (e.g., words or paragraphs) and their role in the document (e.g., body text or caption). There is an abundance of extraction tools, but their quality and the range of their functionality are hard to determine. In this paper, we show how to construct a high-quality benchmark of principally arbitrary size from parallel TeX and PDF data. We construct such a benchmark of 12,098 scientific articles from arXiv.org and make it publicly available. We establish a set of criteria for a clean and independent assessment of the semantic abilities of a given extraction tool. We provide an extensive evaluation of 14 state-of-the-art tools for text extraction from PDF on our benchmark according to our criteria. We include our own method, Icecite, which significantly outperforms all other tools, but is still not perfect. We outline the remaining steps necessary to finally make text extraction from PDF a "solved problem".
Mohsen Ghaffari, Fabian Kuhn, Yannic Maus
On the Complexity of Local Distributed Graph Problems
2017 ACM Symposium on Theory of Computing (STOC)
» show abstract« hide abstract
AbstractThis paper is centered on the complexity of graph problems in the well-studied LOCAL model of distributed computing, introduced by Linial [FOCS '87]. It is widely known that for many of the classic distributed graph problems (including maximal independent set (MIS) and (Δ+1)-vertex coloring), the randomized complexity is at most polylogarithmic in the size n of the network, while the best deterministic complexity is typically 2^(O(log(sqrt(n))). Understanding and narrowing down this exponential gap is considered to be one of the central long-standing open questions in the area of distributed graph algorithms. We investigate the problem by introducing a complexity-theoretic framework that allows us to shed some light on the role of randomness in the LOCAL model. We define the SLOCAL model as a sequential version of the LOCAL model. Our framework allows us to prove completeness results with respect to the class of problems which can be solved efficiently in the SLOCAL model, implying that if any of the complete problems can be solved deterministically in log^(O(1))n rounds in the LOCAL model, we can deterministically solve all efficient SLOCAL-problems (including MIS and (Δ+1)-coloring) in log^(O(1))n rounds in the LOCAL model. We show that a rather rudimentary looking graph coloring problem is complete in the above sense: Color the nodes of a graph with colors red and blue such that each node of sufficiently large polylogarithmic degree has at least one neighbor of each color. The problem admits a trivial zero-round randomized solution. The result can be viewed as showing that the only obstacle to getting efficient determinstic algorithms in the LOCAL model is an efficient algorithm to approximately round fractional values into integer values.
Michael A. Kochte, Matthias Sauer, Laura Rodríguez Gómez, Pascal Raiola, Bernd Becker, Hans-Joachim Wunderlich
Specification and verification of security in reconfigurable scan networks
2017 IEEE European Test Symposium
Jan Burchard, Dominik Erb, Sudhakar M. Reddy, Adit D. Singh, Bernd Becker
Efficient SAT-Based Generation of Hazard-Activated TSO Tests
2017 IEEE VLSI Test Symposium (VTS'17)
Bast H, Buchhold B, Haussmann E, Heindorf S, Potthast M
WDSM Cup 2017: Vandalism Detection and Triple Scoring
2017
» show abstract« hide abstract
AbstractThe WSDM Cup 2017 was a data mining challenge held in conjunction with the 10th International Conference on Web Search and Data Mining (WSDM). It addressed key challenges of knowledge bases today: quality assurance and entity search. For quality assurance, we tackle the task of vandalism detection, based on a dataset of more than 82 million user-contributed revisions of the Wikidata knowledge base, all of which annotated with regard to whether or not they are vandalism. For entity search, we tackle the task of triple scoring, using a dataset that comprises relevance scores for triples from type-like relations including occupation and country of citizenship, based on about 10,000 human relevance judgments. For reproducibility sake, participants were asked to submit their soft-ware on TIRA, a cloud-based evaluation platform, and they were incentivized to share their approaches open source.
Uwe Wagschal, Bernd Becker, Thomas Metz, Thomas Waldvogel, Linus Feiten
Real-time evaluation of political debates at home and abroad with the Debat-O-Meter
2017 Berlin 19th General Online Research Conference (GOR)
» show abstract« hide abstract
AbstractDue to their role in election campaigns, televised debates between political candidates (“TV-Duelle”) have attracted substantial scholarly attention. A large body of work has used physical feedback devices to measure viewers’ reactions to a debate in real-time. However, this approach is limited to lab-based settings with potential negative ramifications for e.g. external validity. Therefore, a method freeing researchers from the need to use physical devices is called for.
Jan Burchard, Felix Neubauer, Pascal Raiola, Dominik Erb, Bernd Becker
Evaluating the Effectiveness of D-Chains in SAT based ATPG
2017 IEEE Latin American Test Symposium (LATS'17)
Matthias Sauer, Pascal Raiola, Linus Feiten, Bernd Becker, Ulrich Rührmair, Ilia Polian
Sensitized Path PUF: A Lightweight Embedded Physical Unclonable Function
2017 Conf. on Design, Automation and Test in Europe
T. Pasternak,, T. Haser,, Thorsten Falk,, Olaf Ronneberger,, K. Palme,, L. Otten
A 3D digital atlas of the Nicotiana tabacum root tip and its use to investigate changes in the root apical meristem induced by the Agrobacterium 6b oncogene
2017 Plant J, volume: 92, issue: 1, pages: 31 - 42
Bast H, Buchhold B, Haussmann E
A Quality Evaluation of Combined Search on a Knowledge Base and Text
2017 Künstliche Intelligenz
» show abstract« hide abstract
AbstractWe provide a quality evaluation of KB+Text search, a deep integration of knowledge base search and standard full-text search. A knowledge base (KB) is a set of subject-predicate-object triples with a common naming scheme. The standard query language is SPARQL, where queries are essentially lists of triples with variables. KB+Text search extends this by a special "occurs-with" predicate, which can be used to express the co-occurrence of words in the text with mentions of entities from the knowledge base. Both pure KB search and standard full-text search are included as special cases. We evaluate the result quality of KB+Text search on three different query sets. The corpus is the full version of the English Wikipedia (2.4 billion word occurrences) combined with the YAGO knowledge base (26 million triples). We provide a web application to reproduce our evaluation, which is accessible via http://ad.informatik.uni-freiburg.de/publications.
Wagner M, Lindauer M, Misir M, Nallaperuma S, Hutter F
A case study of algorithm selection for the traveling thief problem
2017 Journal of Heuristics, pages: 1 - 26
T. Leng Tay,, Dominic Mai,, J. Dautzenberg,, F. Fernández-Klett,, G. Lin, S. ,, M. Datta,, A. Drougard,, T. Stempfl,, A. Ardura-Fabregat,, O. Staszewski,, A. Margineanu,, A. Sporbert,, L. M Steinmetz,, J. Andrew Pospisilik,, S. Jung,, J. Priller,, D. Grün,, Olaf Ronneberger,, M. Prinz
A new fate mapping system reveals context-dependent random or clonal expansion of microglia
2017 Nat Neurosci

Download file
Felix Neubauer, Karsten Scheibler, Bernd Becker, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer
Accurate Dead Code Detection in Embedded C Code by Arithmetic Constraint Solving
2017 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
» show abstract« hide abstract
AbstractUnreachable code fragments in software, despite not having a negative impact on the functional behavior, can have a bad effect in other areas, such as code optimization or coverage-based code validation and certification. Especially the latter is important in industrial, safety critical environments, where detecting such dead code is a major goal to adjust the coverage of software tests. In the context of embedded systems we focus on C programs which are reactive, control-oriented, and floating-point dominated. Such programs are either automatically generated from Simulink-plus-Stateflow models or hand-written according to coding guidelines. While there are various techniques – e.g. abstract interpretation or Counterexample guided abstraction refinement (CEGAR) – to deal with individual issues of this domain, there is none which can cover all of them. The AVACS transfer project T1 aims at the combination of these techniques in order to provide an accurate and efficient dead code detection. In this paper we present the ideas and goals of the project as well as the current status (including very promising experimental results) and future challenges.
Pascal Raiola, Dominik Erb, Sudhakar Reddy, Bernd Becker
Accurate Diagnosis of Interconnect Open Defects based on the Robust Enhanced Aggressor Victim Model
2017 30th International Conference on VLSI Design
» show abstract« hide abstract
AbstractInterconnect opens are known to be one of the predominant defects in nanoscale technologies. Automatic test pattern generation for open faults is challenging, because of their rather unstable behavior and the numerous electrical parameters which need to be considered. Thus, most approaches try to avoid accurate modeling of all constraints like the influence of the aggressors on the open net and use simplified fault models in order to detect as many faults as possible or make assumptions which decrease both complexity and accuracy. Yet, this leads to the problem that not only generated tests may be invalidated but also the localization of a specific fault may fail -- in case such a model is used as basis for diagnosis. Furthermore, most of the models do not consider the problem of oscillating behavior, caused by feedback introduced by coupling capacitances, which occurs in almost all designs. The Robust Enhanced Aggressor Victim Model (REAV) does not only consider the influence of all aggressors accurately but also guarantees robustness against oscillating behavior as well as process variations affecting the thresholds of gates driven by an open interconnect. In this work we present the first diagnostic classification algorithm for this model. This algorithm considers all constraints enforced by the REAV model accurately - and hence handles unknown values as well as oscillating behavior. In addition, it allows to distinguish faults at the same interconnect and thus reducing the area that has to be considered for physical failure analysis. Experimental results show the high efficiency of the new method handling circuits with up to 500,000 non-equivalent faults and considerably increasing the diagnostic resolution.
Schindelhauer C, Wang Z, Zhang L, Wang X, Huang D
Acoustic NLOS Identification Using Acoustic Channel Characteristics for Smartphone Indoor Localization
2017 J Sensors, issue: 17, supplement: 4, pages: 727 - 727
Kundu Kousik, Backofen Rolf
An Efficient Semi-supervised Learning Approach to Predict SH2 Domain Mediated Interactions
2017 Methods Mol Biol, volume: 1555, pages: 83 - 97
» show abstract« hide abstract
AbstractSrc homology 2 (SH2) domain is an important subclass of modular protein domains that plays an indispensable role in several biological processes in eukaryotes. SH2 domains specifically bind to the phosphotyrosine residue of their binding peptides to facilitate various molecular functions. For determining the subtle binding specificities of SH2 domains, it is very important to understand the intriguing mechanisms by which these domains recognize their target peptides in a complex cellular environment. There are several attempts have been made to predict SH2-peptide interactions using high-throughput data. However, these high-throughput data are often affected by a low signal to noise ratio. Furthermore, the prediction methods have several additional shortcomings, such as linearity problem, high computational complexity, etc. Thus, computational identification of SH2-peptide interactions using high-throughput data remains challenging. Here, we propose a machine learning approach based on an efficient semi-supervised learning technique for the prediction of 51 SH2 domain mediated interactions in the human proteome. In our study, we have successfully employed several strategies to tackle the major problems in computational identification of SH2-peptide interactions.
van Rijn J, Hutter F
An Empirical Study of Hyperparameter Importance Across Datasets
2017 Proceedings of the International Workshop on Automatic Selection, Configuration and Composition of Machine Learning Algorithms (AutoML 2017), volume: 1998, pages: 97 - 104
Andreas Kuhner, Tobias Schubert, Christoph Maurer, Wolfram Burgard
An Online System for Tracking the Performance of Parkinson's Patients
2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, Vancouver 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, Vancouver 2017
» show abstract« hide abstract
AbstractAn objective performance measure for movement tasks is widely regarded as having utmost relevance for the therapy of movement disorders. Existing systems typically rely on human experts, which is known to produce substantial inter- and intra-rater variability. Present solutions are either based on simple features or invasive motion capture techniques. They typically work on a specific motion task only and fail to generalize to other tasks. In addition, they often require manual offline pre- and post-processing. In this paper we present a novel approach to compute a continuous and objective performance measure online during a patient session, without tedious and time-consuming pre- or post-processing steps. Our approach is able to generalize between different motion capture devices and different motion tasks. It runs on live motion data extracted with a non-invasive marker-less off-the-shelf visionbased tracking system as well as on data extracted from an inertial measurement unit suit. In the experiments we show that our approach is competitive with an offline approach as well as with the Unified Parkinson’s Disease Rating Scale. Our approach is robust with respect to motion execution speed and it outperforms the offline approach regarding movement task generalization. We show promising results to track the current state of a Parkinson’s subject online during a therapy session.
V. Ulman,, M. Maška,, K. Magnusson,, Olaf Ronneberger,, C. Haubold,, N. Harder,, P. Matula,, P. Matula,, D. Svoboda,, M. Radojevic,, I. Smal,, K. Rohr,, J. Jaldén,, H. Blau,, O. Dzyubachyk,, B. Lelieveldt,, P. Xiao,, Y. Li,, S. Cho,, A. Dufour,, J. Olivo-Marin,, C. Reyes-Aldasoro,, J. Solis-Lemus,, Robert Bensch,, Thomas Brox,, J. Stegmaier,, R. Mikut,, S. Wolf,, F. Hamprecht,, T. Esteves,, P. Quelhas,, Ö. Demirel,, L. Malmström,, F. Jug,, P. Tomancák,, E. Meijering,, A. Muñoz-Barrutia,, M. Kozubek,, C. Ortiz-de-Solor
An objective comparison of cell-tracking algorithms
2017 Nat Methods, volume: 14, pages: 1141 - 1152

Download file
A. Habich,, S. Kloeppel,, Ahmed Abdulkadir,, E. Scheller,, C. Nissen,, J. Peter
Anodal tDCS Enhances Verbal Episodic Memory in Initially Low Performers
2017 Front Hum Neurosci, volume: 11, issue: 542, page: 542

Download file
Universität Freiburg / FreiDok
Applying CDCL to Verification and Test: When Laziness Pays Off
Karsten Scheibler
» show abstract« hide abstract
AbstractThe daily life is more and more interwoven with computerized systems. Besides the obvious ones like notebooks or smartphones, the majority of them is not directly visible -- e.g. embedded systems which control trains, cars, planes, atomic power plants or cardiac pacemakers. Although not directly visible, the correct behaviour of these systems is of utmost importance -- in particular in safety critical environments like the upcoming autonomous cars. Therefore, verifying and testing the involved hardware and software is an absolute requirement. During the design of a system, verification allows to check whether a set of desired properties is fulfilled -- making it possible to detect errors as early as possible. Besides safety requirements, the possible costs of undetected design errors are another main reason to use verification -- in particular when developing hardware components such as integrated circuits. The Pentium FDIV bug is one famous example. With certain parameters, the floating-point division instruction (FDIV) executed on early Intel Pentium processors returned wrong results. Finally, Intel offered all customers to replace these chips -- which caused costs of 475 million USD. However, having an error free design does not guarantee that a manufactured integrated circuit works correctly -- additionally, it has to be assured that the circuit is free of physical defects. This requires tests which are applied after the production of a circuit in order to check whether the circuit works as expected. Similar to hardware, software has to be verified and tested as well. Although it is easier to patch software after its delivery to a customer, the cost argument applies here too, i.e. it is always cheaper to detect errors early than late. Furthermore, software in safety critical environments has to meet certain standards (e.g. ISO 26262) which require, among other criteria, that a high percentage of the code is covered by tests. Thus, unreachable code (also called dead-code) has a negative impact on the test coverage. Fortunately, verification techniques are able to detect such dead-code and hence allow to adjust the test coverage of the remaining reachable code. Verifying that a desired property holds as well as generating a set of tests to be applied to an integrated circuit can be mapped to a formula or sequence of formulas containing Boolean, integer, floating-point or real-valued variables. Thus, proving the existence or absence of a solution for such formulas is a very important task -- which is addressed by this thesis. At the same time, this work also considers the origins of the formulas to be solved in order to tailor and optimize the approaches to their respective domains. When condensing this thesis into three keywords then CDCL, lazy and iSAT3 are the most important ones. The term CDCL is the abbreviation for conflict-driven clause learning and is the current state-of-the-art algorithm when searching for solutions for a given Boolean formula. For the moment the most important aspect is that CDCL does its job by operating on a set of so-called clauses. While some of the aforementioned problems can be expressed with a small set of these clauses which fits into the memory of currently available computers, other problems do not allow such an encoding. This is the point at which the term lazy comes into play. Instead of trying to generate all clauses in advance, some form of clever laziness is applied and the creation of a clause is deferred until it is really needed. This allows to tackle more complex problems which could not be solved before. In particular the solver iSAT3 relies on this technique for solving formulas with Boolean, integer, floating-point and real-valued variables. This solver is the basis of all contributions presented in this thesis.
Lindauer M, Hoos H, Hutter F, Schaub T
AutoFolio: An Automatically Configured Algorithm Selector (Extended Abstract)
2017 Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI’17)
Lindauer M, Hoos H, Leyton-Brown K, Schaub T
Automatic Construction of Parallel Portfolios via Algorithm Configuration
2017 Artificial Intelligence Journal (AIJ), volume: 244, pages: 272 - 290
Mohammadreza Zolfaghari,, Gabriel Leivas Oliveira,, Nima Sedaghat,, Thomas Brox
Chained Multi-stream Networks Exploiting Pose, Motion, and Appearance for Action Classification and Detection
2017

Download file
Hübner David, Tangermann Michael
Challenging the assumption that auditory event-related potentials are independent and identically distributed
2017 Proceedings of the 7th International Brain-Computer Interface Meeting 2017: From Vision to Reality, Verlag der Technischen Universität Graz, pages: 192 - 197
Castano-Candamil Sebastian, Mottaghi Soheil, Coenen Volker, Hofmann Ulrich, Tangermann Michael
Closed-Loop Deep Brain Stimulation System for an Animal Model of Parkinson’s Disease: A Pilot Study
2017 Proceedings of the 7th Graz Brain-Computer Interface Conference (GBCIC 2017), Verlag der Technischen Universität Graz, pages: 58 - 63
Davis Jason, Saunders Sita, Mann Martin, Backofen Rolf
Combinatorial ensemble miRNA target prediction of co-regulation networks with non-prediction data
2017 Nucleic Acids Res, volume: 45, issue: 15, pages: 8745 - 8757
» show abstract« hide abstract
AbstractMicroRNAs (miRNAs) are key regulators of cell-fate decisions in development and disease with a vast array of target interactions that can be investigated using computational approaches. For this study, we developed metaMIR, a combinatorial approach to identify miRNAs that co-regulate identified subsets of genes from a user-supplied list. We based metaMIR predictions on an improved dataset of human miRNA-target interactions, compiled using a machine-learning-based meta-analysis of established algorithms. Simultaneously, the inverse dataset of negative interactions not likely to occur was extracted to increase classifier performance, as measured using an expansive set of experimentally validated interactions from a variety of sources. In a second differential mode, candidate miRNAs are predicted by indicating genes to be targeted and others to be avoided to potentially increase specificity of results. As an example, we investigate the neural crest, a transient structure in vertebrate development where miRNAs play a pivotal role. Patterns of metaMIR-predicted miRNA regulation alone partially recapitulated functional relationships among genes, and separate differential analysis revealed miRNA candidates that would downregulate components implicated in cancer progression while not targeting tumour suppressors. Such an approach could aid in therapeutic application of miRNAs to reduce unintended effects. The utility is available at http://rna.informatik.uni-freiburg.de/metaMIR/.
Falkner S, Klein A, Hutter F
Combining Hyperband and Bayesian Optimization
2017 NIPS 2017 Bayesian Optimization Workshop
Wolling F, Scholl P, Reindl L, Van Laerhoven K
Combining capacitive coupling with conductive clothes: Towards resource-efficient wearable communication
2017 Proceedings - International Symposium on Wearable Computers, ISWC, volume: Part F1305
» show abstract« hide abstract
Abstract© Copyright 2017 Association for Computing Machinery. Traditional intra-body communication approaches mostly rely on either fixed cable joints embedded in clothing, or on wireless radio transmission that tends to reach beyond the body. Situated between these approaches is body-coupled communication, a promising yet less-explored method that transmits information across the user’s skin. We propose a novel body-coupled communication approach that simplifies the physical layer of data transmission via capacitive coupling between wearable systems with conductive fabrics: This layer provides a stable reference potential for the feedback path in proximity to the attached wearables on the human body, to cancel the erratic dependency on the environmental ground, and to increase the communications’ reliability. Evaluation of our prototype shows significant increases in signal quality, due to reduced attenuation and noise. Requirements on hardware and, subsequently, energy consumption, cost, and implementation effort are reduced as well.
Wolling F, Scholl P, Reindl L, Van Laerhoven K
Combining capacitive coupling with conductive clothes: Towards resource-efficient wearable communication
2017 Proceedings - International Symposium on Wearable Computers, ISWC, volume: Part F1305
» show abstract« hide abstract
Abstract© Copyright 2017 Association for Computing Machinery. Traditional intra-body communication approaches mostly rely on either fixed cable joints embedded in clothing, or on wireless radio transmission that tends to reach beyond the body. Situated between these approaches is body-coupled communication, a promising yet less-explored method that transmits information across the user’s skin. We propose a novel body-coupled communication approach that simplifies the physical layer of data transmission via capacitive coupling between wearable systems with conductive fabrics: This layer provides a stable reference potential for the feedback path in proximity to the attached wearables on the human body, to cancel the erratic dependency on the environmental ground, and to increase the communications’ reliability. Evaluation of our prototype shows significant increases in signal quality, due to reduced attenuation and noise. Requirements on hardware and, subsequently, energy consumption, cost, and implementation effort are reduced as well.
Uhl Michael, Houwaart Torsten, Corrado Gianluca, Wright Patrick, Backofen Rolf
Computational analysis of CLIP-seq data
2017 Methods, volume: 118-119, pages: 60 - 72
» show abstract« hide abstract
AbstractCLIP-seq experiments are currently the most important means for determining the binding sites of RNA binding proteins on a genome-wide level. The computational analysis can be divided into three steps. In the first pre-processing stage, raw reads have to be trimmed and mapped to the genome. This step has to be specifically adapted for each CLIP-seq protocol. The next step is peak calling, which is required to remove unspecific signals and to determine bona fide protein binding sites on target RNAs. Here, both protocol-specific approaches as well as generic peak callers are available. Despite some peak callers being more widely used, each peak caller has its specific assets and drawbacks, and it might be advantageous to compare the results of several methods. Although peak calling is often the final step in many CLIP-seq publications, an important follow-up task is the determination of binding models from CLIP-seq data. This is central because CLIP-seq experiments are highly dependent on the transcriptional state of the cell in which the experiment was performed. Thus, relying solely on binding sites determined by CLIP-seq from different cells or conditions can lead to a high false negative rate. This shortcoming can, however, be circumvented by applying models that predict additional putative binding sites.
Andreas Kuhner, Tobias Schubert, Massimo Cenciarini, Isabella Katharina Wiesmeier, Volker Arnd Coenen, Wolfram Burgard, Cornelius Weiller, Christoph Maurer
Correlations between Motor Symptoms across Different Motor Tasks, Quantified via Random Forest Feature Classification in Parkinson’s Disease
2017 Frontiers in Neurology
» show abstract« hide abstract
AbstractBackground: Objective assessments of Parkinson’s disease (PD) patients’ motor state using motion capture techniques are still rarely used in clinical practice, even though they may improve clinical management. One major obstacle relates to the large dimensionality of motor abnormalities in PD. We aimed to extract global motor performance measures covering different everyday motor tasks, as a function of a clinical intervention, i.e., deep brain stimulation (DBS) of the subthalamic nucleus. Methods: We followed a data-driven, machine-learning approach and propose performance measures that employ Random Forests with probability distributions. We applied this method to 14 PD patients with DBS switched-off or -on, and 26 healthy control subjects performing the Timed Up and Go Test (TUG), the Functional Reach Test (FRT), a hand coordination task, walking 10-m straight, and a 90° curve. Results: For each motor task, a Random Forest identified a specific set of metrics that optimally separated PD off DBS from healthy subjects. We noted the highest accuracy (94.6%) for standing up. This corresponded to a sensitivity of 91.5% to detect a PD patient off DBS, and a specificity of 97.2% representing the rate of correctly identified healthy subjects. We then calculated performance measures based on these sets of metrics and applied those results to characterize symptom severity in different motor tasks. Task-specific symptom severity measures correlated significantly with each other and with the Unified Parkinson’s Disease Rating Scale (UPDRS, part III, correlation of r2 = 0.79). Agreement rates between different measures ranged from 79.8 to 89.3%. Conclusion: The close correlation of PD patients’ various motor abnormalities quantified by different, task-specific severity measures suggests that these abnormalities are only facets of the underlying one-dimensional severity of motor deficits. The identification and characterization of this underlying motor deficit may help to optimize therapeutic interventions, e.g., to “automatically” adapt DBS settings in PD patients.
Hassan Hatefi, Ralf Wimmer, Bettina Braitling, Luis Maria Ferrer Fioriti, Bernd Becker, Holger Hermanns
Cost vs. Time in Stochastic Games and Markov Automata
2017 Form Asp Comput, volume: 29, issue: 4, pages: 629 - 649
» show abstract« hide abstract
AbstractCosts and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rewards and cost-bounded reachability for Markov automata and Markov games. We provide a fixed point characterization of this class of properties under early schedulers. Additionally, we give a transformation to expected time-bounded rewards and time-bounded reachability, which can be computed by available algorithms. We prove the correctness of the transformation and show its effectiveness on a number of Markov automata case studies.
Köhler S, Schindelhauer C, Jakoby A
Cyclone codes
2017 International Symposium on Information Theory , pages: 156 - 160
Aktas Tugce, Avsar Ilik Ibrahim, Maticzka Daniel, Bhardwaj Vivek, Pessoa Rodrigues Cecilia, Mittler Gerhard, Manke Thomas, Backofen Rolf, Akhtar Asifa
DHX9 suppresses RNA processing defects originating from the Alu invasion of the human genome
2017 Nature, volume: 544, issue: 7648, pages: 115 - 119
» show abstract« hide abstract
AbstractTransposable elements are viewed as ’selfish genetic elements’, yet they contribute to gene regulation and genome evolution in diverse ways. More than half of the human genome consists of transposable elements. Alu elements belong to the short interspersed nuclear element (SINE) family of repetitive elements, and with over 1 million insertions they make up more than 10% of the human genome. Despite their abundance and the potential evolutionary advantages they confer, Alu elements can be mutagenic to the host as they can act as splice acceptors, inhibit translation of mRNAs and cause genomic instability. Alu elements are the main targets of the RNA-editing enzyme ADAR and the formation of Alu exons is suppressed by the nuclear ribonucleoprotein HNRNPC, but the broad effect of massive secondary structures formed by inverted-repeat Alu elements on RNA processing in the nucleus remains unknown. Here we show that DHX9, an abundant nuclear RNA helicase, binds specifically to inverted-repeat Alu elements that are transcribed as parts of genes. Loss of DHX9 leads to an increase in the number of circular-RNA-producing genes and amount of circular RNAs, translational repression of reporters containing inverted-repeat Alu elements, and transcriptional rewiring (the creation of mostly nonsensical novel connections between exons) of susceptible loci. Biochemical purifications of DHX9 identify the interferon-inducible isoform of ADAR (p150), but not the constitutively expressed ADAR isoform (p110), as an RNA-independent interaction partner. Co-depletion of ADAR and DHX9 augments the double-stranded RNA accumulation defects, leading to increased circular RNA production, revealing a functional link between these two enzymes. Our work uncovers an evolutionarily conserved function of DHX9. We propose that it acts as a nuclear RNA resolvase that neutralizes the immediate threat posed by transposon insertions and allows these elements to evolve as tools for the post-transcriptional regulation of gene expression.
Uwe Wagschal, Thomas Waldvogel, Thomas Metz, Bernd Becker, Linus Feiten, Samuel Weishaupt, Kamaljeet Singh
Das TV-Duell und die Landtagswahl in Schleswig-Holstein: Das Debat-O-Meter als neues Instrument der politischen Kommunikationsforschung
2017 Zeitschrift für Parlamentsfragen (ZParl), volume: 48. Jg., issue: 3, pages: 594 - 613
» show abstract« hide abstract
AbstractPolitische TV-Debatten sind das Großereignis in modernen Wahlkämpfen und verstärkt Gegenstand von politik- und kommunikationswissenschaftlichen Untersuchungen. Die bisherige Forschung verwendete physische Eingabegeräte, die die Forscher auf Laborsettings mit kleinen Fallzahlen und negativen Effekten auf die externe Validität der Messung festlegte. Der Beitrag präsentiert eine Studie zur Landtagswahl in Schleswig-Holstein 2017 mit dem Debat-O-Meter, eine neue internetbasierte Anwendung für Smartphones, Tablets und PCs, die die Analyse von Wahrnehmungen und Wirkungen von politischen TV-Debatten mit einer großen Anzahl an Teilnehmenden in natürlichen Rezeptionssituationen erlaubt. Es wird gezeigt, dass „Real-Time Response“-Messungen (RTR) mit einer großen Teilnehmerzahl von mehr als 850 durch neue Wege der Rekrutierung mithilfe von Medienpartnern außerhalb des Labors möglich sind. Die Analyse belegt, dass Herausforderer Daniel Günther (CDU) die Debatte für sich entscheiden konnte und identifiziert die Parteineigung, die RTR-Bewertung und die Kandidateneinschätzung in der Vorbefragung als erklärungskräftigste Variablen für den Debattensieg.
Ummenhofer B., Zhou H, Uhrig J, Mayer N, Ilg E., Dosovitskiy A., Brox T.
DeMoN: Depth and Motion Network for Learning Monocular Stereo
2017 IEEE Conference on Computer Vision and Pattern Recognition (CVPR) IEEE Conference on Computer Vision and Pattern Recognition

Download file as PDF
Kolkhorst Henrich, Burgard Wolfram, Tangermann Michael
Decoding Hazardous Events in Driving Videos
2017 Graz, Austria Proceedings of the 7th Graz Brain-Computer Interface Conference 2017, Verlag der Technischen Universität Graz, pages: 242 - 247
» show abstract« hide abstract
AbstractDecoding the human brain state with BCI methods can be seen as a building block for human-machine interaction, providing a noisy but objective, low-latency information channel including human reactions to the environment. Specifically in the context of autonomous driving, human judgement is relevant in high-level scene understanding. Despite advances in computer vision and scene understanding, it is still challenging to go from the detection of traffic events to the detection of hazards. We present a preliminary study on hazard perception, implemented in the context of natural driving videos. These have been augmented with artificial events to create potentially hazardous driving situations. We decode brain signals from electroencephalography (EEG) in order to classify single events into hazardous and non-hazardous ones. We find that event-related responses can be discriminated and the classification of events yields an AUC of 0.79. We see these results as a step towards incorporating EEG feedback into more complex, real-world tasks.
Kolkhorst Henrich, Tangermann Michael, Burgard Wolfram
Decoding Perceived Hazardousness from User’s Brain States to Shape Human-Robot Interaction
2017 International Conference on Human-Robot Interaction, Vienna, Austria Proceedings of the Companion of the 2017 ACM/IEEE International Conference on Human-Robot Interaction, ACM, pages: 349 - 350

Download file
Schirrmeister Robin, Springenberg Jost, Fiederer Lukas, Glasstetter Martin, Eggensperger Katharina, Tangermann Michael, Hutter Frank, Burgard Wolfram, Ball Tonio
Deep learning with convolutional neural networks for EEG decoding and visualization
2017 Human Brain Mapping
Schirrmeister R, Springenberg T, Fiederer L, Glasstetter M, Eggensperger K, Tangermann M, Hutter F, Burgard W, Ball T
Deep learning with convolutional neural networks for EEG decoding and visualization
2017 Human Brain Mapping, volume: 38, pages: 5391 - 5420
Schirrmeister Robin, Springenberg Jost, Fiederer Lukas, Glasstetter Martin, Eggensperger Katharina, Tangermann Michael, Hutter Frank, Burgard Wolfram, Ball Tonio
Deep learning with convolutional neural networks for brain mapping and decoding of movement-related information from the human EEG
2017 ArXiv e-prints
» show abstract« hide abstract
AbstractDeep learning with convolutional neural networks (deep ConvNets) has revolutionized computer vision through end-to-end learning, i.e. learning from the raw data. Now, there is increasing interest in using deep ConvNets for end-to-end EEG analysis. However, little is known about many important aspects of how to design and train ConvNets for end-to-end EEG decoding, and there is still a lack of techniques to visualize the informative EEG features the ConvNets learn. Here, we studied deep ConvNets with a range of different architectures, designed for decoding imagined or executed movements from raw EEG. Our results show that recent advances from the machine learning field, including batch normalization and exponential linear units, together with a cropped training strategy, boosted the deep ConvNets decoding performance, reaching or surpassing that of the widely-used filter bank common spatial patterns (FBCSP) decoding algorithm. While FBCSP is designed to use spectral power modulations, the features used by ConvNets are not fixed a priori. Our novel methods for visualizing the learned features demonstrated that ConvNets indeed learned to use spectral power modulations in the alpha, beta and high gamma frequencies. These methods also proved useful as a technique for spatially mapping the learned features, revealing the topography of the causal contributions of features in different frequency bands to decoding the movement classes. Our study thus shows how to design and train ConvNets to decode movement-related information from the raw EEG without handcrafted features and highlights the potential of deep ConvNets combined with advanced visualization techniques for EEG-based brain mapping.
Böttcher S, Scholl P, Van Laerhoven K
Detecting process transitions from wearable sensors: An unsupervised labeling approach
2017 ACM International Conference Proceeding Series, volume: Part F1319
» show abstract« hide abstract
Abstract© 2017 Association for Computing Machinery. Authoring protocols for manual tasks such as following recipes, manufacturing processes, or laboratory experiments requires a significant effort. This paper presents a system that estimates individual procedure transitions from the user’s physical movement and gestures recorded with inertial motion sensors. Combined with egocentric or external video recordings this facilitates efficient review and annotation of video databases. We investigate different clustering algorithms on wearable inertial sensor data recorded on par with video data, to automatically create transition marks between task steps. The goal is to match these marks to the transitions given in a description of the workflow, thus creating navigation cues to browse video repositories of manual work. To evaluate the performance of unsupervised clustering algorithms, the automatically generated marks are compared to human-expert created labels on publicly available datasets. Additionally, we tested the approach on a novel data set in a manufacturing lab environment, describing an existing sequential manufacturing process.
Böttcher S, Scholl P, Van Laerhoven K
Detecting process transitions from wearable sensors: An unsupervised labeling approach
2017 ACM International Conference Proceeding Series, volume: Part F1319
» show abstract« hide abstract
Abstract© 2017 Association for Computing Machinery. Authoring protocols for manual tasks such as following recipes, manufacturing processes, or laboratory experiments requires a significant effort. This paper presents a system that estimates individual procedure transitions from the user’s physical movement and gestures recorded with inertial motion sensors. Combined with egocentric or external video recordings this facilitates efficient review and annotation of video databases. We investigate different clustering algorithms on wearable inertial sensor data recorded on par with video data, to automatically create transition marks between task steps. The goal is to match these marks to the transitions given in a description of the workflow, thus creating navigation cues to browse video repositories of manual work. To evaluate the performance of unsupervised clustering algorithms, the automatically generated marks are compared to human-expert created labels on publicly available datasets. Additionally, we tested the approach on a novel data set in a manufacturing lab environment, describing an existing sequential manufacturing process.
Neuhaus Klaus, Landstorfer Richard, Simon Svenja, Schober Steffen, Wright Patrick, Smith Cameron, Backofen Rolf, Wecko Romy, Keim Daniel, Scherer Siegfried
Differentiation of ncRNAs from small mRNAs in Escherichia coli O157:H7 EDL933 (EHEC) by combined RNAseq and RIBOseq - ryhB encodes the regulatory RNA RyhB and a peptide, RyhP
2017 BMC Genomics, volume: 18, issue: 1
» show abstract« hide abstract
AbstractBACKGROUND: While NGS allows rapid global detection of transcripts, it remains difficult to distinguish ncRNAs from short mRNAs. To detect potentially translated RNAs, we developed an improved protocol for bacterial ribosomal footprinting (RIBOseq). This allowed distinguishing ncRNA from mRNA in EHEC. A high ratio of ribosomal footprints per transcript (ribosomal coverage value, RCV) is expected to indicate a translated RNA, while a low RCV should point to a non-translated RNA. RESULTS: Based on their low RCV, 150 novel non-translated EHEC transcripts were identified as putative ncRNAs, representing both antisense and intergenic transcripts, 74 of which had expressed homologs in E. coli MG1655. Bioinformatics analysis predicted statistically significant target regulons for 15 of the intergenic transcripts; experimental analysis revealed 4-fold or higher differential expression of 46 novel ncRNA in different growth media. Out of 329 annotated EHEC ncRNAs, 52 showed an RCV similar to protein-coding genes, of those, 16 had RIBOseq patterns matching annotated genes in other enterobacteriaceae, and 11 seem to possess a Shine-Dalgarno sequence, suggesting that such ncRNAs may encode small proteins instead of being solely non-coding. To support that the RIBOseq signals are reflecting translation, we tested the ribosomal-footprint covered ORF of ryhB and found a phenotype for the encoded peptide in iron-limiting condition. CONCLUSION: Determination of the RCV is a useful approach for a rapid first-step differentiation between bacterial ncRNAs and small mRNAs. Further, many known ncRNAs may encode proteins as well.
Nima Sedaghat,, A. Mahabal
Effective Image Differencing with ConvNets for Real-time Transient Hunting
2017 Mon Not R Astron Soc

Download file
Biedenkapp A, Lindauer M, Eggensperger K, Fawcett C, Hoos H, Hutter F
Efficient Parameter Importance Analysis via Ablation with Surrogates
2017 Proceedings of the AAAI conference, pages: 773 - 779
Gabriel Leivas Oliveira,, C. Bollen,, W. Burgard,, Thomas Brox
Efficient and Robust Deep Networks for Semantic Segmentation
2017 Int J Robot Res

Download file
O. Makansi,, Eddy Ilg,, Thomas Brox
End-to-End Learning of Video Super-Resolution with Motion Compensation
2017

Download file
Pascal Raiola, Jan Burchard, Felix Neubauer, Dominik Erb, Bernd Becker
Evaluating the Effectiveness of D-chains in SAT-based ATPG and Diagnostic TPG
2017 J Electron Test, volume: 33, issue: 6, pages: 751 - 767
» show abstract« hide abstract
AbstractThe ever increasing size and complexity of today's Very-Large-Scale-Integration (VLSI) designs requires a thorough investigation of new approaches for the generation of test patterns for both test and diagnosis of faults. SAT-based automatic test pattern generation (ATPG) is one of the most popular methods, where, in contrast to classical structural ATPG methods, first a mathematical representation of the problem in form of a Boolean formula is generated, which is then evaluated by a specialized solver. If the considered fault is testable, the solver will return a satisfying assignment, from which a test pattern can be extracted; otherwise no such assignment can exist. In order to speed up test pattern generation, the concept of D-chains was introduced by Larrabee (1992). Hereby supplementary clauses are added to the Boolean formula, reducing the search space and guiding the solver towards the solution. In the past, different variants of D-chains have been developed, such as the backward D-chain or the indirect D-chain. In this work we perform a thorough analysis and evaluation of the D-chain variants for test pattern generation and also analyze the impact of different D-chain encodings on diagnostic test pattern generation. Our experimental results show that depending on the incorporated D-chain the runtime can be reduced tremendously.
Schindelhauer C, Reinld L, Kumberg T
Exploiting Concurrent Wake-Up Transmissions Using Beat Frequencies
2017 J Sensors, issue: 17, supplement: 8, pages: 1717 - 1717
Klein A, Falkner S, Bartels S, Hennig P, Hutter F
Fast Bayesian Optimization of Machine Learning Hyperparameters on Large Datasets
2017 Proceedings of the AISTATS conference
Klein A, Falkner S, Bartels S, Hennig P, Hutter F
Fast Bayesian hyperparameter optimization on large datasets
2017 Electronic Journal of Statistics, volume: 11
Jan Burchard, Dominik Erb, Adit D. Singh, Sudhakar M. Reddy, Bernd Becker
Fast and Waveform-Accurate Hazard-Aware SAT-Based TSOF ATPG
2017 Conference on Design, Automation and Test in Europe
» show abstract« hide abstract
AbstractOpens are known to be one of the predominant defects in nanoscale technologies. Especially with an increasing number of complex cells in today’s VLSI designs intra-gate opens are becoming a major problem. The generation of tests for these faults is hard, as the timing of the circuit needs to be considered accurately to prevent the invalidation of the generated tests through hazards. Current test generation methods, including new cell aware tests that explicitly target open defects, ignore the possibility of hazard caused test invalidation. Such tests can fail to detect a significant fraction of the targeted opens. In this work we present a waveform-accurate hazard-aware test generation approach to target intra-gate opens. Our methodology is based on a SAT-based encoding and allows the generation of tests guaranteed to be robust against hazards. Experimental results for large benchmarks mapped to the state-of-the-art NanGate 45nm cell library including complex cells show the test generation efficiency of the proposed method. Large circuits were efficiently handled – even without the use of fault simulation. Our experiments show that on average, about 10.92 % of conventional hazard- unaware tests will fail to detect the targeted opens because of test invalidation – these are reliably detected by our new test generation methodology. Importantly, our approach can also be applied to improve the effectiveness of commercial cell aware tests.
Martinez-Cantin R, Tee K, Mccourt M, Eggensperger K
Filtering Outliers in Bayesian Optimization
2017 NIPS workshop on Bayesian Optimization (BayesOpt’17)
Eddy Ilg,, Nikolaus Mayer,, Tonmoy Saikia,, Margret Keuper,, Alexey Dosovitskiy,, Thomas Brox
FlowNet 2.0: Evolution of Optical Flow Estimation with Deep Networks
2017

Download file
Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker
From DQBF to QBF by Dependency Elimination
2017 Melbourne, VIC, Australia Int'l Conf. on Theory and Applications of Satisfiability Checking, Serge Gaspers and Toby Walsh, volume: 10491, pages: 326 - 343
» show abstract« hide abstract
AbstractIn this paper, we propose the elimination of dependencies to convert a given dependency quantified Boolean formula (DQBF) to an equisatisfiable QBF. We show how to select a set of dependencies to eliminate such that we arrive at a smallest equisatisfiable QBF in terms of existential variables that is achievable using dependency elimination. This approach is improved by taking so-called don't-care dependencies into account, which result from the application of dependency schemes to the formula and can be added to or removed from the formula at no cost. We have implemented this new method in the state-of-the-art DQBF solver HQS. Experiments show that dependency elimination is clearly superior to the previous method using variable elimination.
Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker
From DQBF to QBF by Dependency Elimination
2017 International Conference on Theory and Applications of Satisfiability Testing (SAT), issue: 10491, pages: 326 - 343
» show abstract« hide abstract
AbstractIn this paper, we propose the elimination of dependencies to convert a given dependency quantified Boolean formula (DQBF) to an equisatisfiable QBF. We show how to select a set of dependencies to eliminate such that we arrive at a smallest equisatisfiable QBF in terms of existential variables that is achievable using dependency elimination. This approach is improved by taking so-called don’t-care dependencies into account, which result from the application of dependency schemes to the formula and can be added to or removed from the formula at no cost. We have implemented this new method in the state-of-the-art DQBF solver HQS. Experiments show that dependency elimination is clearly superior to the previous method using variable elimination.
Benjamin Ummenhofer,, Thomas Brox
Global, Dense Multiscale Reconstruction for a Billion Points
2017 Int J Comput Vision, volume: 125, issue: 1-3, pages: 82 - 94

Download file
Ralf Wimmer, Sven Reimer, Paolo Marin, Bernd Becker
HQSpre - An Effective Preprocessor for QBF and DQBF
2017 Uppsala, Sweden International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part I, Axel Legay and Tiziana Margaria, volume: 10205, pages: 373 - 390
» show abstract« hide abstract
AbstractWe present our new preprocessor \textsc{HQSpre}, a state-of-the-art tool for simplifying quantified Boolean formulas (QBFs) and the first available preprocessor for dependency quantified Boolean formulas (DQBFs). The latter are a generalization of QBFs, resulting from adding so-called Henkin-quantifiers to QBFs. HQSpre applies most of the preprocessing techniques that have been proposed in the literature. It can be used both as a standalone tool and as a library. It is possible to tailor it towards different solver back-ends, e. g., to preserve the circuit structure of the formula when a non-CNF solver back-end is used. Extensive experiments show that HQSpre allows QBF solvers to solve more benchmark instances and is able to decide more instances on its own than state-of-the-art tools. The same impact can be observed in the DQBF domain as well.
Linus Feiten, Matthias Sauer, Bernd Becker
Implementation of Delay-Based PUFs on Altera FPGAs
In: Hardware Security and Trust: Design and Deployment of Integrated Circuits in a Threatened Environment
2017, Springer International Publishing, pages: 211 - 235, ISBN: 978-3-319-44318-8
» show abstract« hide abstract
AbstractThis chapter focuses on the implementation of delay-based PUFs on Altera FPGAs. While there has been a manifold of publications on how to evaluate and refine PUFs, a thorough description of the required "handicrafts" enabling a novice to enter this exciting research field has so far been missing. The methods shared in this chapter are not just easily extractable from available standard documentation, but have been compiled by the authors over a long period of trials and consultations with the Altera user community. Designing a delay-based PUF on FPGAs requires fine-tuning which is often like diverting the automated design tools from their intended use. For example, the device-specific delays for the PUF response generation are generally gathered from circuitry looking redundant to the bitstream compiler. Therefore, the automatic reduction of such seemingly redundant circuitry must be prevented. The way the circuitry is placed and routed also has a major impact on delay characteristics, so it is necessary to customise this instead of letting the compiler do it automatically. The reader will be walked through all necessary steps by means of a running example enabling them to embark on further experiments on their own. Along the way, the architecture of Altera Cyclone FPGAs is explained and results from the authors' own experimental studies are shared.
Hübner David, Kindermans Pieter-Jan, Verhoeven Thibault, Tangermann Michael
Improving learning from label proportions by reducing the feature dimensionality
2017 Proceedings of the 7th International Brain-Computer Interface Meeting 2017: From Vision to Reality, Verlag der Technischen Universität Graz, pages: 186 - 191
Wagner M, Friedrich T, Lindauer M
Improving local search in a minimum vertex cover solver for classes of networks
2017 Proceedings of the IEEE Congress on Evolutionary Computation (CEC)
Schindelhauer C, Moharrami M, Reindl L, Kumberg T
Improving the performance of the cross-layer wake-up routing protocol T-ROME
2017 13th International Wireless Communications and Mobile Computing Conference , pages: 780 - 785
Verhoeven Thibault, Hübner David, Tangermann Michael, Müller Klaus-Robert, Dambre Joni, Kindermans Pieter-Jan
Improving zero-training brain-computer interfaces by mixing model estimators
2017 Journal of Neural Engineering, volume: 14, issue: 3, page: 036021
» show abstract« hide abstract
AbstractObjective. Brain-computer interfaces (BCI) based on event-related potentials (ERP) incorporate a decoder to classify recorded brain signals and subsequently select a control signal that drives a computer application. Standard supervised BCI decoders require a tedious calibration procedure prior to every session. Several unsupervised classification methods have been proposed that tune the decoder during actual use and as such omit this calibration. Each of these methods has its own strengths and weaknesses. Our aim is to improve overall accuracy of ERP-based BCIs without calibration.Approach. We consider two approaches for unsupervised classification of ERP signals. Learning from label proportions (LLP) was recently shown to be guaranteed to converge to a supervised decoder when enough data is available. In contrast, the formerly proposed expectation maximization (EM) based decoding for ERP-BCI does not have this guarantee. However, while this decoder has high variance due to random initialization of its parameters, it obtains a higher accuracy faster than LLP when the initialization is good.We introduce a method to optimally combine these two unsupervised decoding methods, letting one method’s strengths compensate for the weaknesses of the other and vice versa. The new method is compared to the aforementioned methods in a resimulation of an experiment with a visual speller.Main Results. Analysis of the experimental results shows that the new method exceeds the performance of the previous unsupervised classification approaches in terms of ERP classification accuracy and symbol selection accuracy during the spelling experiment. Furthermore, the method shows less dependency on random initialization of model parameters and is consequently more reliable.Significance. Improving the accuracy and subsequent reliability of calibrationless BCIs makes these systems more appealing for frequent use.
Mann Martin, Wright Patrick, Backofen Rolf
IntaRNA 2.0: enhanced and customizable prediction of RNA-RNA interactions
2017 Nucleic Acids Res, volume: 45, issue: W1, pages: W435 - W439
» show abstract« hide abstract
AbstractThe IntaRNA algorithm enables fast and accurate prediction of RNA-RNA hybrids by incorporating seed constraints and interaction site accessibility. Here, we introduce IntaRNAv2, which enables enhanced parameterization as well as fully customizable control over the prediction modes and output formats. Based on up to date benchmark data, the enhanced predictive quality is shown and further improvements due to more restrictive seed constraints are highlighted. The extended web interface provides visualizations of the new minimal energy profiles for RNA-RNA interactions. These allow a detailed investigation of interaction alternatives and can reveal potential interaction site multiplicity. IntaRNAv2 is freely available (source and binary), and distributed via the conda package manager. Furthermore, it has been included into the Galaxy workflow framework and its already established web interface enables ad hoc usage.
E. Levinkov,, Jonas Uhrig,, S. Tang,, M. Omran,, E. Insafutdinov,, A. Kirillov,, C. Rother,, Thomas Brox,, B. Schiele,, B. Andres
Joint Graph Decomposition & Node Labeling: Problem, Algorithms, Applications
2017

Download file
Rippon, G., Jordan-Young, R., Kaiser, A., Joel, D., Fine, C.
Journal of Neuroscience Research Policy on Addressing Sex as a Biological Variable: Comments, Clarifications, and Elaborations.
2017 Journal of Neuroscience Research, volume: 95, issue: 7, pages: 1357 - 1359
Gruning Bjorn, Rasche Eric, Rebolledo-Jaramillo Boris, Eberhard Carl, Houwaart Torsten, Chilton John, Coraor Nate, Backofen Rolf, Taylor James, Nekrutenko Anton
Jupyter and Galaxy: Easing entry barriers into complex data analyses for biomedical researchers
2017 PLoS Comput Biol, volume: 13, issue: 5
» show abstract« hide abstract
AbstractWhat does it take to convert a heap of sequencing data into a publishable result? First, common tools are employed to reduce primary data (sequencing reads) to a form suitable for further analyses (i.e., the list of variable sites). The subsequent exploratory stage is much more ad hoc and requires the development of custom scripts and pipelines, making it problematic for biomedical researchers. Here, we describe a hybrid platform combining common analysis pathways with the ability to explore data interactively. It aims to fully encompass and simplify the "raw data-to-publication" pathway and make it reproducible.
Klein A, Falkner S, Springenberg J, Hutter F
Learning Curve Prediction with Bayesian Neural Networks
2017 International Conference on Learning Representations (ICLR) 2017 Conference Track
Hübner David, Verhoeven Tibault, Schmid Konstantin, Müller Klaus-Robert, Tangermann Michael, Kindermans Pieter-Jan
Learning from Label Proportions in Brain-Computer Interfaces: Online Unsupervised Learning with Guarantees
2017 ArXiv e-prints
Hübner David, Verhoeven Thibault, Schmid Konstantin, Müller Klaus-Robert, Tangermann Michael, Kindermans Pieter-Jan
Learning from label proportions in brain-computer interfaces: online unsupervised learning with guarantees
2017 PloS one, volume: 12, issue: 4, page: e0175856
Christian Zimmermann,, Thomas Brox
Learning to Estimate 3D Hand Pose from Single RGB Images
2017

Download file
Alexey Dosovitskiy,, J. Springenberg,, Maxim Tatarchenko,, Thomas Brox
Learning to Generate Chairs, Tables and Cars with Convolutional Networks
2017 Ieee T Pattern Anal, volume: 39, issue: 4, pages: 692 - 705

Download file
Scholl P, Van Laerhoven K
Lessons learned from designing an instrumented lighter for assessing smoking status
2017 UbiComp/ISWC 2017 - Adjunct Proceedings of the 2017 ACM International Joint Conference on Pervasive and Ubiquitous Computing and Proceedings of the 2017 ACM International Symposium on Wearable Computers
» show abstract« hide abstract
AbstractCopyright © 2017 ACM. Assessing smoking status from wearable sensors can potentially create novel cessation therapies for the global smoking epidemic, without requiring users to regularly fill in questionnaires to obtain their smoking data. In this paper we discuss several design iterations of an instrumented cigarette lighter the records when it is used, to provide the ground-truth for detection from sensor signals measured at the human body, or to provide an alternative low-delay detection mechanism for smoking.
Scholl P, Van Laerhoven K
Lessons learned from designing an instrumented lighter for assessing smoking status
2017 UbiComp/ISWC 2017 - Adjunct Proceedings of the 2017 ACM International Joint Conference on Pervasive and Ubiquitous Computing and Proceedings of the 2017 ACM International Symposium on Wearable Computers
» show abstract« hide abstract
AbstractCopyright © 2017 ACM. Assessing smoking status from wearable sensors can potentially create novel cessation therapies for the global smoking epidemic, without requiring users to regularly fill in questionnaires to obtain their smoking data. In this paper we discuss several design iterations of an instrumented cigarette lighter the records when it is used, to provide the ground-truth for detection from sensor signals measured at the human body, or to provide an alternative low-delay detection mechanism for smoking.
Yuliya Butkova, Ralf Wimmer, Holger Hermanns
Long-run Rewards for Markov Automata
2017 Uppsala, Sweden International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part II, Axel Legay and Tiziana Margaria, volume: 10206, pages: 188 - 203
» show abstract« hide abstract
AbstractMarkov automata are a powerful formalism for modelling systems which exhibit nondeterminism, probabilistic choices and continuous stochastic timing. We consider the computation of long-run average rewards, the most classical problem in continuous-time Markov model analysis. We propose an algorithm based on value iteration. It improves the state of the art by orders of magnitude. The contribution is rooted in a fresh look on Markov automata, namely by treating them as an efficient encoding of CTMDPs with -- in the worst case -- exponentially more transitions.
Nicastro Giuseppe, Candel Adela, Uhl Michael, Oregioni Alain, Hollingworth David, Backofen Rolf, Martin Stephen, Ramos Andres
Mechanism of beta-actin mRNA Recognition by ZBP1
2017 Cell Rep, volume: 18, issue: 5, pages: 1187 - 1199
» show abstract« hide abstract
AbstractZipcode binding protein 1 (ZBP1) is an oncofetal RNA-binding protein that mediates the transport and local translation of beta-actin mRNA by the KH3-KH4 di-domain, which is essential for neuronal development. The high-resolution structures of KH3-KH4 with their respective target sequences show that KH4 recognizes a non-canonical GGA sequence via an enlarged and dynamic hydrophobic groove, whereas KH3 binding to a core CA sequence occurs with low specificity. A data-informed kinetic simulation of the two-step binding reaction reveals that the overall reaction is driven by the second binding event and that the moderate affinities of the individual interactions favor RNA looping. Furthermore, the concentration of ZBP1, but not of the target RNA, modulates the interaction, which explains the functional significance of enhanced ZBP1 expression during embryonic development.
Weidenbach Katrin, Nickel Lisa, Neve Horst, Alkhnbashi Omer, Kunzel Sven, Kupczok Anne, Bauersachs Thorsten, Cassidy Liam, Tholey Andreas, Backofen Rolf, Schmitz Ruth
MetSV, a novel archaeal lytic virus targeting Methanosarcina strains
2017 J Virol
» show abstract« hide abstract
AbstractA novel archaeal lytic virus targeting species of the genus Methanosarcina was isolated using Methanosarcina mazei strain Go1 as host. Due to its spherical morphology the virus was designated Methanosarcinaspherical virus (MetSV). Molecular analysis demonstrated that MetSV contains double stranded linear DNA with a genome size of 10,567 bp containing 22 open reading frames (ORFs) all oriented in the same direction. Functions were predicted for some of these ORFs, i. e. like DNA polymerase, ATPase, DNA-binding protein, as well as envelope (structural) protein. MetSV-derived spacers in CRISPR loci were detected in several published Methanosarcina draft genomes using bioinformatic tools, revealing the potential PAM motif (TTA/T). Transcription and expression of several predicted viral ORFs were validated by RT-PCR, PAGE analysis and LC-MS based proteomics. Analysis of core lipids by APCI mass spectrometry showed that MetSV and M. mazei both contain archaeol and glycerol dialkyl glycerol tetraether without cyclopentane moiety (GDGT-0). The MetSV host range is limited to Methanosarcina strains growing as single cells (M. mazei, M. bakeri and M. soligelidi). In contrast, strains growing as sarcina-like aggregates were apparently protected from infection. Heterogeneity related to morphology phases in M. mazei cultures allowed acquisition of resistance to MetSV after challenge by growing as sarcina-like aggregates. CRISPR/Cas mediated resistance was excluded since neither of the two CRISPR arrays showed MetSV-derived spacer acquisition. Based on these findings, we propose that changing the morphology from single cells to sarcina-like aggregates upon rearrangement of the envelope structure prevents infection and subsequent lysis by MetSV.IMPORTANCE Methanoarchaea are among the most abundant organisms on the planet since they are present in high numbers in major anaerobic environments. They convert various carbon sources e.g. acetate, methylamines or methanol to methane and carbon dioxide, thus they have a significant impact on the emission of major greenhouse gases. Today very little is known about viruses specifically infecting methanoarchaea, which most probably impact the abundance of methanoarchaea in microbial consortia. Here we characterize the first identified Methanosarcina infecting virus (MetSV) and show a mechanism for acquiring resistance against MetSV. Based on our results we propose that growth as sarcina-like aggregates prevents infection and subsequent lysis. These findings allow new insights into virus-host relationship in methanogenic community structures, their dynamics and their phase heterogeneity. Moreover, the availability of a specific virus provides new possibilities to deepen our knowledge on defence mechanisms of potential hosts and offers tools for genetic manipulation.
Hübner David, Verhoeven Thibault, Kindermans Pieter-Jan, Tangermann Michael
Mixing two unsupervised estimators for event-related potential decoding: An online evaluation
2017 Proceedings of the 7th International Brain-Computer Interface Meeting 2017: From Vision to Reality, Verlag der Technischen Universität Graz, pages: 198 - 203
Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Kaoten, Becker B
Motion Planning under Partial Observability using Game-Based Abstraction
2017 Melbourne, VIC, Australia 56th IEEE Conf. on Decision and Control (CDC), pages: 2201 - 2208
» show abstract« hide abstract
AbstractWe study motion planning problems where agents move inside environments that are not fully observable and subject to uncertainties. The goal is to compute a strategy for an agent that is guaranteed to satisfy certain safety and performance specifications. Such problems are naturally modeled by partially observable Markov decision processes (POMDPs). Because of the potentially huge or even infinite belief space of POMDPs, verification and strategy synthesis is in general computationally intractable. We tackle this difficulty by exploiting typical structural properties of such scenarios; for instance, we assume that agents have the ability to observe their own positions inside an evironment. Ambiguity in the state of the environment is abstracted into non-deterministic choices over the possible states of the environment. Technically, this abstraction transforms POMDPs into probabilistic two-player games (PGs). For these PGs, efficient verification tools are able to determine strategies that approximate certain measures on the POMDP. If an approximation is too coarse to provide guarantees, an abstraction refinement scheme further resolves the belief space of the POMDP. We demonstrate that our method improves the state of the art by orders of magnitude compared to a direct solution of the POMDP.
Maxim Tatarchenko,, Alexey Dosovitskiy,, Thomas Brox
Octree Generating Networks: Efficient Convolutional Architectures for High-resolution 3D Outputs
2017

Download file
Robert Mattmüller, Florian Geißer, Benedict Wright, Bernhard Nebel
On the Relationship Between State-Dependent Action Costs and Conditional Effects in Planning
2017
Scholl P, Van Laerhoven K
On the statistical properties of body-worn inertial motion sensor data for identifying sensor modality
2017 Proceedings - International Symposium on Wearable Computers, ISWC, volume: Part F1305
» show abstract« hide abstract
Abstract© 2017 Copyright held by the owner/author(s). Interpreting datasets containing inertial data (acceleration, rateof- turn, magnetic flux) requires a description of the datasets itself. Often this description is unstructured, stored as a convention or simply not available anymore. In this note, we argue that each modality exhibits particular statistical properties, which allows to reconstruct it solely from the sensor’s data. To investigate this, tri-axial inertial sensor data from five publicly available datasets were analysed. Three statistical properties: mode, kurtosis, and number of modes are shown to be sufficient for classification - assuming the sampling rate and sample format are known, and that both acceleration and magnetometer data is present. While those assumption hold, 98% of all 1003 data points were correctly classified.
Scholl P, Van Laerhoven K
On the statistical properties of body-worn inertial motion sensor data for identifying sensor modality
2017 Proceedings - International Symposium on Wearable Computers, ISWC, volume: Part F1305
» show abstract« hide abstract
Abstract© 2017 Copyright held by the owner/author(s). Interpreting datasets containing inertial data (acceleration, rateof- turn, magnetic flux) requires a description of the datasets itself. Often this description is unstructured, stored as a convention or simply not available anymore. In this note, we argue that each modality exhibits particular statistical properties, which allows to reconstruct it solely from the sensor’s data. To investigate this, tri-axial inertial sensor data from five publicly available datasets were analysed. Three statistical properties: mode, kurtosis, and number of modes are shown to be sufficient for classification - assuming the sampling rate and sample format are known, and that both acceleration and magnetometer data is present. While those assumption hold, 98% of all 1003 data points were correctly classified.
Lindauer Marius, van Rijn Jan, Kotthoff Lars
Open Algorithm Selection Challenge 2017: Setup and Scenarios
2017 Brussels, Belgium Proceedings of the Open Algorithm Selection Challenge, PMLR, volume: 79, pages: 1 - 7
Bischl Bernd, Casalicchio Giuseppe, Feurer Matthias, Hutter Frank, Lang Michel, Mantovani Rafael, van Rijn Jan, Vanschoren Joaquin
OpenML Benchmarking Suites and the OpenML100
2017 arXiv, volume: 1708.0373, pages: 1 - 6
Nima Sedaghat,, Mohammadreza, Zolfaghari,, E. Amiri,, Thomas Brox
Orientation-boosted voxel nets for 3D object recognition
2017

Download file
Bast H, Buchhold B, Haussmann E
Overview of the Triple Scoring Task at the WSDM Cup 2017
2017
» show abstract« hide abstract
AbstractThis paper provides an overview of the triple scoring task at the WSDM Cup 2017, including a description of the task and the dataset, an overview of the participating teams and their results, and a brief account of the methods employed. In a nutshell, the task was to compute relevance scores for knowledge-base triples from relations, where such scores make sense. Due to the way the ground truth was constructed, scores were required to be integers from the range 0..7. For example, reasonable scores for the triples Tim Burton profession Director and Tim Burton profession Actor would be 7 and 2, respectively, because Tim Burton is well-known as a director, but he acted only in a few lesser known movies. The triple scoring task attracted considerable interest, with 52 initial registrations and 21 teams who submitted a valid run before the deadline. The winning team achieved an accuracy of 87%, that is, for that fraction of the triples from the test set (which was revealed only after the deadline) the difference to the score from the ground truth was at most 2. The best result for the average difference from the test set scores was 1.50.
Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker
Permissive Finite-State Controllers of POMDPs using Parameter Synthesis
2017
» show abstract« hide abstract
AbstractWe study finite-state controllers (FSCs) for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. The key insight is that computing (randomised) FSCs on POMDPs is equivalent to - and computationally as hard as - synthesis for parametric Markov chains (pMCs). This correspondence allows to use tools for parameter synthesis in pMCs to compute correct-by-construction FSCs on POMDPs for a variety of specifications. Our experimental evaluation shows comparable performance to well-known POMDP solvers.
Lindauer M, Hutter F
Pitfalls and Best Practices for Algorithm Configuration (Breakout Session Report)
2017 Dagstuhl Reports, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, volume: 6, pages: 70 - 72
Daume Michael, Uhl Michael, Backofen Rolf, Randau Lennart
RIP-Seq Suggests Translational Regulation by L7Ae in Archaea
2017 MBio, volume: 8, issue: 4
» show abstract« hide abstract
AbstractL7Ae is a universal archaeal protein that recognizes and stabilizes kink-turn (k-turn) motifs in RNA substrates. These structural motifs are widespread in nature and are found in many functional RNA species, including ribosomal RNAs. Synthetic biology approaches utilize L7Ae/k-turn interactions to control gene expression in eukaryotes. Here, we present results of comprehensive RNA immunoprecipitation sequencing (RIP-Seq) analysis of genomically tagged L7Ae from the hyperthermophilic archaeon Sulfolobus acidocaldarius A large set of interacting noncoding RNAs was identified. In addition, several mRNAs, including the l7ae transcript, were found to contain k-turn motifs that facilitate L7Ae binding. In vivo studies showed that L7Ae autoregulates the translation of its mRNA by binding to a k-turn motif present in the 5’ untranslated region (UTR). A green fluorescent protein (GFP) reporter system was established in Escherichia coli and verified conservation of L7Ae-mediated feedback regulation in Archaea Mobility shift assays confirmed binding to a k-turn in the transcript of nop5-fibrillarin, suggesting that the expression of all C/D box sRNP core proteins is regulated by L7Ae. These studies revealed that L7Ae-mediated gene regulation evolved in archaeal organisms, generating new tools for the modulation of synthetic gene circuits in bacteria.IMPORTANCE L7Ae is an essential archaeal protein that is known to structure ribosomal RNAs and small RNAs (sRNAs) by binding to their kink-turn motifs. Here, we utilized RIP-Seq methodology to achieve a first global analysis of RNA substrates for L7Ae. Several novel interactions with noncoding RNA molecules (e.g., with the universal signal recognition particle RNA) were discovered. In addition, L7Ae was found to bind to mRNAs, including its own transcript’s 5’ untranslated region. This feedback-loop control is conserved in most archaea and was incorporated into a reporter system that was utilized to control gene expression in bacteria. These results demonstrate that L7Ae-mediated gene regulation evolved originally in archaeal organisms. The feedback-controlled reporter gene system can easily be adapted for synthetic biology approaches that require strict gene expression control.
Backofen Rolf, Engelhardt Jan, Erxleben Anika, Fallmann Jorg, Gruning Bjorn, Ohler Uwe, Rajewsky Nikolaus, Stadler Peter
RNA-bioinformatics: Tools, services and databases for the analysis of RNA-based regulation
2017 J Biotechnol, volume: 261, pages: 76 - 84
» show abstract« hide abstract
AbstractThe importance of RNA-based regulation is becoming more and more evident. Genome-wide sequencing efforts have shown that the majority of the DNA in eukaryotic genomes is transcribed. Advanced high-throughput techniques like CLIP for the genome-wide detection of RNA-protein interactions have shown that post-transcriptional regulation by RNA-binding proteins matches the complexity of transcriptional regulation. The need for a specialized and integrated analysis of RNA-based data has led to the foundation of the RNA Bioinformatics Center (RBC) within the German Network of Bioinformatics Infrastructure (de.NBI). This paper describes the tools, services and databases provided by the RBC, and shows example applications. Furthermore, we have setup an RNA workbench within the Galaxy framework. For an easy dissemination, we offer a virtualized version of Galaxy (via Galaxy Docker) enabling other groups to use our RNA workbench in a very simple way.
Miladi Milad, Junge Alexander, Costa Fabrizio, Seemann Stefan, Hull Havgaard Jakob, Gorodkin Jan, Backofen Rolf
RNAscClust: clustering RNA sequences using structure conservation and graph based motifs
2017 Bioinformatics, volume: 33, issue: 14, pages: 2089 - 2096
» show abstract« hide abstract
AbstractMotivation: Clustering RNA sequences with common secondary structure is an essential step towards studying RNA function. Whereas structural RNA alignment strategies typically identify common structure for orthologous structured RNAs, clustering seeks to group paralogous RNAs based on structural similarities. However, existing approaches for clustering paralogous RNAs, do not take the compensatory base pair changes obtained from structure conservation in orthologous sequences into account. Results: Here, we present RNAscClust, the implementation of a new algorithm to cluster a set of structured RNAs taking their respective structural conservation into account. For a set of multiple structural alignments of RNA sequences, each containing a paralog sequence included in a structural alignment of its orthologs, RNAscClust computes minimum free-energy structures for each sequence using conserved base pairs as prior information for the folding. The paralogs are then clustered using a graph kernel-based strategy, which identifies common structural features.We show that the clustering accuracy clearly benefits from an increasing degree of compensatory base pair changes in the alignments. Availability: RNAscClust is available at www.bioinf.uni-freiburg.de/Software/RNAscClust.
Mummadi C, Kasireddy S, Peter Leo F, Scholl P, Verma K, Van Laerhoven K
Real-time embedded recognition of sign language alphabet fingerspelling in an IMU-based glove
2017 ACM International Conference Proceeding Series, volume: Part F1319
» show abstract« hide abstract
AbstractCopyright © 2017 Association for Computing Machinery. Data gloves have numerous applications, including enabling novel human-computer interaction and automated recognition of large sets of gestures, such as those used for sign language. For most of these applications, it is important to build mobile and self-contained applications that run without the need for frequent communication with additional services on a back-end server. We present in this paper a data glove prototype, based on multiple small Inertial Measurement Units (IMUs), with a glove-embedded classifier for the french sign language. In an extensive set of experiments with 57 participants, our system was tested by repeatedly fingerspelling the French Sign Language (LSF) alphabet. Results show that our system is capable of detecting the LSF alphabet with a mean accuracy score of 92% and an F1 score of 91%, with all detections performed on the glove within 63 milliseconds.
Mummadi C, Kasireddy S, Peter Leo F, Scholl P, Verma K, Van Laerhoven K
Real-time embedded recognition of sign language alphabet fingerspelling in an IMU-based glove
2017 ACM International Conference Proceeding Series, volume: Part F1319
» show abstract« hide abstract
AbstractCopyright © 2017 Association for Computing Machinery. Data gloves have numerous applications, including enabling novel human-computer interaction and automated recognition of large sets of gestures, such as those used for sign language. For most of these applications, it is important to build mobile and self-contained applications that run without the need for frequent communication with additional services on a back-end server. We present in this paper a data glove prototype, based on multiple small Inertial Measurement Units (IMUs), with a glove-embedded classifier for the french sign language. In an extensive set of experiments with 57 participants, our system was tested by repeatedly fingerspelling the French Sign Language (LSF) alphabet. Results show that our system is capable of detecting the LSF alphabet with a mean accuracy score of 92% and an F1 score of 91%, with all detections performed on the glove within 63 milliseconds.
J. Peter,, R. Sandkamp,, L. Minkova,, L. Schumacher,, C. Kaller,, Ahmed Abdulkadir,, S. Kloeppel
Real-world navigation in amnestic mild cognitive impairment - The relation to visuospatial memory and volume of hippocampal subregions
2017 Neuropsychologia, volume: 109, pages: 86 - 94

Download file
Fallmann Jorg, Will Sebastian, Engelhardt Jan, Gruning Bjorn, Backofen Rolf, Stadler Peter
Recent advances in RNA folding
2017 J Biotechnol, volume: 261, pages: 97 - 104
» show abstract« hide abstract
AbstractIn the realm of nucleic acid structures, secondary structure forms a conceptually important intermediate level of description and explains the dominating part of the free energy of structure formation. Secondary structures are well conserved over evolutionary time-scales and for many classes of RNAs evolve slower than the underlying primary sequences. Given the close link between structure and function, secondary structure is routinely used as a basis to explain experimental findings. Recent technological advances, finally, have made it possible to assay secondary structure directly using high throughput methods. From a computational biology point of view, secondary structures have a special role because they can be computed efficiently using exact dynamic programming algorithms. In this contribution we provide a short overview of RNA folding algorithms, recent additions and variations and address methods to align, compare, and cluster RNA structures, followed by a tabular summary of the most important software suites in the fields.
Hoenicke, Jochen, Podelski, Andreas
Reducing Livenes to safety in first-order logic
In: PACM: Programming Languages
2017, ACM,
» show abstract« hide abstract
AbstractWe develop a new technique for verifying temporal properties of infinite-state (distributed) systems. The main idea is to reduce the temporal verification problem to the problem of verifying the safety of infinite-state systems expressed in first-order logic. This allows to leverage existing techniques for safety verification to verify temporal properties of interesting distributed protocols, including some that have not been mechanically verified before. We model infinite-state systems using first-order logic, and use first-order temporal logic (FO-LTL) to specify temporal properties. This general formalism allows to naturally model distributed systems, while supporting both unbounded-parallelism (where the system is allowed to dynamically create processes), and infinite-state per process. The traditional approach for verifying temporal properties of infinite-state systems employs well-founded relations (e.g. using linear arithmetic ranking functions). In contrast, our approach is based the idea of fair cycle detection. In finite-state systems, temporal verification can always be reduced to fair cycle detection (a system contains a fair cycle if it revisits a state after satisfying all fairness constraints). However, with both infinitely many states and infinitely many fairness constraints, a straightforward reduction to fair cycle detection is unsound. To regain soundness, we augment the infinite-state transition system by a dynamically computed finite set, that exploits the locality of transitions. This set lets us define a form of fair cycle detection that is sound in the presence of both infinitely many states, and infinitely many fairness constraints. Our approach allows a new style of temporal verification that does not explicitly involve ranking functions. This fits well with pure first-order verification which does not explicitly reason about numerical values. In particular, it can be used with effectively propositional first-order logic (EPR), in which case checking verification conditions is decidable. We applied our technique to verify temporal properties of several interesting protocols. To the best of our knowledge, we have obtained the first mechanized liveness proof for both TLB Shootdown, and Stoppable Paxos.
Klein A, Falkner S, Mansur N, Hutter F
RoBO: A Flexible and Robust Bayesian Optimization Framework in Python
2017 NIPS 2017 Bayesian Optimization Workshop
Loshchilov I, Hutter F
SGDR: Stochastic Gradient Descent with Warm Restarts
2017 International Conference on Learning Representations (ICLR) 2017 Conference Track
Y. He,, W. Chiu,, Margret Keuper,, M. Fritz
STD2P: RGBD Semantic Segmentation Using Spatio-Temporal Data Driven Pooling
2017

Download file
Lindauer M, Hoos H, Hutter F, Leyton-Brown K
Selection and Configuration of Parallel Portfolios
In: Handbook of Parallel Constraint Reasoning
2017, Springer,
Naseer T., Leivas Oliveira G, Brox T., Burgard W.
Semantics-aware Visual Localization under Challenging Perceptual Conditions
2017 IEEE International Conference on Robotics and Automation (ICRA),

Download file as PDF
Tobias Seufert, Christoph Scholl
Sequential Verification Using Reverse PDR
2017 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
» show abstract« hide abstract
AbstractIn the last few years IC3 resp. PDR made a great stir as a SAT-based hardware verification approach without needing to unroll the transition relation as in Bounded Model Checking (BMC). Motivated by different strengths of forward and backward traversal observed in BDD based model checking, we consider Reverse PDR which starts its analysis with the initial states instead of the unsafe states as in original PDR. We show great benefits of Reverse PDR both by a theoretical and an experimental analysis. Finally, we profit from parallelism offered by modern multi-core processors and use a portfolio approach combining the advantages of Reverse and original PDR.
Elsken Thomas, Metzen Jan, Hutter Frank
Simple And Efficient Architecture Search for Convolutional Neural Networks
2017 NIPS Workshop on Meta-Learning
Meurisch C, Naeem U, Scholl P, Azam M, Günther S, Baumann P, Réhman S, Mühlhäuser M
Smartguidance’17:2nd workshop on intelligent personal support of human behavior
2017 UbiComp/ISWC 2017 - Adjunct Proceedings of the 2017 ACM International Joint Conference on Pervasive and Ubiquitous Computing and Proceedings of the 2017 ACM International Symposium on Wearable Computers
» show abstract« hide abstract
AbstractCopyright © 2017 ACM. In today’s fast-paced environment, humans are faced with various problems such as information overload, stress, health and social issues. So-called anticipatory systems promise to approach these issues through personal guidance or support within a user’s daily and professional life. The Second Workshop on Intelligent Personal Support of Human Behavior (SmartGuidance’17) aims to build on the success of the previous workshop (namely Smarticipation) organized in conjunction with UbiComp 2016, to continue discussing the latest research outcomes of anticipatory mobile systems. We invite the submission of papers within this emerging, interdisciplinary research field of anticipatory mobile computing that focuses on understanding, design, and development of such ubiquitous systems. We also welcome contributions that investigate human behaviors, underlying recognition and prediction models; conduct field studies; as well as propose novel HCI techniques to provide personal support. All workshop contributions will be published in supplemental proceedings of the UbiComp 2017 conference and included in the ACM Digital Library.
Meurisch C, Naeem U, Scholl P, Azam M, Günther S, Baumann P, Réhman S, Mühlhäuser M
Smartguidance’17:2nd workshop on intelligent personal support of human behavior
2017 UbiComp/ISWC 2017 - Adjunct Proceedings of the 2017 ACM International Joint Conference on Pervasive and Ubiquitous Computing and Proceedings of the 2017 ACM International Symposium on Wearable Computers
» show abstract« hide abstract
AbstractCopyright © 2017 ACM. In today’s fast-paced environment, humans are faced with various problems such as information overload, stress, health and social issues. So-called anticipatory systems promise to approach these issues through personal guidance or support within a user’s daily and professional life. The Second Workshop on Intelligent Personal Support of Human Behavior (SmartGuidance’17) aims to build on the success of the previous workshop (namely Smarticipation) organized in conjunction with UbiComp 2016, to continue discussing the latest research outcomes of anticipatory mobile systems. We invite the submission of papers within this emerging, interdisciplinary research field of anticipatory mobile computing that focuses on understanding, design, and development of such ubiquitous systems. We also welcome contributions that investigate human behaviors, underlying recognition and prediction models; conduct field studies; as well as propose novel HCI techniques to provide personal support. All workshop contributions will be published in supplemental proceedings of the UbiComp 2017 conference and included in the ACM Digital Library.
Jonas Uhrig,, N. Schneider,, L. Schneider,, U. Franke,, Thomas Brox,, A. Geiger
Sparsity Invariant CNNs
2017

Download file
Robert Bensch,, N. Scherf,, J. Huisken,, Thomas Brox,, Olaf Ronneberger
Spatiotemporal Deformable Prototypes for Motion Anomaly Detection
2017 Int J Comput Vision, volume: 122, issue: 3, pages: 502 - 523

Download file
Michael Kochte, Sauer M, Laura Rodriguez Gomez, Raiola P, Becker B, Hans-Joachim Wunderlich
Specification and verification of security in reconfigurable scan networks
2017 IEEE European Test Symposium
Reimann Viktoria, Alkhnbashi Omer, Saunders Sita, Scholz Ingeborg, Hein Stephanie, Backofen Rolf, Hess Wolfgang
Structural constraints and enzymatic promiscuity in the Cas6-dependent generation of crRNAs
2017 Nucleic Acids Res, volume: 45, issue: 2, pages: 915 - 925
» show abstract« hide abstract
AbstractA hallmark of defense mechanisms based on clustered regularly interspaced short palindromic repeats (CRISPR) and associated sequences (Cas) are the crRNAs that guide these complexes in the destruction of invading DNA or RNA. Three separate CRISPR-Cas systems exist in the cyanobacterium Synechocystis sp. PCC 6803. Based on genetic and transcriptomic evidence, two associated endoribonucleases, Cas6-1 and Cas6-2a, were postulated to be involved in crRNA maturation from CRISPR1 or CRISPR2, respectively. Here, we report a promiscuity of both enzymes to process in vitro not only their cognate transcripts, but also the respective non-cognate precursors, whereas they are specific in vivo Moreover, while most of the repeats serving as substrates were cleaved in vitro, some were not. RNA structure predictions suggested that the context sequence surrounding a repeat can interfere with its stable folding. Indeed, structure accuracy calculations of the hairpin motifs within the repeat sequences explained the majority of analyzed cleavage reactions, making this a good measure for predicting successful cleavage events. We conclude that the cleavage of CRISPR1 and CRISPR2 repeat instances requires a stable formation of the characteristic hairpin motif, which is similar between the two types of repeats. The influence of surrounding sequences might partially explain variations in crRNA abundances and should be considered when designing artificial CRISPR arrays.
Castano-Candamil Sebastian, Tangermann Michael
Subspace Decomposition in the Frequency Domain
2017 Proceedings of the 7th Graz Brain-Computer Interface Conference (GBCIC 2017), Verlag der Technischen Universität Graz, pages: 64 - 69
Schindelhauer C, Reindl L, Kumberg T, Schink M
T-ROME: A Simple and Energy Efficient Tree Routing Protocol for Low-Power Wake-up Receivers
, 2017
Schindelhauer C, Kumberg T, Reindl L, Schink M
T-ROME: A simple and energy efficient tree routing protocol for low-power wake-up receivers
2017 Ad Hoc Netw, issue: 59, pages: 97 - 115
Hutter F, Lindauer M, Balint A, Bayless S, Hoos H, Leyton-Brown K
The Configurable SAT Solver Challenge (CSSC)
2017 Artificial Intelligence Journal (AIJ), volume: 243, pages: 1 - 25
Gruning Bjorn, Fallmann Jorg, Yusuf Dilmurat, Will Sebastian, Erxleben Anika, Eggenhofer Florian, Houwaart Torsten, Batut Berenice, Videm Pavankumar, Bagnacani Andrea, Wolfien Markus, Lott Steffen, Hoogstrate Youri, Hess Wolfgang, Wolkenhauer Olaf, Hoffmann Steve, Akalin Altuna, Ohler Uwe, Stadler Peter, Backofen Rolf
The RNA workbench: best practices for RNA and high-throughput sequencing bioinformatics in Galaxy
2017 Nucleic Acids Res, volume: 45, issue: W1, pages: W560 - W566
» show abstract« hide abstract
AbstractRNA-based regulation has become a major research topic in molecular biology. The analysis of epigenetic and expression data is therefore incomplete if RNA-based regulation is not taken into account. Thus, it is increasingly important but not yet standard to combine RNA-centric data and analysis tools with other types of experimental data such as RNA-seq or ChIP-seq. Here, we present the RNA workbench, a comprehensive set of analysis tools and consolidated workflows that enable the researcher to combine these two worlds. Based on the Galaxy framework the workbench guarantees simple access, easy extension, flexible adaption to personal and security needs, and sophisticated analyses that are independent of command-line knowledge. Currently, it includes more than 50 bioinformatics tools that are dedicated to different research areas of RNA biology including RNA structure analysis, RNA alignment, RNA annotation, RNA-protein interaction, ribosome profiling, RNA-seq analysis and RNA target prediction. The workbench is developed and maintained by experts in RNA bioinformatics and the Galaxy framework. Together with the growing community evolving around this workbench, we are committed to keep the workbench up-to-date for future standards and needs, providing researchers with a reliable and robust framework for RNA data analysis. AVAILABILITY: The RNA workbench is available at https://github.com/bgruening/galaxy-rna-workbench.
Greff K, Klein A, Chovanec M, Hutter F, Schmidhuber J
The Sacred Infrastructure for Computational Research
2017 Proceedings of the 15th Python in Science Conference (SciPy 2017)
Tobias Schubert, Benjamin Völker, Marc Pfeifer, Bernd Becker
The Smart MiniFab: An Industrial IoT Demonstrator Anywhere at Any Time
2017 Smart Education and e-Learning 2017, Vilamoura/Portugal, KES International Springer International Publishing, pages: 253 - 262
Wilson James, Moriconi Riccardo, Hutter Frank, Deisenroth Marc
The reparameterization trick for acquisition functions
2017 Proceedings of BayesOpt 2017
Schellenberg, D., Kaiser, A.
The sex/gender distinction: Beyond F and M., in: APA Handbook of the Psychology of Women, Eds: Cheryl B. Travis, Jacquelyn W. White, Alexandra Rutherford, Wendi S. Williams.
2017 American Psychological Association, pages: 165 - 187
Keren Censor-Hillel, Mohsen Ghaffari, George Giakkoupis, Bernhard Haeupler, Fabian Kuhn
Tight Bounds on Vertex Connectivity Under Sampling
2017 Acm T Algorithms, volume: 13, issue: 2, pages: 19:1 - 19:26
» show abstract« hide abstract
AbstractA fundamental result by Karger [10] states that for any λ-edge-connected graph with n nodes, independently sampling each edge with probability p = Ω(log (n)/λ) results in a graph that has edge connectivity Ω(λp), with high probability. This article proves the analogous result for vertex connectivity, when either vertices or edges are sampled. We show that for any k-vertex-connected graph G with n nodes, if each node is independently sampled with probability p=Ω(&sqrt;log(n)/k), then the subgraph induced by the sampled nodes has vertex connectivity Ω(kp2), with high probability. If edges are sampled with probability p = Ω(log (n)/k), then the sampled subgraph has vertex connectivity Ω(kp), with high probability. Both bounds are existentially optimal.
Meinel Andreas, Lotte Fabien, Tangermann Michael
Tikhonov Regularization Enhances EEG-Based Spatial Filtering For Single-Trial Regression
2017 Graz, Austria Proceedings of the 7th Graz Brain-Computer Interface Conference 2017, Verlag der Technischen Universität Graz, pages: 308 - 313
Gabriel Leivas Oliveira,, N. Radwan,, W. Burgard,, Thomas Brox
Topometric Localization with Deep Learning
2017

Download file
Jan Burchard, Ange-Salomé Messeng Ekossono, Jan Horáček, Maël Gay, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia Polian
Towards Mixed Structural-Functional Models for Algebraic Fault Attacks on Ciphers
2017 RESCUE Workshop on Reliability, Security and Quality at ETS 2017
Jan Burchard, Ange-Salomé Messeng Ekossono, Jan Horáček, Maël Gay, Bernd Becker, Tobias Schubert, Martin Kreuzer, Ilia Polian
Towards Mixed Structural-Functional Models for Algebraic Fault Attacks on Ciphers
2017 International Verification and Security Workshop (IVSW) 2017
Haussmann E
Towards Precise and Convenient Semantic Search on Text and Knowledge Bases
2017
» show abstract« hide abstract
AbstractIn this dissertation, we consider the problem of making semantic search on text and knowledge bases more precise and convenient. In a nutshell, semantic search is search with meaning . To this respect, text and knowledge bases have different advantages and disadvantages. Large amounts of text are easily available on the web, and they contain a wealth of information in natural language. However, text represents information in an unstructured form. It follows no pre-defined schema, and without further processing, a machine can understand its meaning only on a superficial level. Knowledge bases, on the other hand, contain structured information in the form of subject predicate object triples. The meaning of triples is well defined, and triples can be retrieved precisely via a query language. However, ormulating queries in this language is inconvenient and compared to text only a small fraction of information is currently available in knowledge bases. In this document, we summarize our contributions on making semantic search on text and knowledge bases more precise and convenient. For knowledge bases, we introduce an approach to answer natural language questions. A user can pose questions conveniently in natural language and ask, for example, who is the ceo of apple? , instead of having to learn and use a specific query language. Our approach applies learning-to-rank strategies and improved the state of the art on two widely used benchmarks at the time of publication. For knowledge bases, we also describe a novel approach to compute relevance scores for triples from type-like relations like profession and nationality . For example, on a large knowledge base, a query for american actors can return a list of more than 60 thousand actors in no particular order. Relevance scores allow to sort this list so that, e.g., frequent lead actors appear before those who only had single cameo roles. In a benchmark that we generated via crowdsourcing, we show that our rankings are closer to human judgments than approaches from the literature. Finally, for text, we introduce a novel natural language processing technique that identifies which words in a sentence “semantically belong together”. For example, in the sentence Bill Gates, founder of Microsoft, and Jeff Bezos, founder of Amazon, are among the wealthiest persons in the world , the words Bill Gates ,founder , and Amazon do not belong together, but the words Bill Gates ,founder, and Microsoft do. We show that when query keywords are required to belong together in order to match, search results become more precise. Given the characteristics of text and knowledge bases outlined above, it is promising to consider a search that combines both. For example, for the query CEOs of U.S. companies who advocate cryptocurrencies , a list of CEOs of U.S. companies can be retrieved from a knowledge base. The information who is advocating cryptocurrencies is rather specific and changes frequently. It is, therefore, better found in full text. As part of this thesis, we describe how a combined search could be achieved and present and evaluate a fully func- tional prototype. All of our approaches are accompanied by an extensive evaluation which show their practicability and, where available, compare them to established approaches from the literature.
Gabriel Kalweit, Joschka Boedecker
Uncertainty-driven Imagination for Continuous Deep Reinforcement Learning
2017 Conference on Robot Learning

Download file as PDF
Bernd Becker, Christoph Scholl, Ralf Wimmer
Verification of Incomplete Designs
In: Formal System Verification - State of the Art and Future Trends
2017, Springer, Rolf Drechsler, pages: 37 - 72, Rolf Drechsler, ISBN: 978-3-319-57683-1
» show abstract« hide abstract
AbstractWe consider the verification of digital systems which are incomplete in the sense that for some modules only their interfaces (i.e., the signals entering and leaving the module) are known, but not their implementations. For such designs, we study realizability (``Is it possible to implement the missing modules such that the complete design has certain properties?'') and validity (``Does a property hold no matter how the missing parts are implemented?'').
Bernd Becker, Christoph Scholl, Ralf Wimmer
Verification of Incomplete Designs
In: Formal System Verification State-of the-Art and Future Trends
2017, Springer International Publishing, Rolf Drechsler, pages: 37 - 72, Rolf Drechsler, ISBN: 978-3-319-57683-1
» show abstract« hide abstract
AbstractWe consider the verification of digital systems which are incomplete in the sense that for some modules only their interfaces (i.e., the signals entering and leaving the module) are known, but not their implementations. For such designs, we study realizability ("Is it possible to implement the missing modules such that the complete design has certain properties?") and validity ("Does a property hold no matter how the missing parts are implemented?").
Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, Boris Wirtz
Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization
Sci Comput Program, issue: 148, pages: 123 - 160, 2017
Lindauer M, Kotthoff L
What can we learn from algorithm selection data? (Breakout Session Report)
2017 Dagstuhl Reports, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, volume: 6, pages: 64 - 65
Huggins Jane, Guger Christoph, Ziat Mounia, Zander Thorsten, Taylor Denise, Tangermann Michael, Soria-Frisch Aureli, Simeral John, Scherer Reinhold, Rupp Rüdiger, Ruffini Giulio, Robinson Douglas, Ramsey Nick, Nijholt Anton, Müller-Putz Gernot, McFarland Dennis, Mattia Donatella, Lance Brent, Kindermans Pieter-Jan, Iturrate Inąaki, Herff Christian, Gupta Disha, Do An, Collinger Jennifer, Chavarriaga Ricardo, Chase Steven, Bleichner Martin, Batista Aaron, Anderson Charles, Aarnoutse Erik
Workshops of the Sixth International Brain-Computer Interface Meeting: brain-computer interfaces past, present, and future
2017 Brain-Computer Interfaces, volume: 4, issue: 1-2, pages: 3 - 36
Prasse Daniela, Förstner Konrad, Jäger Dominik, Backofen Rolf, Schmitz Ruth
sRNA154 a newly identified regulator of nitrogen fixation in Methanosarcina mazei strain Go1
2017 RNA Biol, volume: 13, issue: 11, pages: 1544 - 58
» show abstract« hide abstract
AbstractTrans-encoded sRNA154 is exclusively expressed under nitrogen (N)-deficiency in Methanosarcina mazei strain Go1. The sRNA154 deletion strain showed a significant decrease in growth under N-limitation, pointing toward a regulatory role of sRNA154 in N-metabolism. Aiming to elucidate its regulatory function we characterized sRNA154 by means of biochemical and genetic approaches. 24 homologs of sRNA154 were identified in recently reported draft genomes of Methanosarcina strains, demonstrating high conservation in sequence and predicted secondary structure with two highly conserved single stranded loops. Transcriptome studies of sRNA154 deletion mutants by an RNA-seq approach uncovered nifH- and nrpA-mRNA, encoding the alpha-subunit of nitrogenase and the transcriptional activator of the nitrogen fixation (nif)-operon, as potential targets besides other components of the N-metabolism. Furthermore, results obtained from stability, complementation and western blot analysis, as well as in silico target predictions combined with electrophoretic mobility shift-assays, argue for a stabilizing effect of sRNA154 on the polycistronic nif-mRNA and nrpA-mRNA by binding with both loops. Further identified N-related targets were studied, which demonstrates that translation initiation of glnA2-mRNA, encoding glutamine synthetase2, appears to be affected by sRNA154 masking the ribosome binding site, whereas glnA1-mRNA appears to be stabilized by sRNA154. Overall, we propose that sRNA154 has a crucial regulatory role in N-metabolism in M. mazei by stabilizing the polycistronic mRNA encoding nitrogenase and glnA1-mRNA, as well as allowing a feed forward regulation of nif-gene expression by stabilizing nrpA-mRNA. Consequently, sRNA154 represents the first archaeal sRNA, for which a positive posttranscriptional regulation is demonstrated as well as inhibition of translation initiation.

2016

back to the year overview

Marc Pfeifer, Tobias Schubert, Bernd Becker
PackSens: A Condition and Transport Monitoring System Based on an Embedded Sensor Platform
2016 7th EAI International Conference on Sensor Systems and Software Proceedings of the 7th EAI International Conference on Sensor Systems and Software, pages: 81 - 92
» show abstract« hide abstract
AbstractAs a consequence of the growing globalization, transports which need a safe handling are increasing. Therefore, this paper introduces an innovative transport and condition monitoring system based on a mobile embedded sensor platform. The platform is equipped with a variety of sensors needed to extensively monitor a transport and can be attached directly to the transported good. The included microcontroller processes all relevant data served by the sensors in a very power efficient manner. Furthermore, it provides possible violations of previously given thresholds through a standardized Near Field Communication (NFC) interface to the user. Since falls are one major cause of damages while transportation, the presented system is the first one that not only detects every fall but also analyses the fall height and other parameters related to the fall event in real-time on the platform. The whole system was tested in different experiments where all critical situations and in particular all fall situations have been detected correctly.
Camilo Gordillo, Barbara Frank, Istvan Ulbert, Oliver Paul, Patrick Ruther, Wolfram Burgard
Automatic Channel Selection in Neural Microprobes: A Combinatorial Multi-Armed Bandit Approach
2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2016) Proc. of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)
» show abstract« hide abstract
AbstractState-of-the-art neural microprobes contain hundreds of electrodes within a single shaft. Due to hardware and wiring restrictions, it is usually only possible to measure a small subset of the available electrodes simultaneously. The selection of the best channels is typically performed offline either manually or automatically. However, having a fixed selection for long-term observation does not allow the system to react to changes in the neural activity, and may therefore lead to the loss of important information. In this paper, we formulate the process of autonomously selecting the best subset of electrodes as a combinatorial multi-armed bandit problem with non-stationary rewards, thus allowing the probe to adapt its selection policies online. In order to minimize exploratory actions of the probe, we furthermore take advantage of the existing dependencies between neighboring channels. Our approach is an adaptation of the discounted upper confidence bounds (D-UCB) algorithm, and identifies the electrodes providing the largest amount of non-redundant information. To the best of our knowledge, this is the first online approach for the problem of electrode selection. In extensive experiments, we demonstrate that our solution is not only able to converge towards an average optimal selection policy, but it is also able to react to changes in the neural activity or to damages of the recording electrodes.
Benjamin Völker, Tobias Schubert, Bernd Becker
iHouse: A Voice-Controlled, Centralized, Retrospective Smart Home
2016 7th EAI International Conference on Sensor Systems and Software
» show abstract« hide abstract
AbstractSpeech recognition in smart home systems has become pop- ular in both, research and consumer areas. This paper introduces an in- novative concept for a modular, customizable, and voice-controlled smart home system. The system combines the advantages of distributed and centralized processing to enable a secure as well as highly modular plat- form and allows to add existing non-smart components retrospectively into the smart environment. To interact with the system in the most com- fortable way - and in particular without additional devices like smart- phones - voice-controlling was added as the means of choice. The task of speech recognition is partitioned into decentral Wake-Up-Word (WUW) recognition and central continuous speech recognition to enable flexibil- ity while maintaining security. This is achieved utilizing a novel WUW algorithm suitable to be executed on small microcontrollers which uses Mel Frequency Cepstral Coefficients as well as Dynamic Time Warping. A high rejection rate up to 99.93% was achieved, justifying the use of the algorithm as a voice trigger in the developed smart home system.
Matthias Sauer, Jie Jiang, Sven Reimer, Kohei Miyase, Xiaoqing Wen, Bernd Becker, Ilia Polian
On Optimal Power-aware Path Sensitization
2016 2016 25nd IEEE Asian Test Symposium (ATS)
Mathias Soeken, Pascal Raiola, Baruch Sterin, Bernd Becker, Giovanni De Micheli, Matthias Sauer
SAT-based Combinational and Sequential Dependency Computation
2016 Haifa Verification Conference (HVC)
Kuhner A, Schubert T, Cenciarini M, Maurer C, Burgard W
A Probabilistic Approach Based on Random Forests to Estimating Similarity of Human Motion in the Context of Parkinson’s Disease
2016 IEEE/RSJ International Conference on Intelligent Robots and Systems, Daejeon 2016 Proc. of IEEE/RSJ International Conference on Intelligent Robots and Systems
» show abstract« hide abstract
AbstractThe objective characterization of human motion is required in a variety of fields including competitive sports, rehabilitation and the detection of motor deficits. Nowadays, typically human experts evaluate the motor behavior. These evaluations are based on their individual experience which leads to a low inter- and intra-expert reliability. Standardized tests improve on the reliability but are still prone to subjective ratings and require human expert knowledge. This paper presents a novel method to characterize the motor state of Parkinson patients using full body motion capturing data based on a combination of multiple metrics. Our approach merges various metrics with a Random Forest and uses a probabilistic formulation to compute a one-dimensional measure for the performed motion. We present an application of our approach to the problem of relating subject motion to different classes like healthy subjects and Parkinson disease patients with deep brain stimulation switched on or off. In the experimental session we show that our measure leads to high classification rates and high entropy values for real-world data. Besides, we show that our method discriminates between Parkinson’s subjects (with and without stimulation) and healthy persons as good as the Unified Parkinson’s Disease Rating Scale (UPDRS).
Burget F, Bennewitz M, Burgard W
BI2RRT*: An Efficient Sampling-Based Path Planning Framework for Task-Constrained Mobile Manipulation
2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) IEEE, pages: 3714 - 3721
» show abstract« hide abstract
AbstractMobile manipulators installed in warehouses and factories for conveying goods between working stations need to meet the requirements of time-critical workflows. More- over, the systems are expected to deal with changing tasks, cluttered environments and constraints imposed by the goods to be delivered. In this paper, we present a novel planning framework for generating asymptotically optimal paths for mobile manipulators subject to task constraints. Our approach introduces the Bidirectional Informed RRT* (BI 2 RRT*) that extends the Informed RRT* [1] towards bidirectional search and satisfaction of end-effector task constraints. In various experiments, we demonstrate the efficiency of BI 2 RRT* for both unconstrained and constrained mobile manipulation planning problems. As the results show, our planning framework finds better solutions than Informed RRT* and Bidirectional RRT* in less planning time.
Sebastian Volkmann, Linus Feiten, Christian Zimmermann, Sebastian Sester, Laura Wehle, Bernd Becker
Digitale Tarnkappe: Anonymisierung in Videoaufnahmen
2016 INFORMATIK 2016 Gesellschaft für Informatik (GI), Heinrich C. Mayr, Martin Pinzger, volume: P-252, pages: 413 - 426
» show abstract« hide abstract
AbstractVideoüberwachung ist heute allgegenwärtig. Sie dient dazu, Delikte im Nachhinein aufzuklären, zur Echtzeit-Überwachung oder zur Abschreckung. Darüber hinaus gibt es aber auch wirtschaftliche Interessen für eine Videoüberwachung und automatische Erfassung von Personen - z.B. zur Erstellung von Kundenprofilen und somit zur Analyse von Kaufverhalten. Dem gegenüber stehen Rechtsansprüche sowie ethische und gesellschaftliche Grundnormen, etwa dass Menschen nicht unter Generalverdacht gestellt oder ohne Zustimmung aufgezeichnet werden dürfen. In dieser Arbeit wird ein technischer Lösungsansatz behandelt, der eine flexible Handhabung der Videoüberwachung erlaubt. Es werden in diesem Zusammenhang neben der technischen Umsetzung auch ökonomische, ethische und juristische Fragen betrachtet. Der Lösungsansatz besteht darin, Personen auf Videoaufnahmen durch ein kryptographisches Verfahren unkenntlich zu machen, noch bevor die Aufnahmen die Kamera-Elektronik verlassen. Nur mittels eines geheimen kryptographischen Schlüssels können einzelne Zeit- und Bildbereiche einer Aufnahme wieder deanonymisiert werden, wodurch rechtlichen wie ethischen Bedenken Rechnung getragen werden kann. In kommerziellen Szenarien erlaubt es diese digitale Tarnkappe, dass Kunden z.B. im Rahmen eines Prämien-Programms freiwillig auf Anonymisierung verzichten. Während in der Literatur der Informatik bereits seit längerem Technologien für solche System beschrieben werden, werden in dieser Arbeit Wege gezeigt, wie dessen Einbettung in die Gesellschaft wirklich realisiert werden könnte.

Download file
Tobias Schubert, Isabel Dahlhausen
Pilotkurs Schlüsseltechnologien der vernetzten Produktion – Wissenschaftliche Weiterbildung für Ingenieure und Ingenieurinnen, Fach‐ & Führungskräfte im Bereich Industrie 4.0
2016 DGWF-Jahrestagung 2016, pages: 142 - 143
Jan Burchard, Tobias Schubert, Bernd Becker
Distributed Parallel #SAT Solving
2016 IEEE Cluster 2016
» show abstract« hide abstract
AbstractThe #SAT problem, that is counting the number of solutions of a propositional formula, extends the well- known SAT problem into the realm of probabilistic reasoning. However, the higher computational complexity and lack of fast solvers still limits its applicability for real world problems. In this work we present our distributed parallel #SAT solver dCountAntom which utilizes both local, shared-memory paral- lelism as well as distributed (cluster computing) parallelism. Although highly parallel solvers are known in SAT solving, such techniques have never been applied to the #SAT problem. Furthermore we introduce a solve progress indicator which helps the user to assess whether the presented problem is likely solvable within a reasonable time. Our analysis shows a high accuracy of the estimated progress. Our experiments with up to 256 CPU cores working in parallel yield large speedups across different benchmarks derived from real world problems: With the maximum number of available cores dCountAntom solved problems on average 141 times faster than a single core implementation.
Schätzle A, Przyjaciel-Zablocki M, Skilevic, S, , Lausen G
S2RDF: RDF Querying with SPARQL on Spark
2016 42nd International Conference on Very Large Data Bases , volume: 9, issue: 10
Mohamad Ahmadi, Fabian Kuhn
Multi-Message Broadcast in Dynamic Radio Networks
2016 12th Int. Symp. on Algorithms and Experiments for Wireless Sensor Networks (ALGOSENSORS), Aarhus, Denmark
» show abstract« hide abstract
AbstractWe continue the recent line of research studying information dissemination problems in adversarial dynamic radio networks. We give two generic algorithms which allow to transform generalized version of single-message broadcast algorithms into multi-message broadcast algorithms. Based on these generic algorithms, we obtain multi-message broadcast algorithms for dynamic radio networks for a number of different dynamic network settings. For one of the modeling assumptions, our algorithms are complemented by a lower bound which shows that the upper bound is close to optimal.
Jeremy T. Fineman, Seth Gilbert, Fabian Kuhn, Calvin Newport
Contention Resolution on a Fading Channel
2016 2016 ACM Symposium on Principles of Distributed Computing (PODC)
» show abstract« hide abstract
AbstractIn this paper, we study upper and lower bounds for contention resolution on a single hop fading channel; i.e., a channel where receive behavior is determined by a signal to interference and noise ratio (SINR) equation. The best known previous solution solves the problem in this setting in O(log2 n log log n) rounds, with high probability in the system size n. We describe and analyze an algorithm that solves the problem in O(log n + log R) rounds, where R is the ratio between the longest and shortest link, and is a value upper bounded by a polynomial in n for most feasible deployments. We complement this result with an Ω(log n) lower bound that proves the bound tight for reasonable R. We note that in the classical radio network model (which does not include signal fading), high probability contention resolution requires Ω(log 2 n) rounds. Our algorithm, therefore, affirms the conjecture that the spectrum reuse enabled by fading should allow distributed algorithms to achieve a significant improvement on this log2 n speed limit. In addition, we argue that the new techniques required to prove our upper and lower bounds are of general use for analyzing other distributed algorithms in this increasingly well-studied fading channel setting.
Dan Hefetz, Fabian Kuhn, Yannic Maus, Angelika Steger
Polynomial Lower Bound for Distributed Graph Coloring in a Weak LOCAL Model
2016 30th International Symposium on DIStributed Computing (DISC), Paris, September 26-30, 2016
» show abstract« hide abstract
AbstractWe show an Omega(\Delta^{\frac{1}{3}-\frac{\eta}{3}}) lower bound on the runtime of any deterministic distributed O(\Delta^{1+\eta})-graph coloring algorithm in a weak variant of the LOCAL model. In particular, given a network graph G=(V,E), in the weak LOCAL model nodes communicate in synchronous rounds and they can use unbounded local computation. The nodes have no identifiers, but instead, the computation starts with an initial valid vertex coloring. A node can broadcast a single message of unbounded size to its neighbors and receives the set of messages sent to it by its neighbors. The proof uses neighborhood graphs and improves their understanding in general such that it might help towards finding a lower (runtime) bound for distributed graph coloring in the standard LOCAL model.
Fabian Kuhn, Sebastian Daum, Yannic Maus
Rumor Spreading with Bounded In-Degree
2016 23rd Int. Coll. on Structural Information and Communication Complexity (SIROCCO), Helsinki, Finland
» show abstract« hide abstract
AbstractIn the classic gossip-based model of communication for disseminating information in a network, in each time unit, every node u is allowed to contact a single random neighbor v. If u knows the data (rumor) to be disseminated, it disperses it to v (known as PUSH) and if it does not, it requests it from v (known as PULL). While in the classic gossip model, each node is only allowed to contact a single neighbor in each time unit, each node can possibly be contacted by many neighboring nodes. In the present paper, we consider a restricted model where at each node only one incoming request can be served. As long as only a single piece of information needs to be disseminated, this does not make a difference for push requests. It however has a significant effect on pull requests. In the paper, we therefore concentrate on this weaker pull version, which we call 'restricted pull'. We distinguish two versions of the restricted pull protocol depending on whether the request to be served among a set of pull requests at a given node is chosen adversarially or uniformly at random. As a first result, we prove an exponential separation between the two variants. We show that there are instances where if an adversary picks the request to be served, the restricted pull protocol requires a polynomial number of rounds whereas if the winning request is chosen uniformly at random, the restricted pull protocol only requires a polylogarithmic number of rounds to inform the whole network. Further, as the main technical contribution, we show that if the request to be served is chosen randomly, the slowdown of using restricted pull versus using the classic pull protocol can w.h.p. be upper bounded by O(Δ/δlogn), where Δ and δ are the largest and smallest degree of the network.
Bast H, Buchhold B, Haussmann E
Semantic Search on Text and Knowledge Bases
2016
» show abstract« hide abstract
AbstractThis article provides a comprehensive overview of the broad area of semantic search on text and knowledge bases. In a nutshell, semantic search is “search with meaning”. This “meaning” can refer to various parts of the search process: understanding the query (instead of just finding matches of its components in the data), understanding the data (instead of just searching it for such matches), or representing knowledge in a way suitable for meaningful retrieval. Semantic search is studied in a variety of different communities with a variety of different views of the problem. In this survey, we classify this work according to two dimensions: the type of data (text, knowl- edge bases, combinations of these) and the kind of search (keyword, structured, natural language). We consider all nine combinations. The focus is on fundamental techniques, concrete systems, and benchmarks. The survey also considers advanced issues: ranking, indexing, ontology matching and merging, and inference. It also provides a succinct overview of natural language processing techniques that are useful for semantic search: POS tagging, named-entity recognition and disambiguation, sentence parsing, and word vectors. The survey is as self-contained as possible, and should thus also serve as a good tutorial for newcomers to this fascinating and highly topical field.
Mathias Soeken, Pascal Raiola, Baruch Sterin, Matthias Sauer
SAT-based Functional Dependency Computation
2016 International Workshop on Logic & Synthesis
Michael Kochte, Rafal Baranowski, Matthias Sauer, Bernd Becker, Hans-Joachim Wunderlich
Formal Verification of Secure Reconfigurable Scan Network Infrastructure
2016 IEEE European Test Symposium
Michael Kochte, Matthias Sauer, Pascal Raiola, Bernd Becker, Hans-Joachim Wunderlich
SHIVA: Sichere Hardware in der Informationsverarbeitung Formaler Nachweis komplexer Sicherheitseigenschaften in rekonfigurierbarer Infrastruktur
2016 eda Workshop
Andreas Riefert, Riccardo Cantoro, Matthias Sauer, Matteo Sonza Reorda, Bernd Becker
Effective Generation and Evaluation of Diagnostic SBST Programs
2016 IEEE VLSI Test Symposium
Linus Feiten, Matthias Sauer, Bernd Becker
On Metrics to Quantify the Inter-Device Uniqueness of PUFs
2016 TRUDEVICE Workshop, Dresden
» show abstract« hide abstract
AbstractPhysically Unclonable Functions (PUFs) have been an emerging topic in hardware security and trust in recent years, and many different kinds of PUFs have been presented in the literature. An important criterion is always the diversity of PUF responses for different devices, called inter-device uniqueness. A very popular uniqueness metric consists of calculating the pairwise hamming distance between the response bit-strings of all devices, assuming that all response bits are uncorrelated. Such correlations, however, should be regarded when a statement about inter-device uniqueness is made. We therefore propose a novel correlation metric to fulfil this requirement. Furthermore, we show that the hamming distance metric is actually redundant when at the same time the also popular bit-aliasing metric is applied.
Matthias Sauer, Sven Reimer, Daniel Tille, Karsten Scheibler, Dominik Erb, Ulrike Pfannkuchen, Bernd Becker
Clock Cycle Aware Encoding for SAT-based Circuit Initialization
2016 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”
Bast H, Storandt S, Hertel M
Scalable Transfer Patterns
2016 ALENEX
» show abstract« hide abstract
AbstractWe consider the problem of Pareto-optimal route planning in public-transit networks of a whole country, a whole continent, or even the whole world. On such large networks, existing approaches suffer from either a very large space consumption, a very long preprocessing time or slow query processing. Transfer Patterns, a state-of-the-art technique for route planning in transit networks, achieves excellent query times, but the space consumption is large and the preprocessing time is huge. In this paper, we introduce a new scheme for the Transfer Pattern precomputation and query graph construction that reduces both the necessary preprocessing time and space consumption by an order of magnitude and more. Average query times are below 1 ms for local queries, independent of the size of the network, around 30 ms for non-local queries on the complete transit network of Germany, and an estimated 200 ms for a ﬁctitious transit network covering the currently available data of the whole world.
Valeriy Balabanov, Jie-Hong Roland Jiang, Christoph Scholl, Alan Mishchenko, Robert K. Brayton
2QBF: Challenges and Solutions
2016 International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer-Verlag, issue: 9710, pages: 453 - 469
» show abstract« hide abstract
Abstract2QBF is a special form \forall x \exists y. \Phi of the quantified Boolean formula (QBF) restricted to only two quantification layers, where \Phi is a quantifier-free formula. Despite its restricted form, it provides a framework for a wide range of applications, such as artificial intelligence, graph theory, synthesis, etc. In this work, we overview two main 2QBF challenges in terms of solving and certification. We contribute several improvements to existing solving approaches and study how the corresponding approaches affect certification. We further conduct an extensive experimental comparison on both competition and application benchmarks to demonstrate strengths of the proposed methodology.
Çiçek Ö, Abdulkadir A., Lienkamp S., Brox T., Ronneberger O
3D U-Net: Learning Dense Volumetric Segmentation from Sparse Annotation
2016 Medical Image Computing and Computer-Assisted Intervention (MICCAI) LNCS, Springer, volume: 9901, pages: 424 - 432

Download file as PDF
Andreas Riefert, Riccardo Cantoro, Matthias Sauer, Matteo Sonza Reorda, Bernd Becker
A Flexible Framework for the Automatic Generation of SBST Programs
2016 IEEE Transactions on Very Large Scale Integration (VLSI) Systems, volume: 24, issue: 10, pages: 3055 - 3066
Mayer N, Ilg E., Häusser P., Fischer P., Cremers D., Dosovitskiy A., Brox T.
A Large Dataset to Train Convolutional Networks for Disparity, Optical Flow, and Scene Flow Estimation
2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR)

Download file as PDF
Morciniec T, Podelski A
A Logical Approach to Generating Test Plans
2016 CoRR abs/1612.04351, volume: 2016
Lindner Felix
A Model of a Robot’s Will Based on Higher-Order Desires
2016 Proceedings of the IEEE International Symposium on Robot and Human Interactive Communication (RO-MAN 2016)
Scholl Philipp, Van Laerhoven Kristof
A Multi-Media Exchange Format for Time-Series Dataset Curation
2016 UbiComp 2016 Adjunct - Proceedings of the 2016 ACM International Joint Conference on Pervasive and Ubiquitous Computing
» show abstract« hide abstract
AbstractExchanging data as comma-separated values (CSV) is slow, cumbersome and error-prone. Especially for timeseries data, which is common in Activity Recognition, synchronizing several independently recorded sensors is challenging. Adding second level evidence, like video recordings from multiple angles and time-coded annotations, further complicates the matter of curating such data. A possible alternative is to make use of standardized multimedia formats. Sensor data can be encoded in audio format, and time-coded information, like annotations, as subtitles. Video data can be added easily. All this media can be merged into a single container file, which makes the issue of synchronization explicit. The incurred performance overhead by this encoding is shown to be negligible and compression can be applied to optimize storage and transmission overhead.
Scholl Philipp, Van Laerhoven Kristof
A Multi-Media Exchange Format for Time-Series Dataset Curation
2016 UbiComp 2016 Adjunct - Proceedings of the 2016 ACM International Joint Conference on Pervasive and Ubiquitous Computing
» show abstract« hide abstract
AbstractExchanging data as comma-separated values (CSV) is slow, cumbersome and error-prone. Especially for timeseries data, which is common in Activity Recognition, synchronizing several independently recorded sensors is challenging. Adding second level evidence, like video recordings from multiple angles and time-coded annotations, further complicates the matter of curating such data. A possible alternative is to make use of standardized multimedia formats. Sensor data can be encoded in audio format, and time-coded information, like annotations, as subtitles. Video data can be added easily. All this media can be merged into a single container file, which makes the issue of synchronization explicit. The incurred performance overhead by this encoding is shown to be negligible and compression can be applied to optimize storage and transmission overhead.
Do C, Schubert T, Burgard W
A Probabilistic Approach to Liquid Level Detection in Cups Using an RGB-D Camera
2016 Pro. Of the IEEE/RSJ Int. Conf. On Intelligent Robots and Systems (IROS) Pro. Of the IEEE/RSJ Int. Conf. On Intelligent Robots and Systems (IROS) 2016
» show abstract« hide abstract
AbstractRobotic assistants have the potential to greatly improve our quality of life by supporting us in our daily activities. A service robot acting autonomously in an indoor environment is faced with very complex tasks. Consider the problem of pouring a liquid into a cup, the robot should first determine if the cup is empty or partially filled. RGB-D cameras provide noisy depth measurements which depend on the opaqueness and refraction index of the liquid. In this paper, we present a novel probabilistic approach for estimating the fill-level of a liquid in a cup using an RGB-D camera. Our approach does not make any assumptions about the properties of the liquid like its opaqueness or its refraction index. We develop a probabilistic model using features extracted from RGB and depth data. Our experiments demonstrate the robustness of our method and an improvement over the state of the art.
Lindner Felix
A Social Robot’s Knowledge About Territories in Public Space
2016 Proceedings of the 3rd Workshop on Public Space Human-Robot Interaction (PubRob 2016)
Marrett Karl, Wronkiewicz Mark, Tangermann Michael, Lee Adrian
A User-Focused Study of Auditory P300 Brain-Computer Interface Design
2016 Asilomar Conference Center, Pacific Grove, California, USA Proceedings of the 6th International Brain-Computer Interface Meeting: BCI Past, Present, and Future, Verlag der Technischen Universität Graz, pages: 17 - 17
Scholl P, Van Laerhoven K
A multi-media exchange format for time-series dataset curation
2016 UbiComp 2016 Adjunct - Proceedings of the 2016 ACM International Joint Conference on Pervasive and Ubiquitous Computing
» show abstract« hide abstract
Abstract© 2016 ACM. Exchanging data as comma-separated values (CSV) is slow, cumbersome and error-prone. Especially for timeseries data, which is common in Activity Recognition, synchronizing several independently recorded sensors is challenging. Adding second level evidence, like video recordings from multiple angles and time-coded annotations, further complicates the matter of curating such data. A possible alternative is to make use of standardized multimedia formats. Sensor data can be encoded in audio format, and time-coded information, like annotations, as subtitles. Video data can be added easily. All this media can be merged into a single container file, which makes the issue of synchronization explicit. The incurred performance overhead by this encoding is shown to be negligible and compression can be applied to optimize storage and transmission overhead.
Scholl P, Van Laerhoven K
A multi-media exchange format for time-series dataset curation
2016 UbiComp 2016 Adjunct - Proceedings of the 2016 ACM International Joint Conference on Pervasive and Ubiquitous Computing
» show abstract« hide abstract
Abstract© 2016 ACM. Exchanging data as comma-separated values (CSV) is slow, cumbersome and error-prone. Especially for timeseries data, which is common in Activity Recognition, synchronizing several independently recorded sensors is challenging. Adding second level evidence, like video recordings from multiple angles and time-coded annotations, further complicates the matter of curating such data. A possible alternative is to make use of standardized multimedia formats. Sensor data can be encoded in audio format, and time-coded information, like annotations, as subtitles. Video data can be added easily. All this media can be merged into a single container file, which makes the issue of synchronization explicit. The incurred performance overhead by this encoding is shown to be negligible and compression can be applied to optimize storage and transmission overhead.
Musso Mariacristina, Bamdadian Atieh, Denzer Simone, Umarova Roza, Hübner David, Tangermann Michael
A novel BCI based rehabilitation approach for aphasia rehabilitation
2016 Asilomar Conference Center, Pacific Grove, California, USA Proceedings of the 6th International Brain-Computer Interface Meeting: Past, Present, and Future, Verlag der Technischen Universität Graz, pages: 104 - 104
Bischl B, Kerschke P, Kotthoff L, Lindauer M, Malitsky Y, Frechétte A, Hoos H, Hutter F, Leyton-Brown K, Tierney K, Vanschoren J
ASlib: A Benchmark Library for Algorithm Selection
2016 Artificial Intelligence Journal (AIJ), volume: 237, pages: 41 - 58
Geißer Florian, Keller Thomas, Mattmüller Robert
Abstractions for Planning with State-Dependent Action Costs
2016 Proceedings of the 26th International Conference on Automated Planning and Scheduling (ICAPS 2016)
Karsten Scheibler, Dominik Erb, Bernd Becker
Accurate CEGAR-based ATPG in Presence of Unknown Values for Large Industrial Designs
2016 Conf. on Design, Automation and Test in Europe
» show abstract« hide abstract
AbstractUnknown values emerge during the design and test generation process as well as during later test application and system operation. They adversely affect the test quality by reducing the controllability and observability of internal circuit structures -- resulting in a loss of fault coverage. To handle unknown values, conventional test generation algorithms as used in state-of-the-art commercial tools, rely on n-valued algebras. However, n-valued algebras introduce pessimism as soon as X-values reconverge. Consequently, these algorithms fail to compute the accurate result. Therefore, this paper focuses on a new highly incremental CEGAR-based algorithm that overcomes these limitations and hence is completely accurate in presence of unknown values. It relies on a modified SAT-solver tailored to this specific problem. The experimental results for circuits with up to 2.400.000 gates show that this combination allows high accuracy and high scalability at the same time. Compared to a state-of-the-art commercial tool, the fault coverage could be increased significantly. Furthermore, the runtime is reduced remarkably compared to a QBF-based encoding of the problem.
Felix Neubauer, Karsten Scheibler, Bernd Becker, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer
Accurate Dead Code Detection in Embedded C Code by Arithmetic Constraint Solving
2016 First International Workshop on Satisfiability Checking and Symbolic Computation - FETOPEN-CSA SC2 Workshop - Affiliated with SYNASC 2016
» show abstract« hide abstract
AbstractUnreachable code fragments in software, despite not having a negative impact on the functional behavior, can have a bad effect in other areas, such as code optimization or coverage-based code validation and certification. Especially the latter is important in industrial, safety critical environments, where detecting such dead code is a major goal to adjust the coverage of software tests. In the context of embedded systems we focus on C programs which are reactive, control-oriented, and floating-point dominated. Such programs are either automatically generated from Simulink-plus-Stateflow models or hand-written according to coding guidelines. While there are various techniques – e.g. abstract interpretation or Counterexample guided abstraction refinement (CEGAR) – to deal with individual issues of this domain, there is none which can cover all of them. The AVACS transfer project T1 aims at the combination of these techniques in order to provide an accurate and efficient dead code detection. In this paper we present the ideas and goals of the project as well as the current status (including very promising experimental results) and future challenges.
Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, Bernd Becker
Accurate ICP-based Floating-Point Reasoning
2016 Formal Methods in Computer-Aided Design, pages: 177 - 184
» show abstract« hide abstract
AbstractIn scientific and technical software, floating-point arithmetic is often used to approximate arithmetic on physical quantities natively modeled as reals. Checking properties for such programs (e.g. proving unreachability of code fragments) requires accurate reasoning over floating-point arithmetic. Currently, most of the SMT-solvers addressing this problem class rely on bit-blasting. Recently, methods based on reasoning in interval lattices have been lifted from the reals (where they traditionally have been successful) to the floating-point numbers. The approach presented in this paper follows the latter line of interval-based reasoning, but extends it by including bitwise integer operations and cast operations between integer and floating-point arithmetic. Such operations have hitherto been omitted, as they tend to define sets not concisely representable in interval lattices, and were consequently considered the domain of bit-blasting approaches. By adding them to interval-based reasoning, the full range of basic data types and operations of C programs is supported. Furthermore, we propose techniques in order to mitigate the problem of aliasing during interval reasoning. The experimental results confirm the efficacy of the proposed techniques. Our approach outperforms solvers relying on bit-blasting as well as the existing interval-based SMT-solver.
Schilling Christian, Bogomolov Sergiy, Henzinger Thomas, Podelski Andreas, Ruess Jakob
Adaptive moment closure for parameter inference of biochemical reaction networks
2016 Biosystems, volume: 149, pages: 15 - 25
, volume: 421
Advances in Intelligent Systems and Computing
Van Laerhoven K, Scholl P
» show abstract« hide abstract
Abstract© Springer International Publishing Switzerland 2016. Wearable sensors have traditionally been designed around a micro controller that periodically reads values from attached sensor chips, before analyzing and forwarding data. As many off-the-shelf sensor chips have become smaller and widespread in consumer appliances, the way they are interfaced has become digital and more potent. This paper investigates the impact of using such chips that are not only smaller and cheaper as their predecessors, but also come with an arsenal of extra processing and detection capabilities, built in the sensor package. A case study with accompanying experiments using two MEMS accelerometers, show that using these capabilities can cause significant reductions in resources for data acquisition, and could even support basic recognition tasks.
, volume: 421
Advances in Intelligent Systems and Computing
Van Laerhoven K, Scholl P
» show abstract« hide abstract
Abstract© Springer International Publishing Switzerland 2016. Wearable sensors have traditionally been designed around a micro controller that periodically reads values from attached sensor chips, before analyzing and forwarding data. As many off-the-shelf sensor chips have become smaller and widespread in consumer appliances, the way they are interfaced has become digital and more potent. This paper investigates the impact of using such chips that are not only smaller and cheaper as their predecessors, but also come with an arsenal of extra processing and detection capabilities, built in the sensor package. A case study with accompanying experiments using two MEMS accelerometers, show that using these capabilities can cause significant reductions in resources for data acquisition, and could even support basic recognition tasks.
Ahmed Mahdi, Karsten Scheibler, Felix Neubauer, Martin Fränzle, Bernd Becker
Advancing software model checking beyond linear arithmetic theories
2016 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 14-17, 2016 Twelfth Haifa Verification Conference 2016, Bloem, Roderick, Arbel, Eli (Eds.), volume: 10028, pages: 186 - 201
» show abstract« hide abstract
AbstractMotivated by the practical need for verifying embedded control programs involving linear, polynomial, and transcendental arithmetics, we demonstrate in this paper a CEGAR technique addressing reachability checking over that rich fragment of arithmetics. In contrast to previous approaches, it is neither based on bit-blasting of floating- point implementations nor confined to decidable fragments of real arithmetic, namely linear or polynomial arithmetic. Its CEGAR loop is based on Craig interpolation within the iSAT3 SMT solver, which employs (abstract) conflict-driven clause learning (CDCL) over interval domains together with interval constraint propagation. As usual, the interpolants thus obtained on spurious counterexamples are used to subsequently refine the abstraction, yet in contrast to manipulating and refining the state set of a discrete-state abstraction, we propose a novel technique for refining the abstraction, where we annotate the abstract model’s transitions with side-conditions summarizing their effect. We exploit this for implementing case-based reasoning based on assumption-commitment predicates extracted from the stepwise interpolants in a lazy abstraction mechanism. We implemented our approach within iSAT3 and demonstrate its effectiveness by verifying several benchmarks.
Schwabe Nils, Scholl Philipp, Van Laerhoven Kristof
An Ad-Hoc Capture System for Augmenting Non-Digital Water Meters
2016 Proceedings of the 6th International Conference on the Internet of Things
Schwabe Nils, Scholl Philipp, Van Laerhoven Kristof
An Ad-Hoc Capture System for Augmenting Non-Digital Water Meters
2016 Proceedings of the 6th International Conference on the Internet of Things
Marius Lindauer Rolf-David, Hutter Frank
An Empirical Study of Per-Instance Algorithm Scheduling
2016 Proceedings of the International Conference on Learning and Intelligent Optimization (LION’16)
Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker
Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas
2016 Int'l Workshop on Logic and Synthesis
» show abstract« hide abstract
AbstractWe consider Dependency Quantified Boolean Formulas (DQBFs), a generalization of Quantified Boolean Formulas (QBFs), and demonstrate that DQBFs are a natural calculus to exactly express the realizability problem of incomplete combinational and sequential circuits with an arbitrary number of (combinational or bounded-memory) black boxes. In contrast to usual approaches for controller synthesis, restrictions to the interfaces of missing circuit parts in distributed architectures are strictly taken into account. We present a solution method for DQBFs together with the extraction of Skolem functions for existential variables, which can directly serve as implementations for the black boxes. First experimental results are provided.
Karsten Scheibler, Dominik Erb, Bernd Becker
Applying Tailored Formal Methods to X-ATPG
2016 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
» show abstract« hide abstract
AbstractWhen producing integrated circuits (ICs) one wants to know whether a manufactured IC works as expected and is free of physical defects. Basically, for combinational circuits, this is done by applying patterns to the circuit inputs and checking if the circuit outputs show the expected result. In case of sequential circuits, one concentrates on the combinational core of the circuit and treats the signal lines driven by flip-flops as additional (secondary) inputs. The job of automatic test pattern generation (ATPG) is to find such input patterns. Usually, these patterns are generated with respect to a fault-model. E.g. the stuck-at fault model assumes that a physical defect causes signal lines in a circuit to stay on a fixed logical value (logic-0 or logic-1). The aim is to find patterns for all possible fault locations. In SAT-based ATPG the circuit is transformed into two Boolean formulas F1 and F2. One formula describes the fault-free circuit and the second formula contains the fault-affected circuit (we consider one fault at a time). If (F1 XOR F2) is satisfiable a test pattern for the current fault under consideration is found. This is the basic principle of two-valued SAT-based ATPG and a very similar approach is used for combinational equivalence checking. However, usually, one can not assume full control of all sequential elements and primary inputs. Therefore, uninitialized flip-flops may occur in the design -- leading to binary but unknown values (X-values). Classically, these X-values are handled by three-valued logic (01X). But this introduces pessimism when X-values reconverge in the circuit. On the other hand, the expressiveness of QBF allows to encode the unknown values accurately -- but comes at the cost of much higher runtimes. Therefore, we presented in [1] an accurate SAT-based CEGAR approach for automatic test pattern generation (ATPG) in presence of X-values. This approach is tailored to and optimized for this specific problem class and could also be used for closely related topics such as equivalence checking in presence of X-values. Although the approach is similar to an existing CEGAR-based 2-QBF solving algorithm, we show that our method has up to 50x lower runtimes. This underlines that an efficient CNF-encoding of a problem together with the fastest available standard solver does not guarantee optimal performance. Tailoring the underlying formal methods to the target problem class may give remarkable speedups on top.
Ruder M., Dosovitskiy A., Brox T.
Artistic style transfer for videos
2016 German Conference on Pattern Recognition (GCPR)

Download file as PDF
Benedict Wright, Robert Mattmüller
Automated Data Management Workflow Generation with Ontologies and Planning
2016 30th Workshop on Planen/Scheduling und Konfigurieren/Entwerfen
Tobias Schubert, Katharina Eggensperger, Alexis Gkogkidis, Frank Hutter, Tonio Ball, Wolfram Burgard
Automatic Bone Parameter Estimation for Skeleton Tracking in Optical Motion Capture
2016 IEEE International Conference on Robotics and Automation 2016, Stockholm Proc of. IEEE International Conference on Robotics and Automation
» show abstract« hide abstract
AbstractMotion analysis is important in a broad range of contexts, including animation, bio-mechanics, robotics and experiments investigating animal behavior. For applications, in which tracking accuracy is one of the main require- ments, passive optical motion capture systems are widely used. Many skeleton tracking methods based on such systems use a predefined skeleton model, which is scaled once in the initialization step to the individual size of the character to be tracked. However, there are remarkable differences in the bone length relations across gender and even more across mammal races. In practice, the optimal skeleton model has to be determined in a manual and time-consuming process. In this paper, we reformulate this task as an optimization problem aiming to rescale a rough hierarchical skeleton structure to optimize probabilistic skeleton tracking performance. We solve this optimization problem by means of state-of-the-art black- box optimization methods based on sequential model-based Bayesian optimization (SMBO). We compare different SMBO methods on three real-world datasets with an animal and humans, demonstrating that we can automatically find skeleton structures for previously unseen mammals. The same methods also allow an automated choice of a suitable starting frame for initializing tracking.
Schubert T, Eggensperger K, Gkogkidis A, Hutter F, Ball T, Burgard W
Automatic Bone Parameter Estimation for Skeleton Tracking in Optical Motion Capture
2016 Proceedings of the IEEE International Conference on Robotics and Automation (ICRA’16)
Umarova Roza, Castaño-Candamil Sebastián, Bamdadian Atieh, Kübel Sebastian, Musso Mariacristina, Kloeppel Stefan, Tangermann Michael
BCI-Approach for Cognitive Rehabilitation in Stroke: Pilot Data from Patient with Spatial Neglect
2016 Asilomar Conference Center, Pacific Grove, California, USA Proceedings of the 6th International Brain-Computer Interface Meeting: BCI Past, Present, and Future, Verlag der Technischen Universität Graz, pages: 135 - 135
Wang Ziyu, Hutter Frank, Zoghi Masrour, Matheson David, de Freitas Nando
Bayesian Optimization in a Billion Dimensions via Random Embeddings
2016 Journal of Artificial Intelligence Research (JAIR), volume: 55, pages: 361 - 387
Springenberg J, Klein A, Falkner S, Hutter F
Bayesian optimization with robust Bayesian neural networks
2016 Advances in Neural Information Processing Systems 29
Bolander Thomas, Engesser Thorsten, Mattmüller Robert, Nebel Bernhard
Better Eager Than Lazy? How Agent Types Impact the Successfulness of Implicit Coordination
2016 Proceedings of the ICAPS-2016 Workshop on Distributed and Multi-Agent Planning (DMAP 2016)
Loshchilov I, Hutter F
CMA-ES for Hyperparameter Optimization of Deep Neural Networks
2016 International Conference on Learning Representations (ICLR) 2016 Workshop Track
Alkhnbashi Omer, Shah Shiraz, Garrett Roger, Saunders Sita, Costa Fabrizio, Backofen Rolf
Characterizing leader sequences of CRISPR loci
2016 Bioinformatics, volume: 32, issue: 17, pages: i576 - i585
» show abstract« hide abstract
AbstractMOTIVATION: The CRISPR-Cas system is an adaptive immune system in many archaea and bacteria, which provides resistance against invading genetic elements. The first phase of CRISPR-Cas immunity is called adaptation, in which small DNA fragments are excised from genetic elements and are inserted into a CRISPR array generally adjacent to its so called leader sequence at one end of the array. It has been shown that transcription initiation and adaptation signals of the CRISPR array are located within the leader. However, apart from promoters, there is very little knowledge of sequence or structural motifs or their possible functions. Leader properties have mainly been characterized through transcriptional initiation data from single organisms but large-scale characterization of leaders has remained challenging due to their low level of sequence conservation. RESULTS: We developed a method to successfully detect leader sequences by focusing on the consensus repeat of the adjacent CRISPR array and weak upstream conservation signals. We applied our tool to the analysis of a comprehensive genomic database and identified several characteristic properties of leader sequences specific to archaea and bacteria, ranging from distinctive sizes to preferential indel localization. CRISPRleader provides a full annotation of the CRISPR array, its strand orientation as well as conserved core leader boundaries that can be uploaded to any genome browser. In addition, it outputs reader-friendly HTML pages for conserved leader clusters from our database. AVAILABILITY AND IMPLEMENTATION: CRISPRleader and multiple sequence alignments for all 195 leader clusters are available at http://www.bioinf.uni-freiburg.de/Software/CRISPRleader/ CONTACT: costa@informatik.uni-freiburg.de or backofen@informatik.uni-freiburg.de SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.
Podelski A, Schäf M, Wies T
Classifying Bugs with Interpolants
2016 TAP, volume: 2016, pages: 151 - 168
Valeriy Balabanov, Jie-Hong R. Jiang, Alan Mishchenko, Christoph Scholl
Clauses Versus Gates in CEGAR-Based 2QBF Solving
2016 Workshop of the Thirtieth AAAI Conference on Artificial Intelligence Beyond NP
» show abstract« hide abstract
Abstract2QBF is a special case of general quantified Boolean formulae (QBF). It is limited to just two quantification levels, i.e., to a form \forall X \exists Y. \Phi. Despite this limitation it applies to a wide range of applications, e.g., to artificial intelligence, graph theory, synthesis, etc.. Recent research showed that CEGAR-based methods give a performance boost to QBF solving (e.g. compared to QDPLL). Conjunctive normal form (CNF) is a commonly accepted representation for both SAT and QBF problems; however, it does not reflect the circuit structure that might be present in the problem. Existing attempts of extracting this structure from CNF and using it in 2QBF context do not show advantages over CNF based 2QBF solvers. In this work we introduce a new workflow for 2QBF, containing a new *semantic* circuit extraction algorithm and a CEGAR-based 2QBF solver that uses circuit structure and is improved by so-called 'cofactor sharing' heuristics. We evaluate the proposed methodology on a range of benchmarks and show the practicality of the new approach.
Jimenez-Del-Toro o., Muller H., Krenn M., Gruenberg K., Aziz Taha A., Winterstein M., Eggel I., Foncubierta-Rodriguez A., Goksel O., Jakab A., Kontokotsios G., Langs G., Menze B., Salas Fernandez T., Schaer R., Walleyo A., Andre Weber M., Dicente Cid Y., Gass T., Heinrich M., Jia F., Kahl F., Kechichian R., Mai D., SpanierA., Vincent G., Wang C., Wyeth D., Hanbury A.
Cloud-Based Evaluation of Anatomical Structure Segmentation and Landmark Detection Algorithms: VISCERAL Anatomy Benchmarks
2016 Ieee T Med Imaging

Download file as PDF
Ragni Marco, Barkowsky Thomas, Nebel Bernhard, Freksa Christian
Cognitive Space and Spatial Cognition: The SFB/TR 8 Spatial Cognition.
2016 KI, volume: 30, issue: 1, pages: 83 - 88
Blahoudek Frantisek, Heizmann Matthias, Schewe Sven, Strejcek Jan, Tsai Ming-Hsien
Complementing Semi-deterministic Büchi Automata
2016 Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Springer, volume: 9636, pages: 770 - 787
Schindelhauer C, Reindl L, Bannoura A
Convergecast Algorithms for Wake-up Transceivers
2016 5th International Confererence on Sensor Networks , pages: 137 - 143
Beyer Dirk, Dangl Matthias, Dietsch Daniel, Heizmann Matthias
Correctness witnesses
2016 Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016, ACM, pages: 326 - 337
Thomas Metz, Uwe Wagschal, Thomas Waldvogel, Marko Bachl, Linus Feiten, Bernd Becker
Das Debat-O-Meter: ein neues Instrument zur Analyse von TV-Duellen
2016 ZSE Zeitschrift für Staats- und Europawissenschaften, volume: 14, issue: 1, pages: 124 - 149
Leivas Oliveira G., Valada A., Bollen C., Burgard W., Brox T.
Deep Learning for Human Part Discovery in Images
2016 IEEE International Conference on Robotics and Automation (ICRA),

Download file as PDF
Valada A., Leivas Oliveira G., Burgard W., Brox T.
Deep Multispectral Semantic Scene Understanding of Forested Environments using Multimodal Fusion
2016 International Symposium on Experimental Robotics (ISER 2016)

Download file as PDF
Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker
Dependency Schemes for DQBF
2016 Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer, volume: 9710, pages: 473 - 489
» show abstract« hide abstract
AbstractDependency schemes allow to identify variable independencies in QBFs or DQBFs. For QBF, several dependency schemes have been proposed, which differ in the number of independencies they are able to identify. In this paper, we analyze the spectrum of dependency schemes that were proposed for QBF. It turns out that only some of them are sound for DQBF. For the sound ones, we provide a correctness proof, for the others counterexamples. Experiments show that a significant number of dependencies can either be added to or removed from a formula without changing its truth value, but with significantly increasing the flexibility for modifying the representation.
Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker
Dependency Schemes for DQBF
2016 International Conference on Theory and Applications of Satisfiability Testing (SAT), issue: 9710, pages: 473 - 489
» show abstract« hide abstract
AbstractDependency schemes allow to identify variable independencies in QBFs or DQBFs. For QBF, several dependency schemes have been proposed, which differ in the number of independencies they are able to identify. In this paper, we analyze the spectrum of dependency schemes that were proposed for QBF. It turns out that only some of them are sound for DQBF. For the sound ones, we provide a correctness proof, for the others counter examples. Experiments show that a significant number of dependencies can either be added to or removed from a formula without changing its truth value, but with significantly increasing the flexibility for modifying the representation.
Holzer Martin, Krahling Verena, Amman Fabian, Barth Emanuel, Bernhart Stephan, Carmelo Victor, Collatz Maximilian, Doose Gero, Eggenhofer Florian, Ewald Jan, Fallmann Jorg, Feldhahn Lasse, Fricke Markus, Gebauer Juliane, Gruber Andreas, Hufsky Franziska, Indrischek Henrike, Kanton Sabina, Linde Jorg, Mostajo Nelly, Ochsenreiter Roman, Riege Konstantin, Rivarola-Duarte Lorena, Sahyoun Abdullah, Saunders Sita, Seemann Stefan, Tanzer Andrea, Vogel Bertram, Wehner Stefanie, Wolfinger Michael, Backofen Rolf, Gorodkin Jan, Grosse Ivo, Hofacker Ivo, Hoffmann Steve, Kaleta Christoph, Stadler Peter, Becker Stephan, Marz Manja
Differential transcriptional responses to Ebola and Marburg virus infection in bat and human cells
2016 Sci Rep-uk, volume: 6, page: 34589
» show abstract« hide abstract
AbstractThe unprecedented outbreak of Ebola in West Africa resulted in over 28,000 cases and 11,000 deaths, underlining the need for a better understanding of the biology of this highly pathogenic virus to develop specific counter strategies. Two filoviruses, the Ebola and Marburg viruses, result in a severe and often fatal infection in humans. However, bats are natural hosts and survive filovirus infections without obvious symptoms. The molecular basis of this striking difference in the response to filovirus infections is not well understood. We report a systematic overview of differentially expressed genes, activity motifs and pathways in human and bat cells infected with the Ebola and Marburg viruses, and we demonstrate that the replication of filoviruses is more rapid in human cells than in bat cells. We also found that the most strongly regulated genes upon filovirus infection are chemokine ligands and transcription factors. We observed a strong induction of the JAK/STAT pathway, of several genes encoding inhibitors of MAP kinases (DUSP genes) and of PPP1R15A, which is involved in ER stress-induced cell death. We used comparative transcriptomics to provide a data resource that can be used to identify cellular responses that might allow bats to survive filovirus infections.
Kong Hui, Bartocci Ezio, Bogomolov Sergiy, Grosu Radu, Henzinger Thomas, Jiang Yu, Schilling Christian
Discrete Abstraction of Multiaffine Systems
2016 HSB, volume: 9957, pages: 128 - 144
Dosovitskiy A., Fischer P., Spingenberg J., Riedmiller M., Brox T.
Discriminative Unsupervised Feature Learning with Exemplar Convolutional Neural Networks
2016 IEEE Transactions on Pattern Analysis and Machine Intelligence

Download file as PDF
Post Martijn, van der Putten Peter, van Rijn J
Does Feature Selection Improve Classification? A Large Scale Experiment in OpenML
2016 Advances in Intelligent Data Analysis XV, Springer, pages: 158 - 170
Castaño-Candamil Sebastián, Coenen Volker, Reinacher Peter, Piroth Tobias, Tangermann Michael
EP 65. DBS-induced alpha desynchronization in the subthalamic nucleus of PD patients
2016 Clin Neurophysiol, Elsevier, volume: 127, issue: 9, pages: e202 - e203
Castaño-Candamil Sebastián, Bamdadian Atieh, Kübel Sebastian, Umarova Roza, Tangermann Michael
ERP Features Correlate with Reaction Time in a Covert-Attention Task
2016 Asilomar Conference Center, Pacific Grove, California, USA Proceedings of the 6th International Brain-Computer Interface Meeting: BCI Past, Present, and Future, Verlag der Technischen Universität Graz, pages: 179 - 179
Bamdadian Atieh, Denzer Simone, Musso Cristina, Tangermann Michael
ERP Responses of the Elderly for Bisyllabic Word Stimuli
2016 Asilomar Conference Center, Pacific Grove, California, USA Proceedings of the 6th International Brain-Computer Interface Meeting: BCI Past, Present, and Future, Verlag der Technischen Universität Graz, pages: 180 - 180
Leivas Oliveira G., Burgard W., Brox T.
Efficient Deep Models for Monocular Road Segmentation.
2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)

Download file as PDF
Joan Bordoy J, Wendeberg J, Schindelhauer C, Höflinger F, Reindl L
Exploiting ground reflection for robust 3D smartphone localization
2016 International Conference on Indoor Positioning and Indoor Navigation , pages: 1 - 6
Mashhadi Afra, Acer Utku, Boran Aidan, Scholl Philipp, Forlivesi Claudio, Vanderhulst Geert, Kawsar Fahim
Exploring space syntax on entrepreneurial opportunities with Wi-Fi analytics
2016 Proceedings of the 2016 ACM International Joint Conference on Pervasive and Ubiquitous Computing - UbiComp ’16
» show abstract« hide abstract
AbstractIndustrial events and exhibitions play a powerful role in creating social relations amongst individuals and firms, enabling them to expand their social network so to acquire resources. However, often these events impose a spatial structure which impacts encounter opportunities. In this paper, we study the impact that the spatial configuration has on the formation of network relations. We designed, developed and deployed aWi-Fi analytics solution comprising of wearableWi-Fi badges and gateways in a large scale industrial exhibition event to study the spatio-temporal trajectories of the 2.5K+ attendees including two special groups: 34 investors and 27 entrepreneurs. Our results suggest that certain zones with designated functionalities play a key role in forming social ties across attendees and the different behavioural properties of investors and entrepreneurs can be explained through a spatial lens. Based on our findings we offer three concrete recommendations for future organisers of networking events.
Mashhadi Afra, Acer Utku, Boran Aidan, Scholl Philipp, Forlivesi Claudio, Vanderhulst Geert, Kawsar Fahim
Exploring space syntax on entrepreneurial opportunities with Wi-Fi analytics
2016 Proceedings of the 2016 ACM International Joint Conference on Pervasive and Ubiquitous Computing - UbiComp ’16
» show abstract« hide abstract
AbstractIndustrial events and exhibitions play a powerful role in creating social relations amongst individuals and firms, enabling them to expand their social network so to acquire resources. However, often these events impose a spatial structure which impacts encounter opportunities. In this paper, we study the impact that the spatial configuration has on the formation of network relations. We designed, developed and deployed aWi-Fi analytics solution comprising of wearableWi-Fi badges and gateways in a large scale industrial exhibition event to study the spatio-temporal trajectories of the 2.5K+ attendees including two special groups: 34 investors and 27 entrepreneurs. Our results suggest that certain zones with designated functionalities play a key role in forming social ties across attendees and the different behavioural properties of investors and entrepreneurs can be explained through a spatial lens. Based on our findings we offer three concrete recommendations for future organisers of networking events.
Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, Bernd Becker
Extending iSAT3 with ICP-Contractors for Bitwise Integer Operations
AVACS Technical Report, SFB/TR 14 AVACS, Subproject T1, volume: 116, 2016
Hafner D., Ochs P., Weickert J., Reißel M., Grewenig S.
FSI schemes: Fast semi-iterative solvers for PDEs and Optimisation Methods
2016 , volume: 9796, pages: 91 - 102

Download file as PDF
Seipp Jendrik, Pommerening Florian, Sievers Silvan, Wehrle Martin, Fawcett Chris, Alkhazraji Yusra
Fast Downward Aidos (planner abstract)
2016 The 1st Unsolvability International Planning Competition (IPC 2016)
Hoppmann Anselm, Schlosser Pascal, Backofen Rolf, Lausch Ekkehart, Kottgen Anna
GenToS
2016 PLoS One, volume: 11, issue: 9
» show abstract« hide abstract
AbstractGenome-wide association studies (GWAS) evaluate associations between genetic variants and a trait or disease of interest free of prior biological hypotheses. GWAS require stringent correction for multiple testing, with genome-wide significance typically defined as association p-value <5*10-8. This study presents a new tool that uses external information about genes to prioritize SNP associations (GenToS). For a given list of candidate genes, GenToS calculates an appropriate statistical significance threshold and then searches for trait-associated variants in summary statistics from human GWAS. It thereby allows for identifying trait-associated genetic variants that do not meet genome-wide significance. The program additionally tests for enrichment of significant candidate gene associations in the human GWAS data compared to the number expected by chance. As proof of principle, this report used external information from a comprehensive resource of genetically manipulated and systematically phenotyped mice. Based on selected murine phenotypes for which human GWAS data for corresponding traits were publicly available, several candidate gene input lists were derived. Using GenToS for the investigation of candidate genes underlying murine skeletal phenotypes in data from a large human discovery GWAS meta-analysis of bone mineral density resulted in the identification of significantly associated variants in 29 genes. Index variants in 28 of these loci were subsequently replicated in an independent GWAS replication step, highlighting that they are true positive associations. One signal, COL11A1, has not been discovered through GWAS so far and represents a novel human candidate gene for altered bone mineral density. The number of observed genes that contained significant SNP associations in human GWAS based on murine candidate gene input lists was much greater than the number expected by chance across several complex human traits (enrichment p-value as low as 10-10). GenToS can be used with any candidate gene list, any GWAS summary file, runs on a desktop computer and is freely available.
Dosovitskiy A., Brox T.
Generating Images with Perceptual Similarity Metrics based on Deep Networks
2016 Advances in Neural Information Processing Systems (NIPS)

Download file as PDF
Leike Jan, Heizmann Matthias
Geometric Nontermination Arguments
2016 CoRR, volume: abs/1609.05207
Holmqvist Erik, Wright Patrick, Li Lei, Bischler Thorsten, Barquist Lars, Reinhardt Richard, Backofen Rolf, Vogel Jorg
Global RNA recognition patterns of post-transcriptional regulators Hfq and CsrA revealed by UV crosslinking in vivo
2016 EMBO J
» show abstract« hide abstract
AbstractThe molecular roles of manyRNA-binding proteins in bacterial post-transcriptional gene regulation are not well understood. Approaches combiningin vivo UVcrosslinking withRNAdeep sequencing (CLIP-seq) have begun to revolutionize the transcriptome-wide mapping of eukaryoticRNA-binding protein target sites. We have appliedCLIP-seq to chart the target landscape of two major bacterial post-transcriptional regulators, Hfq and CsrA, in the model pathogenSalmonellaTyphimurium. By detecting binding sites at single-nucleotide resolution, we identifyRNApreferences and structural constraints of Hfq and CsrA during their interactions with hundreds of cellular transcripts. This reveals 3’-located Rho-independent terminators as a universal motif involved in Hfq-RNAinteractions. Additionally, Hfq preferentially binds 5’ tosRNA-target sites inmRNAs, and 3’ to seed sequences insRNAs, reflecting a simple logic in how Hfq facilitatessRNA-mRNAinteractions. Importantly, global knowledge of Hfq sites significantly improvessRNA-target predictions. CsrA bindsAUGGAsequences in apical loops and targets manySalmonellavirulencemRNAs. Overall, our genericCLIP-seq approach will bring new insights into post-transcriptional gene regulation byRNA-binding proteins in diverse bacterial species.
Bogomolov S, Donzé A, Frehse G, Grosu R, Johnson T, Ladan H, Podelski A, Wehrle M
Guided search for hybrid systems based on coarse-grained space abstractions
2016 STTT, volume: 18, pages: 449 - 467
Lindner Felix
How To Count Multiple Personal-Space Intrusions in Social Robot Navigation
2016 Proceedings of the Robo-Philosophy Conference 2016
Felix Lindner
How To Count Multiple Personal-Space Intrusions in Social Robot Navigation.
2016 In Proceedings of the Robo-Philosophy Conference 2016. 2016.
» show abstract« hide abstract
AbstractOne aspect of social robot navigation is to avoid personal space intrusions. Computationally, this can be achieved by introducing social costs into a robot's path planner's objective function. This article tackles the normative question of how robots should aggregate social costs incurred by multiple personal-space intrusions. Of particular interest is the question whether numbers should count, i.e., whether a robot ought to intrude into one person's personal space in order to aboid intruding into multiple personal spaces. This work proposes four different modes of aggregation of the costs of intrusions into personal space, discusses some of the philosophical arguments, and presents results from a pilot study.
Meinel Andreas, Eggensperger Katharina, Tangermann Michael, Hutter Frank
Hyperparameter Optimization for Machine Learning Problems in BCI
2016 Asilomar Conference Center, Pacific Grove, California, USA Proceedings of the 6th International Brain-Computer Interface Meeting: BCI Past, Present, and Future, Verlag der Technischen Universität Graz, pages: 184 - 184
Meinel A, Eggensperger K, Tangermann M, Hutter F
Hyperparameter Optimization for Machine Learning Problems in BCI (Abstract)
2016 Proceedings of the International Brain Computer Interface Meeting 2016
Van Laerhoven Kristof, Scholl Philipp
Interrupts Become Features: Using On-Sensor Intelligence for Recognition Tasks
In: Embedded Engineering Education
2016, Cham Springer International Publishing,
Van Laerhoven Kristof, Scholl Philipp
Interrupts Become Features: Using On-Sensor Intelligence for Recognition Tasks
In: Embedded Engineering Education
2016, Cham Springer International Publishing,
Dosovitskiy A., Brox T.
Inverting Visual Representations with Convolutional Networks
2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR)

Download file as PDF
Dosovitskiy A., Springenberg J., Tatarchenko M, Brox T.
Learning to Generate Chairs, Tables and Cars with Convolutional Networks
2016 IEEE Transactions on Pattern Analysis and Machine Intelligence

Download file as PDF
Wecker Thomas, Hoffmeier Klaus, Plotner Anne, Gruning Bjorn, Horres Ralf, Backofen Rolf, Reinhard Thomas, Schlunck Gunther
MicroRNA Profiling in Aqueous Humor of Individual Human Eyes by Next-Generation Sequencing
2016 Invest Ophth Vis Sci, volume: 57, issue: 4, pages: 1706 - 13
» show abstract« hide abstract
AbstractPURPOSE: Extracellular microRNAs (miRNAs) in aqueous humor were suggested to have a role in transcellular signaling and may serve as disease biomarkers. The authors adopted next-generation sequencing (NGS) techniques to further characterize the miRNA profile in single samples of 60 to 80 muL human aqueous humor. METHODS: Samples were obtained at the outset of cataract surgery in nine independent, otherwise healthy eyes. Four samples were used to extract RNA and generate sequencing libraries, followed by an adapter-driven amplification step, electrophoretic size selection, sequencing, and data analysis. Five samples were used for quantitative PCR (qPCR) validation of NGS results. Published NGS data on circulating miRNAs in blood were analyzed in comparison. RESULTS: One hundred fifty-eight miRNAs were consistently detected by NGS in all four samples; an additional 59 miRNAs were present in at least three samples. The aqueous humor miRNA profile shows some overlap with published NGS-derived inventories of circulating miRNAs in blood plasma with high prevalence of human miR-451a, -21, and -16. In contrast to blood, miR-184, -4448, -30a, -29a, -29c, -19a, -30d, -205, -24, -22, and -3074 were detected among the 20 most prevalent miRNAs in aqueous humor. Relative expression patterns of miR-451a, -202, and -144 suggested by NGS were confirmed by qPCR. CONCLUSIONS: Our data illustrate the feasibility of miRNA analysis by NGS in small individual aqueous humor samples. Intraocular cells as well as blood plasma contribute to the extracellular aqueous humor miRNome. The data suggest possible roles of miRNA in intraocular cell adhesion and signaling by TGF-beta and Wnt, which are important in intraocular pressure regulation and glaucoma.
Dominik Erb, Karsten Scheibler, Michael A. Kochte, Matthias Sauer, Hans-Joachim Wunderlich, Bernd Becker
Mixed 01X-RSL-Encoding for Fast and Accurate ATPG with Unknowns
2016 21st Asia and South Pacific Design Automation Conference
» show abstract« hide abstract
AbstractUnknown (X) values in a design introduce pessimism in conventional test generation algorithms, which results in a loss of fault coverage. This pessimism is reduced by a more accurate modeling and analysis. Unfortunately, accurate analysis techniques highly increase runtime and limit scalability. One promising technique to prevent high runtimes while still providing high accuracy is the use of restricted symbolic logic (RSL). However, also pure RSL-based algorithms reach their limits as soon as millon gate circuits need to be processed. In this paper, we propose new ATPG techniques to overcome such limitations. An efficient hybrid encoding combines the accuracy of RSL-based modeling with the compactness of conventional three-valued encoding. A low-cost two-valued SAT-based untestability check is able to classify most untestable faults with low runtime. An incremental and event-based accurate fault simulator is introduced to reduce fault simulation effort. The experiments demonstrate the effectiveness of the proposed techniques. On average, over 99.3% of the faults are accurately classified. Both the number of aborts and the total runtime are significantly reduced compared to the state-of-the-art pure RSL-based algorithm. For circuits up to a million gates, the fault coverage could be increased considerably compared to a state-of-the-art commercial tool with very competitive runtimes.
Tatarchenko M, Dosovitskiy A., Brox T.
Multi-view 3D Models from Single Images with a Convolutional Network
2016 European Conference on Computer Vision (ECCV)

Download file as PDF
Kaiser, A., Schmitz, S.
Neuroscience, Brain Research, and Sexuality.
2016 In N. Naples (Ed.), The Wiley-Blackwell Encyclopedia of Gender and Sexuality Studies, IV, pages: 1759 - 1765
» show abstract« hide abstract
AbstractSince, in the 1990s, the brain became an object of significant social importance and neuroscience emerged as a leading, powerful, and culturally significant field of science, gender and queer studies, too, began to devote considerable attention to examining how neuroscience makes sexual performance, sexual behavior, and sexual desire a part of the brain. In this entry, we describe how and when exactly sex/gender and sexuality became involved in neuroscience.
Der Andere Verlag
On the Handling of Uncertainty in Test Pattern Generation
ISBN: 978-3-86247-571-1
Dominik Erb
Loshchilov I, Hutter F
Online Batch Selection for Faster Training of Neural Networks
2016 International Conference on Learning Representations (ICLR) 2016 Workshop Track
Abdo N, Stachniss C, Burgard W, Spinello L
Organizing Objects by Predicting User Preferences Through Collaborative Filtering
2016 The International Journal of Robotics Research (IJRR)
» show abstract« hide abstract
AbstractAs service robots become more and more capable of performing useful tasks for us, there is a growing need to teach robots how we expect them to carry out these tasks. However, different users typically have their own preferences, for example with respect to arranging objects on different shelves. As many of these preferences depend on a variety of factors including personal taste, cultural background, or common sense, it is challenging for an expert to pre-program a robot in order to accommodate all potential users. At the same time, it is impractical for robots to constantly query users about how they should perform individual tasks. In this work, we present an approach to learn patterns in user preferences for the task of tidying up objects in containers, e.g. shelves or boxes. Our method builds upon the paradigm of collaborative filtering for making personalized recommendations and relies on data from different users which we gather using crowdsourcing. To deal with novel objects for which we have no data, we propose a method that compliments standard collaborative filtering by leveraging information mined from the Web. When solving a tidy-up task, we first predict pairwise object preferences of the user. Then, we subdivide the objects in containers by modeling a spectral clustering problem. Our solution is easy to update, does not require complex modeling, and improves with the amount of user data. We evaluate our approach using crowdsourcing data from over 1200 users and demonstrate its effectiveness for two tidy-up scenarios. Additionally, we show that a real robot can reliably predict user preferences using our approach.
Meyer Johannes, Meinel Andreas, Schreiner Thomas, Rasch Björn, Tangermann Michael
P26 Versuchspersonenunabhängige Single-Trial-Erkennung von langsamen Wellen im Schlaf-EEG
2016 Somnologie, volume: 20, issue: 1, pages: 75 - 76
Tobias Nicholas, Heinrich Antje, Eresmann Helena, Wright Patrick, Neubacher Nick, Backofen Rolf, Bode Helge
Photorhabdus-nematode symbiosis is dependent on hfq-mediated regulation of secondary metabolites
2016 Environ Microbiol
» show abstract« hide abstract
AbstractPhotorhabdus luminescens maintains a symbiotic relationship with the nematodes Heterorhabditis bacteriophora and together they infect and kill insect larvae. To maintain this symbiotic relationship, the bacteria must produce an array of secondary metabolites to assist in the development and replication of nematodes. The regulatory mechanisms surrounding production of these compounds are mostly unknown. The global post-transcriptional regulator, Hfq, is widespread in bacteria and performs many functions, one of which is the facilitation of sRNA binding to target mRNAs, with recent research thoroughly exploring its various pleiotropic effects. Here we generate and characterize an hfq deletion mutant and show that in the absence of hfq, the bacteria are no longer able to maintain a healthy symbiosis with nematodes due to the abolishment of the production of all known secondary metabolites. RNAseq led us to produce a second deletion of a known repressor, HexA, in the same strain, which restored both metabolite production and symbiosis. This article is protected by copyright. All rights reserved.
Uhrig J., Cordts M., Franke U., Brox T.
Pixel-level encoding and depth layering for instance-level semantic segmentation
2016 German Conference on Pattern Recognition (GCPR)

Download file as PDF
Tripp Vanessa, Martin Roman, Orell Alvaro, Alkhnbashi Omer, Backofen Rolf, Randau Lennart
Plasticity of archaeal C/D box sRNA biogenesis
2016 Mol Microbiol
» show abstract« hide abstract
AbstractArchaeal and eukaryotic organisms contain sets of C/D box s(no)RNAs with guide sequences that determine ribose 2’-O-methylation sites of target RNAs. The composition of these C/D box sRNA sets is highly variable between organisms and results in varying RNA modification patterns which are important for ribosomal RNA folding and stability. Little is known about the genomic organization of C/D box sRNA genes in archaea. Here, we aimed to obtain first insights into the biogenesis of these archaeal C/D box sRNAs and analyzed the genetic context of more than 300 archaeal sRNA genes. We found that the majority of these genes do not possess independent promoters but are rather located at positions that allow for co-transcription with neighboring genes and their start or stop codons were frequently incorporated into the conserved boxC and D motifs. The biogenesis of plasmid-encoded C/D box sRNA variants was analyzed in vivo in Sulfolobus acidocaldarius. It was found that C/D box sRNA maturation occurs independent of their genetic context and relies solely on the presence of intact RNA kink-turn structures. The observed plasticity of C/D box sRNA biogenesis is suggested to enable their accelerated evolution and, consequently, allow for adjustments of the RNA modification landscape. This article is protected by copyright. All rights reserved.
Keuper M., Brox T.
Point-wise mutual information-based video segmentation with high temporal consistency
2016 ECCV 2016 workshops Springer
Meinel Andreas, Castaño-Candamil Sebastián, Reis Janine, Tangermann Michael
Pre-Trial EEG-based Single-Trial Motor Performance Prediction to Enhance Neuroergonomics for a Hand Force Task
2016 Frontiers in Human Neuroscience, volume: 10, issue: 170
» show abstract« hide abstract
AbstractWe propose a framework for building electrophysiological predictors of single-trial motor performance variations, exemplified for SVIPT, a sequential isometric force control task suitable for hand motor rehabilitation after stroke. Electroencephalogram (EEG) data of 20 subjects with mean age of 53 years was recorded prior to and during 400 trials of SVIPT. They were executed within a single session with the non-dominant left hand, while receiving continuous visual feedback of the produced force trajectories. The behavioral data showed strong trial-by-trial performance variations for five clinically relevant metrics, which accounted for reaction time as well as for the smoothness and precision of the produced force trajectory. 18 out of 20 tested subjects remained after preprocessing and entered offline analysis. Source Power Comodulation (SPoC) was applied on EEG data of a short time interval prior to the start of each SVIPT trial. For 11 subjects, SPoC revealed robust oscillatory EEG subspace components, whose bandpower activity are predictive for the performance of the upcoming trial. Since SPoC may overfit to non-informative subspaces, we propose to apply three selection criteria accounting for the meaningfulness of the features. Across all subjects, the obtained components were spread along the frequency spectrum and showed a variety of spatial activity patterns. Those containing the highest level of predictive information resided in and close to the alpha band. Their spatial patterns resemble topologies reported for visual attention processes as well as those of imagined or executed hand motor tasks. In summary, we identified subject-specific single predictors that explain up to 36% of the performance fluctuations and may serve for enhancing neuroergonomics of motor rehabilitation scenarios.

Download file
Theiss Marian, Scholl Philipp
Predicting Grasps with a Wearable Inertial and EMG Sensing Unit for Low-Power Detection of In-Hand Objects
2016 Augmented Human
» show abstract« hide abstract
AbstractDetecting the task at hand can often be improved when it is also known what object the user is holding. Several sensing modalities have been suggested to identify handheld objects, from wrist-worn RFID readers to cameras. A critical obstacle to using such sensors, however, is that they tend to be too power hungry for continuous usage. This paper proposes a system that detects grasping using first inertial sensors and then Electromyography (EMG) on the forearm, to then selectively activate the object identification sensors. This three- Tiered approach would therefore only attempt to identify in-hand objects once it is known a grasping has occurred. Our experiments show that high recall can be obtained for grasp detection, 95% on average across participants, with the grasping of lighter and smaller objects clearly being more dificult. © 2016 ACM.
Theiss Marian, Scholl Philipp
Predicting Grasps with a Wearable Inertial and EMG Sensing Unit for Low-Power Detection of In-Hand Objects
2016 Augmented Human
» show abstract« hide abstract
AbstractDetecting the task at hand can often be improved when it is also known what object the user is holding. Several sensing modalities have been suggested to identify handheld objects, from wrist-worn RFID readers to cameras. A critical obstacle to using such sensors, however, is that they tend to be too power hungry for continuous usage. This paper proposes a system that detects grasping using first inertial sensors and then Electromyography (EMG) on the forearm, to then selectively activate the object identification sensors. This three- Tiered approach would therefore only attempt to identify in-hand objects once it is known a grasping has occurred. Our experiments show that high recall can be obtained for grasp detection, 95% on average across participants, with the grasping of lighter and smaller objects clearly being more dificult. © 2016 ACM.
Meinel Andreas, Schlichtmann Eva, Koller Torsten, Reis Janine, Tangermann Michael
Predicting Single-Trial Motor Performance from Oscillatory EEG in Chronic Stroke Patients
2016 Asilomar Conference Center, Pacific Grove, California, USA Proceedings of the 6th International Brain-Computer Interface Meeting: BCI Past, Present, and Future, Verlag der Technischen Universität Graz, pages: 140 - 140
Zimmermann Thomas, Cleland-Huang Jane, Su Zhendong
Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016
2016 ACM, ACM
Christ J, Hoenicke J
Proof Tree Preserving Tree Interpolation
2016 J Autom Reasoning, volume: 57, issue: 1, pages: 67 - 95
» show abstract« hide abstract
AbstractCraig interpolation has a wide range of applications in model checking, verification, and state space abstraction. Recent advances use a more general version of interpolation called tree interpolation. In this paper, we present a method to extract tree interpolants from a proof tree generated by an SMT solver without modifying the proof tree. The framework is general with respect to the theories involved. We instantiate the framework to the combination of the theories of uninterpreted functions and linear arithmetic.
Golkov V., Skwark M., Golkov A., Dosovitskiy A., Brox T., Meiler J., Cremers D.
Protein contact prediction from amino acid co-evolution using convolutional networks for graph-valued images
2016 Advances in Neural Information Processing Systems (NIPS)

Download file as PDF
Farzan A, Kincaid Z, Podelski A
Proving Liveness of Parameterized Programs
2016 LICS, volume: 2016, pages: 185 - 196
Del Vecchio Giorgia, De Vito Francesca, Saunders Sita, Risi Adele, Mannironi Cecilia, Bozzoni Irene, Presutti Carlo
RNA-binding protein HuR and the members of the miR-200 family play an unconventional role in the regulation of c-Jun mRNA
2016 RNA, volume: 22, issue: 10, pages: 1510 - 21
» show abstract« hide abstract
AbstractPost-transcriptional gene regulation is a fundamental step for coordinating cellular response in a variety of processes. RNA-binding proteins (RBPs) and microRNAs (miRNAs) are the most important factors responsible for this regulation. Here we report that different components of the miR-200 family are involved in c-Jun mRNA regulation with the opposite effect. While miR-200b inhibits c-Jun protein production, miR-200a tends to increase the JUN amount through a stabilization of its mRNA. This action is dependent on the presence of the RBP HuR that binds the 3’UTR of c-Jun mRNA in a region including the mir-200a binding site. The position of the binding site is fundamental; by mutating this site, we demonstrate that the effect is not micro-RNA specific. These results indicate that miR-200a triggers a microRNA-mediated stabilization of c-Jun mRNA, promoting the binding of HuR with c-Jun mRNA. This is the first example of a positive regulation exerted by a microRNA on an important oncogene in proliferating cells.
Feo Arenis S, Westphal B, Dietsch D, Muñiz M, Siyar Andisha A, Podelski A,
Ready for testing: ensuring conformance to industrial standards through formal verification
2016 Form Asp Comput, volume: 28, pages: 499 - 527
Hengel Matthias, Wölfl Stefan, Nebel Bernhard
Reasoning about general TBoxes with spatial and temporal constraints: Implementation and optimizations
2016 Proceedings of the 29th International Workshop on Description Logics (DL 2016)
Castaño-Candamil Sebastián, Dähne Sven, Tangermann Michael
Relevant Frequency Estimation in EEG Recordings for Source Power Co-Modulation
2016 Asilomar Conference Center, Pacific Grove, California, USA Proceedings of the 6th International Brain-Computer Interface Meeting: BCI Past, Present, and Future, Verlag der Technischen Universität Graz, pages: 156 - 156
Scholl Philipp, Van Laerhoven Kristof
Remind - Towards a Personal Remembrance Search Engine for Motion Augmented Multi-Media Recordings
2016 MUM 2016 - Proceedings of the international 2016 Conference on Multimedia and Ubiquitous Systems
Scholl Philipp, Van Laerhoven Kristof
Remind - Towards a Personal Remembrance Search Engine for Motion Augmented Multi-Media Recordings
2016 MUM 2016 - Proceedings of the international 2016 Conference on Multimedia and Ubiquitous Systems
Langenfeld V, Post A, Podelski A
Requirements Defects over a Project Lifetime: An Empirical Analysis of Defect Data from a 5-Year Automotive Project at Bosch
2016 REFSQ, volume: 2016, pages: 145 - 160
Linus Feiten, Sebastian Sester, Christian Zimmermann, Sebastian Volkmann, Laura Wehle, Bernd Becker
Revocable Anonymisation in Video Surveillance: A "Digital Cloak of Invisibility"
In: Technology and Intimacy: Choice or Coercion
2016, Springer International Publishing, pages: 314 - 327, ISBN: 978-3-319-44804-6
» show abstract« hide abstract
AbstractVideo surveillance is an omnipresent phenomenon in today's metropolitan life. Mainly intended to solve crimes, to prevent them by realtime-monitoring or simply as a deterrent, video surveillance has also become interesting in economical contexts; e.g. to create customer profiles and analyse patterns of their shopping behaviour. The extensive use of video surveillance is challenged by legal claims and societal norms like not putting everybody under generalised suspicion or not recording people without their consent. In this work we propose a technological solution to balance the positive and negative effects of video surveillance. With automatic image recognition algorithms on the rise, we suggest to use that technology to not just automatically identify people but blacken their images. This blackening is done with a cryptographic procedure allowing to revoke it with an appropriate key. Many of the legal and ethical objections to video surveillance could thereby be accommodated. In commercial scenarios, the operator of a customer profiling program could offer enticements for voluntarily renouncing one's anonymity. Customers could e.g. wear a small infrared LED to signal their agreement to being tracked. After explaining the implementation details, this work outlines a multidisciplinary discussion incorporating an economic, ethical and legal viewpoint.
Valada A., Leivas Oliveira G., Brox T., Burgard W.
Robust Semantic Segmentation using Deep Fusion
2016 Robotics: Science and Systems (RSS 2016) Workshop,Are the Sceptics Right? Limits and Potentials of Deep Learning in Robotics,

Download file as PDF
Müller S., Ochs P., Weickert J., Graf N.
Robust interactive multi-label segmentation with an advanced edge detector
2016 German Conference on Pattern Recognition (GCPR) LNCS, Springer, volume: 9796, pages: 117 - 128
Bast H, Delling D, Goldberg A, Müller-Hannemann M, Pajor T, Sanders P, Wagner D, Werneck R
Route Planning in Transportation Networks
In: Algorithm Engineering
2016, Springer, Lasse Kliemann, Peter Sanders, pages: 19 - 80, Lasse Kliemann, Peter Sanders, ISBN: 978-3-319-49486-9
» show abstract« hide abstract
AbstractWe survey recent advances in algorithms for route planning in transportation networks. For road networks, we show that one can compute driving directions in milliseconds or less even at continental scale. A variety of techniques provide different trade-offs between preprocessing effort, space requirements, and query time. Some algorithms can answer queries in a fraction of a microsecond, while others can deal efficiently with real-time traffic. Journey planning on public transportation systems, although conceptually similar, is a significantly harder problem due to its inherent time-dependent and multicriteria nature. Although exact algorithms are fast enough for interactive queries on metropolitan transit systems, dealing with continent-sized instances requires simplifications or heavy preprocessing. The multimodal route planning problem, which seeks journeys combining schedule-based transportation (buses, trains) with unrestricted modes (walking, driving), is even harder, relying on approximate solutions even for metropolitan inputs.
Bernd Becker, Katrin Weber, Linus Feiten
SMartphones In der LEhre (SMILE)
In: Kreativ, Innovativ, Motivierend - Lehrkonzepte in der Praxis: Der Instructional Development Award (IDA) der Universität Freiburg
2016, Universitäts Verlag Webler (UVW), pages: 117 - 133, ISBN: 3-946017-01-0
Kaiser, A.
Sex/Gender Matters and Sex/Gender Materialities in the Brain.
2016 In V. Pitts-Taylor (Ed.), Mattering: Feminism, Science and Materialism, pages: 123 - 139
» show abstract« hide abstract
AbstractAnelis Kaiser examines the sciences of the brain and the brain itself as contested sites for the exploration of sex/gender in material terms. She draws from Barad’s understanding of materiality to explain the subsurface of bodily matter and finds in this concept, to some extend, a way to approach the brain in its material becoming. The author shows the intransigence of dichotomously mattered sexed/gendered brain regions in neuroscientific practice, and argues that in contrast to Barad’s “non-vital” materiality of physics, addressing the brain’s sex/gendered materiality requires a distinct approach to the “bio” of neurobiological matter. Against this backdrop, she gives particular attention to the independent agency of matter and makes the applicability of an agentic materiality in neuroscientific empiricism a subject of discussion.
Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
Skolem Functions for DQBF
2016 Int'l Symposium on Automated Technology for Verification and Analysis (ATVA) Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Springer, volume: 9938, pages: 395 - 411
» show abstract« hide abstract
AbstractWe consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don't-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.
Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
Skolem Functions for DQBF
2016 International Symposium on Automated Technology for Verification and Analysis (ATVA)
» show abstract« hide abstract
AbstractWe consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don't-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.
Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
Skolem Functions for DQBF (Extended Version)
, 2016
Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
Skolem Functions for DQBF, Extended Version
, 2016
Alkhazraji Yusra, Wehrle Martin
Sleep Sets Meet Duplicate Elimination
2016 Proceedings of the Ninth Annual Symposium on Combinatorial Search (SoCS 2016) (SoCS 2016)
Maël Gay, Jan Burchard, Jan Horáček, Ange-Salomé Messeng Ekossono, Tobias Schubert, Bernd Becker, Ilia Polian, Martin Kreuzer
Small Scale AES Toolbox: Algebraic and Propositional Formulas, Circuit-Implementations and Fault Equations
2016 FCTRU'16
de Araujo Oliveira Joao, Costa Fabrizio, Backofen Rolf, Stadler Peter, Machado Telles Walter Maria, Hertel Jana
SnoReport 2.0
2016 BMC Bioinformatics, volume: 17, issue: Suppl 18
» show abstract« hide abstract
AbstractBACKGROUND: snoReport uses RNA secondary structure prediction combined with machine learning as the basis to identify the two main classes of small nucleolar RNAs, the box H/ACA snoRNAs and the box C/D snoRNAs. Here, we present snoReport 2.0, which substantially improves and extends in the original method by: extracting new features for both box C/D and H/ACA box snoRNAs; developing a more sophisticated technique in the SVM training phase with recent data from vertebrate organisms and a careful choice of the SVM parameters C and gamma; and using updated versions of tools and databases used for the construction of the original version of snoReport. To validate the new version and to demonstrate its improved performance, we tested snoReport 2.0 in different organisms. RESULTS: Results of the training and test phases of boxes H/ACA and C/D snoRNAs, in both versions of snoReport, are discussed. Validation on real data was performed to evaluate the predictions of snoReport 2.0. Our program was applied to a set of previously annotated sequences, some of them experimentally confirmed, of humans, nematodes, drosophilids, platypus, chickens and leishmania. We significantly improved the predictions for vertebrates, since the training phase used information of these organisms, but H/ACA box snoRNAs identification was improved for the other ones. CONCLUSION: We presented snoReport 2.0, to predict H/ACA box and C/D box snoRNAs, an efficient method to find true positives and avoid false positives in vertebrate organisms. H/ACA box snoRNA classifier showed an F-score of 93 % (an improvement of 10 % regarding the previous version), while C/D box snoRNA classifier, an F-Score of 94 % (improvement of 14 %). Besides, both classifiers exhibited performance measures above 90 %. These results show that snoReport 2.0 avoid false positives and false negatives, allowing to predict snoRNAs with high quality. In the validation phase, snoReport 2.0 predicted 67.43 % of vertebrate organisms for both classes. For Nematodes and Drosophilids, 69 % and 76.67 showing that snoReport 2.0 is good to identify snoRNAs in vertebrates and also H/ACA box snoRNAs in invertebrates organisms.
Knoop Jens, Zdun Uwe
Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik, 23.-26. Februar 2016, Wien, Österreich
2016 GILNI, GI, volume: 252
Bensch R., Scherf N., Huisken J., Brox T., Ronneberger O
Spatiotemporal Deformable Prototypes for Motion Anomaly Detection
2016 Int J Comput Vision, volume: 1, pages: 1 - 22
Stangler D, Mann M, Kahle H.-P., Rosskopf E, Fink S, Spiecker H
Spatiotemporal alignment of radial tracheid diameter profiles of submontane Norway spruce
2016 Dendrochronologia, volume: 37, pages: 33 - 45
» show abstract« hide abstract
AbstractStudying intra-annual wood formation dynamics provides valuable information on how tree growth and forests are affected by environmental changes and climatic extreme events. This study has the aim to evaluate and to quantify synergetic potentials emerging from a combination of current state of the art techniques used to monitor intra-annual wood formation processes. Norway spruce trees were studied in detail during the growing season 2009 with weekly sampling of microcores, high resolution point-dendrometers and wood anatomical analysis. The combination of the applied techniques allowed us to convert the spatial scales of radial tracheid diameter profiles to seasonal time scales and to synchronize fluctuations in intra-annual cell diameter profiles. This spatiotemporal information was used to validate the recently introduced software MICA (Multiple interval-based curve alignment). In comparison to the conventional approach of averaging profiles of tree ring variables, the MICA aligned profiles exhibit a significantly higher synchronicity of the averaged data points. We also demonstrate two new features in the MICA application that enable to extrapolate spatiotemporal information between intra-annual profiles for the construction of robust mean (consensus) profiles that are representative for the population dynamics. By using a set of complementary techniques in an integrated approach, this study highlights a new methodological framework that can contribute to a better understanding of the environmental control of wood formation during the growing season.
Manthey N, Lindauer M
SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers
2016 Proceedings of the International Conference on Satisfiability Solving (SAT’16)
Keller Thomas, Pommerening Florian, Seipp Jendrik, Geißer Florian, Mattmüller Robert
State-dependent Cost Partitionings for Cartesian Abstractions in Classical Planning (Extended Abstract)
2016 Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016)
Nguyen A., Dosovitskiy A., Yosinski J., Brox T., Clune J.
Synthesizing the preferred inputs for neurons in neural networks via deep generator networks
2016 Advances in Neural Information Processing Systems (NIPS)

Download file as PDF
Linus Feiten, Jonathan Oesterle, Tobias Martin, Matthias Sauer, Bernd Becker
Systematic Frequency Biases in Ring Oscillator PUFs on FPGAs
2016 IEEE Transactions on Multi-Scale Computing Systems (TMSCS), volume: PP, issue: 99
» show abstract« hide abstract
AbstractPhysically unclonable functions (PUFs) are an emerging primitive in hardware security, enabling the identification of computer-chips. A promising type particularly for FPGA implementations is the Ring Oscillator (RO) PUF, where signal delays – stemming from uncontrollable variations in the manufacturing process – are used as device-specific characteristics. Based on experimental results gathered with 38 identical Altera FPGAs, we show the existence of nondevice- specific i.e. systemic RO frequency biases, traced back to (1) the internal routing within the RO’s look-up tables, (2) the RO locations on the FPGAs, or (3) the non-PUF payload activity. As these biases are the same for all devices, the result is poor inter-device uniqueness and unreliable signatures under changing payloads. After characterising these biases with a newly developed set of metrics, we suggest a method to overcome them: Using only a small sample of devices, the average bias over all devices for each RO is predicted and the relative differences caused by systemic biases are nullified. We demonstrate the viability of this method by determining the sufficient random sample sizes and showing that the inter-device uniqueness is drastically increased and the PUF signatures become reliable even under changing payload activities.
Ralf Wimmer
Tagungsband des 19. GI/ITG/GMM-Workshops "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV)
2016 Universität Freiburg / FreiDok, page: 150
Martin Böhnert, Christoph Scholl
Task Variants with Different Scratchpad Memory Consumption in Multi-Task Environments
2016 International Conference on Architecture of Computing Systems (ARCS), issue: 9637, pages: 143 - 156
» show abstract« hide abstract
AbstractWe present an approach which schedules task sets using scratchpad memory (SPM) in an embedded multi-task system with real-time constraints. A new task model is introduced, where each task is represented by different pre-compiled variants which differ in the amount of scratchpad memory used. A higher use of SPM leads to smaller run-times of a task. Moreover, the energy consumption is reduced by replacing memory accesses by SPM accesses. Our heuristic method assembles a task set of these variants by choosing one variant per task. After selecting candidates from the pre-computed set of task variants, the task set can be handled by a real-time scheduler like EDF. Our approach is able to build a new incremental task set and feasible transition in dynamically changing environments. Furthermore we show an extension of our approach to multicore environments.
Ochs P., Ranftl R., Brox T., Pock T.
Techniques for gradient based bilevel optimization with nonsmooth lower level problems
2016 J Math Imaging Vis, volume: 56, issue: 2, pages: 175 - 194

Download file as PDF
Aldinger Johannes, Löhr Johannes
The Jumpbot Domain for Numeric Planning
Uni Freiburg, issue: 279, 2016
Christoph Scholl, Florian Pigorsch
The QBF Solver AIGSolve
2016 International Workshop on Quantified Boolean Formulas
» show abstract« hide abstract
AbstractAIGSolve is a rewriting-based solver based on And-Inverter Graphs (AIGs). In this approach, quantifiers are eliminated, starting with the inner-most quantifiers. Intermediate results are represented symbolically using AIGs. The basic method consists of cofactor-based quantifier elimination which is combined with a multitude of optimization approaches including a SAT- and BDD-based compaction of the representations, methods for preprocessing QBF-formulas based on incremental SAT, heuristics that exchange quantifiers of the same level, heuristics that use BDD-based quantifier elimination as an alternative, as well as structure extraction and structure exploitation for the processed instances.
Niknafs Yashar, Han Sumin, Ma Teng, Speers Corey, Zhang Chao, Wilder-Romans Kari, Iyer Matthew, Pitchiaya Sethuramasundaram, Malik Rohit, Hosono Yasuyuki, Prensner John, Poliakov Anton, Singhal Udit, Xiao Lanbo, Kregel Steven, Siebenaler Ronald, Zhao Shuang, Uhl Michael, Gawronski Alexander, Hayes Daniel, Pierce Lori, Cao Xuhong, Collins Colin, Backofen Rolf, Sahinalp Cenk, Rae James, Chinnaiyan Arul, Feng Felix
The lncRNA landscape of breast cancer reveals a role for DSCAM-AS1 in breast cancer progression
2016 Nat Commun, volume: 7
» show abstract« hide abstract
AbstractMolecular classification of cancers into subtypes has resulted in an advance in our understanding of tumour biology and treatment response across multiple tumour types. However, to date, cancer profiling has largely focused on protein-coding genes, which comprise <1% of the genome. Here we leverage a compendium of 58,648 long noncoding RNAs (lncRNAs) to subtype 947 breast cancer samples. We show that lncRNA-based profiling categorizes breast tumours by their known molecular subtypes in breast cancer. We identify a cohort of breast cancer-associated and oestrogen-regulated lncRNAs, and investigate the role of the top prioritized oestrogen receptor (ER)-regulated lncRNA, DSCAM-AS1. We demonstrate that DSCAM-AS1 mediates tumour progression and tamoxifen resistance and identify hnRNPL as an interacting protein involved in the mechanism of DSCAM-AS1 action. By highlighting the role of DSCAM-AS1 in breast cancer biology and treatment resistance, this study provides insight into the potential clinical implications of lncRNAs in breast cancer.
Chechik Marsha, Raskin Jean-François
Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
2016 SpringerLecture Notes in Computer Science, Springer, volume: 9636
Mendoza H, Klein A, Feurer M, Springenberg J, Hutter F
Towards Automatically-Tuned Neural Networks
2016 ICML 2016 AutoML Workshop
Sun Dali, Geißer Florian, Nebel Bernhard
Towards Effective Localization in Dynamic Environments
2016 Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2016)
Schulte Tim, Nebel Bernhard
Trial-based Heuristic Tree-search for Distributed Multi-Agent Planning
2016 Proceedings of the 4th Workshop on Distributed and Multi-Agent Planning (DMAP 2016) (DMAP 2016)
Schulte Tim, Nebel Bernhard
Trial-based Heuristic Tree-search for Distributed Multi-Agent Planning
2016 Proceedings of the Ninth Annual Symposium on Combinatorial Search (SoCS 2016) (SoCS 2016)
Schindelhauer C, janson T, Traub-Ens A
Turning interferences into noise in ad hoc networks
2016 Telecommun Syst, issue: 62, supplement: 2, pages: 435 - 448
Duggirala Parasara, Fan Chuchu, Potok Matthew, Qi Bolun, Mitra Sayan, Viswanathan Mahesh, Bak Stanley, Bogomolov Sergiy, Johnson Taylor, Nguyen Luan, Schilling Christian, Sogokon Andrew, Tran Hoang-Dung, Xiang Weiming
Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP
2016 2016 IEEE Conference on Control Applications, CCA 2016, Buenos Aires, Argentina, September 19-22, 2016, IEEE, pages: 1024 - 1029
Paolo Marin, Massimno Narizzano, Luca Pulina, Armando Tacchella, Enrico Giunchiglia
Twelve Years of QBF Evaluations: QSAT Is PSpace-Hard and It Shows
2016 Fund Inform, volume: 149, issue: 1-2, pages: 133 - 158
Heizmann M, Dietsch D, Greitschus M, Leike J, Musa B, Schätzle C, Podelski A
Ultimate Automizer with Two-track Proofs - (Competition Contribution)
2016 TACAS, volume: 2016, pages: 950 - 953
Heizmann Matthias, Dietsch Daniel, Greitschus Marius, Leike Jan, Musa Betim, Schätzle Claus, Podelski Andreas
Ultimate Automizer with Two-track Proofs - (Competition Contribution)
2016 Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Springer, volume: 9636, pages: 950 - 953
Matthias Sauer, Linus Feiten, Bernd Becker, Ulrich Rührmair, Ilia Polian
Utilizing Intrinsic Delay Variability in Complex Digital Circuits for Defining PUF Behavior
2016 TRUDEVICE Workshop, Dresden
Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, Boris Wirtz
Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization
SFB/TR 14 AVACS Technical Report, issue: 103, 2016
Beyer Dirk, Dangl Matthias, Dietsch Daniel, Heizmann Matthias, Stahlbauer Andreas
Witness validation and stepwise testification across software verifiers
2016 Software Engineering 2016, Fachtagung des GI-Fachbereichs Softwaretechnik, 23.-26. Februar 2016, Wien, Österreich, GI, volume: 252, pages: 105 - 106
Golkov V., Dosovitskiy A., Sperl J., Menzel M., Czisch M., Sämann P., Brox T., Cremers D.
q-Space Deep Learning: Twelve-Fold Shorter and Model-Free Diffusion MRI Scans
2016 Ieee T Med Imaging, volume: 25, issue: 5

Download file as PDF

Credits: SILK Icons by http://www.famfamfam.com/lab/icons/silk/

Publications IIF of last two years

2017

2016

Start Footer

Personal tools

Document Actions

Publications IIF of last two years

2017

2016

Start Footer

Personal tools