@article{1027,
  abstract     = {The rising prevalence of antibiotic resistant bacteria is an increasingly serious public health challenge. To address this problem, recent work ranging from clinical studies to theoretical modeling has provided valuable insights into the mechanisms of resistance, its emergence and spread, and ways to counteract it. A deeper understanding of the underlying dynamics of resistance evolution will require a combination of experimental and theoretical expertise from different disciplines and new technology for studying evolution in the laboratory. Here, we review recent advances in the quantitative understanding of the mechanisms and evolution of antibiotic resistance. We focus on key theoretical concepts and new technology that enables well-controlled experiments. We further highlight key challenges that can be met in the near future to ultimately develop effective strategies for combating resistance.},
  author       = {Lukacisinova, Marta and Bollenbach, Mark Tobias},
  journal      = {Current Opinion in Biotechnology},
  pages        = {90 -- 97},
  publisher    = {Elsevier},
  title        = {{Toward a quantitative understanding of antibiotic resistance evolution}},
  doi          = {10.1016/j.copbio.2017.02.013},
  volume       = {46},
  year         = {2017},
}

@article{682,
  abstract     = {Left-right asymmetry is a fundamental feature of higher-order brain structure; however, the molecular basis of brain asymmetry remains unclear. We recently identified structural and functional asymmetries in mouse hippocampal circuitry that result from the asymmetrical distribution of two distinct populations of pyramidal cell synapses that differ in the density of the NMDA receptor subunit GluRε2 (also known as NR2B, GRIN2B or GluN2B). By examining the synaptic distribution of ε2 subunits, we previously found that β2-microglobulin-deficient mice, which lack cell surface expression of the vast majority of major histocompatibility complex class I (MHCI) proteins, do not exhibit circuit asymmetry. In the present study, we conducted electrophysiological and anatomical analyses on the hippocampal circuitry of mice with a knockout of the paired immunoglobulin-like receptor B (PirB), an MHCI receptor. As in β2-microglobulin-deficient mice, the PirB-deficient hippocampus lacked circuit asymmetries. This finding that MHCI loss-of-function mice and PirB knockout mice have identical phenotypes suggests that MHCI signals that produce hippocampal asymmetries are transduced through PirB. Our results provide evidence for a critical role of the MHCI/PirB signaling system in the generation of asymmetries in hippocampal circuitry.},
  author       = {Ukai, Hikari and Kawahara, Aiko and Hirayama, Keiko and Case, Matthew J and Aino, Shotaro and Miyabe, Masahiro and Wakita, Ken and Oogi, Ryohei and Kasayuki, Michiyo and Kawashima, Shihomi and Sugimoto, Shunichi and Chikamatsu, Kanako and Nitta, Noritaka and Koga, Tsuneyuki and Shigemoto, Ryuichi and Takai, Toshiyuki and Ito, Isao},
  issn         = {1932-6203},
  journal      = {PLoS One},
  number       = {6},
  publisher    = {Public Library of Science},
  title        = {{PirB regulates asymmetries in hippocampal circuitry}},
  doi          = {10.1371/journal.pone.0179377},
  volume       = {12},
  year         = {2017},
}

@article{1024,
  abstract     = {The history of auxin and cytokinin biology including the initial discoveries by father–son duo Charles Darwin and Francis Darwin (1880), and Gottlieb Haberlandt (1919) is a beautiful demonstration of unceasing continuity of research. Novel findings are integrated into existing hypotheses and models and deepen our understanding of biological principles. At the same time new questions are triggered and hand to hand with this new methodologies are developed to address these new challenges.},
  author       = {Hurny, Andrej and Benková, Eva},
  issn         = {1064-3745},
  journal      = {Auxins and Cytokinins in Plant Biology},
  pages        = {1 -- 29},
  publisher    = {Springer},
  title        = {{Methodological advances in auxin and cytokinin biology}},
  doi          = {10.1007/978-1-4939-6831-2_1},
  volume       = {1569},
  year         = {2017},
}

@article{1028,
  abstract     = {Optogenetics and photopharmacology provide spatiotemporally precise control over protein interactions and protein function in cells and animals. Optogenetic methods that are sensitive to green light and can be used to break protein complexes are not broadly available but would enable multichromatic experiments with previously inaccessible biological targets. Herein, we repurposed cobalamin (vitamin B12) binding domains of bacterial CarH transcription factors for green-light-induced receptor dissociation. In cultured cells, we observed oligomerization-induced cell signaling for the fibroblast growth factor receptor 1 fused to cobalamin-binding domains in the dark that was rapidly eliminated upon illumination. In zebrafish embryos expressing fusion receptors, green light endowed control over aberrant fibroblast growth factor signaling during development. Green-light-induced domain dissociation and light-inactivated receptors will critically expand the optogenetic toolbox for control of biological processes.},
  author       = {Kainrath, Stephanie and Stadler, Manuela and Gschaider-Reichhart, Eva and Distel, Martin and Janovjak, Harald L},
  issn         = {1433-7851},
  journal      = {Angewandte Chemie International Edition},
  number       = {16},
  pages        = {4608--4611},
  publisher    = {Wiley},
  title        = {{Green-light-induced inactivation of receptor signaling using cobalamin-binding domains}},
  doi          = {10.1002/anie.201611998},
  volume       = {56},
  year         = {2017},
}

@inproceedings{1082,
  abstract     = {In many applications, it is desirable to extract only the relevant aspects of data. A principled way to do this is the information bottleneck (IB) method, where one seeks a code that maximises information about a relevance variable, Y, while constraining the information encoded about the original data, X. Unfortunately however, the IB method is computationally demanding when data are high-dimensional and/or non-gaussian. Here we propose an approximate variational scheme for maximising a lower bound on the IB objective, analogous to variational EM. Using this method, we derive an IB algorithm to recover features that are both relevant and sparse. Finally, we demonstrate how kernelised versions of the algorithm can be used to address a broad range of problems with non-linear relation between X and Y.},
  author       = {Chalk, Matthew J and Marre, Olivier and Tkacik, Gasper},
  location     = {Barcelona, Spain},
  pages        = {1965--1973},
  publisher    = {Neural Information Processing Systems Foundation},
  title        = {{Relevant sparse codes with variational information bottleneck}},
  volume       = {29},
  year         = {2016},
}

@inproceedings{1090,
  abstract     = { While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.},
  author       = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
  location     = {Krakow; Poland},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Nested weighted limit-average automata of bounded width}},
  doi          = {10.4230/LIPIcs.MFCS.2016.24},
  volume       = {58},
  year         = {2016},
}

@inproceedings{1093,
  abstract     = {We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. },
  author       = {Daca, Przemyslaw and Henzinger, Thomas A and Kretinsky, Jan and Petrov, Tatjana},
  location     = {Quebec City; Canada},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Linear distances between Markov chains}},
  doi          = {10.4230/LIPIcs.CONCUR.2016.20},
  volume       = {59},
  year         = {2016},
}

@inproceedings{1095,
  abstract     = { The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations. },
  author       = {Haas, Andreas and Henzinger, Thomas A and Holzer, Andreas and Kirsch, Christoph and Lippautz, Michael and Payer, Hannes and Sezgin, Ali and Sokolova, Ana and Veith, Helmut},
  booktitle    = {Leibniz International Proceedings in Informatics},
  location     = {Quebec City; Canada},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Local linearizability for concurrent container-type data structures}},
  doi          = {10.4230/LIPIcs.CONCUR.2016.6},
  volume       = {59},
  year         = {2016},
}

@inproceedings{1097,
  abstract     = {We present an interactive system for computational design, optimization, and fabrication of multicopters. Our computational approach allows non-experts to design, explore, and evaluate a wide range of different multicopters. We provide users with an intuitive interface for assembling a multicopter from a collection of components (e.g., propellers, motors, and carbon fiber rods). Our algorithm interactively optimizes shape and controller parameters of the current design to ensure its proper operation. In addition, we allow incorporating a variety of other metrics (such as payload, battery usage, size, and cost) into the design process and exploring tradeoffs between them. We show the efficacy of our method and system by designing, optimizing, fabricating, and operating multicopters with complex geometries and propeller configurations. We also demonstrate the ability of our optimization algorithm to improve the multicopter performance under different metrics.},
  author       = {Du, Tao and Schulz, Adriana and Zhu, Bo and Bickel, Bernd and Matusik, Wojciech},
  location     = {Macao, China},
  number       = {6},
  publisher    = {ACM},
  title        = {{Computational multicopter design}},
  doi          = {10.1145/2980179.2982427},
  volume       = {35},
  year         = {2016},
}

@inproceedings{1098,
  abstract     = {Better understanding of the potential benefits of information transfer and representation learning is an important step towards the goal of building intelligent systems that are able to persist in the world and learn over time. In this work, we consider a setting where the learner encounters a stream of tasks but is able to retain only limited information from each encountered task, such as a learned predictor. In contrast to most previous works analyzing this scenario, we do not make any distributional assumptions on the task generating process. Instead, we formulate a complexity measure that captures the diversity of the observed tasks. We provide a lifelong learning algorithm with error guarantees for every observed task (rather than on average). We show sample complexity reductions in comparison to solving every task in isolation in terms of our task complexity measure. Further, our algorithmic framework can naturally be viewed as learning a representation from encountered tasks with a neural network.},
  author       = {Pentina, Anastasia and Urner, Ruth},
  location     = {Barcelona, Spain},
  pages        = {3619--3627},
  publisher    = {Neural Information Processing Systems Foundation},
  title        = {{Lifelong learning with weighted majority votes}},
  volume       = {29},
  year         = {2016},
}

@inproceedings{1099,
  abstract     = {We present FlexMolds, a novel computational approach to automatically design flexible, reusable molds that, once 3D printed, allow us to physically fabricate, by means of liquid casting, multiple copies of complex shapes with rich surface details and complex topology. The approach to design such flexible molds is based on a greedy bottom-up search of possible cuts over an object, evaluating for each possible cut the feasibility of the resulting mold. We use a dynamic simulation approach to evaluate candidate molds, providing a heuristic to generate forces that are able to open, detach, and remove a complex mold from the object it surrounds. We have tested the approach with a number of objects with nontrivial shapes and topologies.},
  author       = {Malomo, Luigi and Pietroni, Nico and Bickel, Bernd and Cignoni, Paolo},
  location     = {Macao, China},
  number       = {6},
  publisher    = {ACM},
  title        = {{FlexMolds: Automatic design of flexible shells for molding}},
  doi          = {10.1145/2980179.2982397},
  volume       = {35},
  year         = {2016},
}

@inproceedings{1102,
  abstract     = {Weakly-supervised object localization methods tend to fail for object classes that consistently co-occur with the same background elements, e.g. trains on tracks. We propose a method to overcome these failures by adding a very small amount of model-specific additional annotation. The main idea is to cluster a deep network\'s mid-level representations and assign object or distractor labels to each cluster. Experiments show substantially improved localization results on the challenging ILSVC2014 dataset for bounding box detection and the PASCAL VOC2012 dataset for semantic segmentation.},
  author       = {Kolesnikov, Alexander and Lampert, Christoph},
  booktitle    = {Proceedings of the British Machine Vision Conference 2016},
  location     = {York, United Kingdom},
  pages        = {92.1--92.12},
  publisher    = {BMVA Press},
  title        = {{Improving weakly-supervised object localization by micro-annotation}},
  doi          = {10.5244/C.30.92},
  volume       = {2016-September},
  year         = {2016},
}

@inproceedings{1103,
  abstract     = {We propose two parallel state-space-exploration algorithms for hybrid automaton (HA), with the goal of enhancing performance on multi-core shared-memory systems. The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN model checker, when traversing the discrete modes of the HA, and enhances it with a parallel exploration of the continuous states within each mode. We show that this simple-minded extension of PBFS does not provide the desired load balancing in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS), which uses a cheap precomputation of the cost associated with the post operations (both continuous and discrete) in order to improve load balancing. We illustrate the TP-BFS and the cost precomputation of the post operators on a support-function-based algorithm for state-space exploration. The performance comparison of the two algorithms shows that, in general, TP-BFS provides a better utilization/load-balancing of the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect to SpaceEx LGG scenario. In order to make the comparison fair, we employed an equal number of post operations in both tools. To the best of our knowledge, this paper represents the first attempt to provide parallel, reachability-analysis algorithms for HA.},
  author       = {Gurung, Amit and Deka, Arup and Bartocci, Ezio and Bogomolov, Sergiy and Grosu, Radu and Ray, Rajarshi},
  location     = {Kanpur, India },
  publisher    = {IEEE},
  title        = {{Parallel reachability analysis for hybrid systems}},
  doi          = {10.1109/MEMCOD.2016.7797741},
  year         = {2016},
}

@inproceedings{1105,
  abstract     = {Jointly characterizing neural responses in terms of several external variables promises novel insights into circuit function, but remains computationally prohibitive in practice. Here we use gaussian process (GP) priors and exploit recent advances in fast GP inference and learning based on Kronecker methods, to efficiently estimate multidimensional nonlinear tuning functions. Our estimator require considerably less data than traditional methods and further provides principled uncertainty estimates. We apply these tools to hippocampal recordings during open field exploration and use them to characterize the joint dependence of CA1 responses on the position of the animal and several other variables, including the animal\'s speed, direction of motion, and network oscillations.Our results provide an unprecedentedly detailed quantification of the tuning of hippocampal neurons. The model\'s generality suggests that our approach can be used to estimate neural response properties in other brain regions.},
  author       = {Savin, Cristina and Tkacik, Gasper},
  location     = {Barcelona; Spain},
  pages        = {3610--3618},
  publisher    = {Neural Information Processing Systems Foundation},
  title        = {{Estimating nonlinear neural response functions using GP priors and Kronecker methods}},
  volume       = {29},
  year         = {2016},
}

@article{11069,
  abstract     = {Repeated rounds of nuclear envelope (NE) rupture and repair have been observed in laminopathy and cancer cells and result in intermittent loss of nucleus compartmentalization. Currently, the causes of NE rupture are unclear. Here, we show that NE rupture in cancer cells relies on the assembly of contractile actin bundles that interact with the nucleus via the linker of nucleoskeleton and cytoskeleton (LINC) complex. We found that the loss of actin bundles or the LINC complex did not rescue nuclear lamina defects, a previously identified determinant of nuclear membrane stability, but did decrease the number and size of chromatin hernias. Finally, NE rupture inhibition could be rescued in cells treated with actin-depolymerizing drugs by mechanically constraining nucleus height. These data suggest a model of NE rupture where weak membrane areas, caused by defects in lamina organization, rupture because of an increase in intranuclear pressure from actin-based nucleus confinement.},
  author       = {Hatch, Emily M. and HETZER, Martin W},
  issn         = {0021-9525},
  journal      = {Journal of Cell Biology},
  keywords     = {Cell Biology},
  number       = {1},
  pages        = {27--36},
  publisher    = {Rockefeller University Press},
  title        = {{Nuclear envelope rupture is induced by actin-based nucleus confinement}},
  doi          = {10.1083/jcb.201603053},
  volume       = {215},
  year         = {2016},
}

@article{11070,
  abstract     = {The organization of the genome in the three-dimensional space of the nucleus is coupled with cell type-specific gene expression. However, how nuclear architecture influences transcription that governs cell identity remains unknown. Here, we show that nuclear pore complex (NPC) components Nup93 and Nup153 bind superenhancers (SE), regulatory structures that drive the expression of key genes that specify cell identity. We found that nucleoporin-associated SEs localize preferentially to the nuclear periphery, and absence of Nup153 and Nup93 results in dramatic transcriptional changes of SE-associated genes. Our results reveal a crucial role of NPC components in the regulation of cell type-specifying genes and highlight nuclear architecture as a regulatory layer of genome functions in cell fate.},
  author       = {Ibarra, Arkaitz and Benner, Chris and Tyagi, Swati and Cool, Jonah and HETZER, Martin W},
  issn         = {1549-5477},
  journal      = {Genes & Development},
  keywords     = {Developmental Biology, Genetics},
  number       = {20},
  pages        = {2253--2258},
  publisher    = {Cold Spring Harbor Laboratory},
  title        = {{Nucleoporin-mediated regulation of cell identity genes}},
  doi          = {10.1101/gad.287417.116},
  volume       = {30},
  year         = {2016},
}

@article{11071,
  abstract     = {Nuclear pore complexes (NPCs) emerged as nuclear transport channels in eukaryotic cells ∼1.5 billion years ago. While the primary role of NPCs is to regulate nucleo–cytoplasmic transport, recent research suggests that certain NPC proteins have additionally acquired the role of affecting gene expression at the nuclear periphery and in the nucleoplasm in metazoans. Here we identify a widely expressed variant of the transmembrane nucleoporin (Nup) Pom121 (named sPom121, for “soluble Pom121”) that arose by genomic rearrangement before the divergence of hominoids. sPom121 lacks the nuclear membrane-anchoring domain and thus does not localize to the NPC. Instead, sPom121 colocalizes and interacts with nucleoplasmic Nup98, a previously identified transcriptional regulator, at gene promoters to control transcription of its target genes in human cells. Interestingly, sPom121 transcripts appear independently in several mammalian species, suggesting convergent innovation of Nup-mediated transcription regulation during mammalian evolution. Our findings implicate alternate transcription initiation as a mechanism to increase the functional diversity of NPC components.},
  author       = {Franks, Tobias M. and Benner, Chris and Narvaiza, Iñigo and Marchetto, Maria C.N. and Young, Janet M. and Malik, Harmit S. and Gage, Fred H. and HETZER, Martin W},
  issn         = {1549-5477},
  journal      = {Genes & Development},
  keywords     = {Developmental Biology, Genetics},
  number       = {10},
  pages        = {1155--1171},
  publisher    = {Cold Spring Harbor Laboratory},
  title        = {{Evolution of a transcriptional regulator from a transmembrane nucleoporin}},
  doi          = {10.1101/gad.280941.116},
  volume       = {30},
  year         = {2016},
}

@article{11072,
  abstract     = {Spatiotemporal activation of RhoA and actomyosin contraction underpins cellular adhesion and division. Loss of cell–cell adhesion and chromosomal instability are cardinal events that drive tumour progression. Here, we show that p120-catenin (p120) not only controls cell–cell adhesion, but also acts as a critical regulator of cytokinesis. We find that p120 regulates actomyosin contractility through concomitant binding to RhoA and the centralspindlin component MKLP1, independent of cadherin association. In anaphase, p120 is enriched at the cleavage furrow where it binds MKLP1 to spatially control RhoA GTPase cycling. Binding of p120 to MKLP1 during cytokinesis depends on the N-terminal coiled-coil domain of p120 isoform 1A. Importantly, clinical data show that loss of p120 expression is a common event in breast cancer that strongly correlates with multinucleation and adverse patient survival. In summary, our study identifies p120 loss as a driver event of chromosomal instability in cancer.
},
  author       = {van de Ven, Robert A.H. and de Groot, Jolien S. and Park, Danielle and van Domselaar, Robert and de Jong, Danielle and Szuhai, Karoly and van der Wall, Elsken and Rueda, Oscar M. and Ali, H. Raza and Caldas, Carlos and van Diest, Paul J. and HETZER, Martin W and Sahai, Erik and Derksen, Patrick W.B.},
  issn         = {2041-1723},
  journal      = {Nature Communications},
  keywords     = {General Physics and Astronomy, General Biochemistry, Genetics and Molecular Biology, General Chemistry},
  publisher    = {Springer Nature},
  title        = {{p120-catenin prevents multinucleation through control of MKLP1-dependent RhoA activity during cytokinesis}},
  doi          = {10.1038/ncomms13874},
  volume       = {7},
  year         = {2016},
}

@inproceedings{1115,
  abstract     = {We present a coherent microwave to telecom signal converter based on the electro-optical effect using a crystalline WGM-resonator coupled to a 3D microwave cavity, achieving high photon conversion efficiency of 0.1% with MHz bandwidth.},
  author       = {Rueda, Alfredo and Sedlmeir, Florian and Collodo, Michele and Vogl, Ulrich and Stiller, Birgit and Schunk, Georg and Strekalov, Dimitry and Marquardt, Christoph and Fink, Johannes M and Painter, Oskar and Leuchs, Gerd and Schwefel, Harald},
  location     = {San Jose, CA, USA},
  publisher    = {IEEE},
  title        = {{Efficient single sideband microwave to optical conversion using a LiNbO₃ WGM-resonator}},
  doi          = {10.1364/CLEO_SI.2016.SF2G.3},
  year         = {2016},
}

@phdthesis{1130,
  abstract     = {In this thesis we present a computer-aided programming approach to concurrency. Our approach helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t. a specification. We consider both user-provided explicit specifications in the form of assertion
statements in the code as well as an implicit specification. The implicit specification is inferred from the non-preemptive behaviour. Let us consider sequences of calls that the program makes to an external interface. The implicit specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We consider several semantics-preserving fixes that go beyond atomic sections typically explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers and wait-signal statements and last, but not least reorder independent statements. The latter may be useful if a thread is released to early, e.g., before some initialisation is completed. We guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective function. We dub our solution trace-based synchronisation synthesis and it is loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger the specification violation. Synchronisation may be placed immediately (greedy approach) or delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach we construct a set of global constraints over synchronisation placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronisation placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronisation solution. We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver
benchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs. For the experiments with an explicit specification we added assertions that would detect the bugs in the experiments. Device drivers lend themselves to implicit specification, where the device and the operating system are the external interfaces. Our experiments demonstrate that our synthesis method is precise and efficient. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronisation placements are produced for our experiments, favouring e.g. a minimal number of synchronisation operations or maximum concurrency.},
  author       = {Tarrach, Thorsten},
  issn         = {2663-337X},
  pages        = {151},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Automatic synthesis of synchronisation primitives for concurrent programs}},
  doi          = {10.15479/at:ista:1130},
  year         = {2016},
}

