@inproceedings{8302, abstract = {While showing great promise, Bitcoin requires users to wait tens of minutes for transactions to commit, and even then, offering only probabilistic guarantees. This paper introduces ByzCoin, a novel Byzantine consensus protocol that leverages scalable collective signing to commit Bitcoin transactions irreversibly within seconds. ByzCoin achieves Byzantine consensus while preserving Bitcoin’s open membership by dynamically forming hash power-proportionate consensus groups that represent recently-successful block miners. ByzCoin employs communication trees to optimize transaction commitment and verification under normal operation while guaranteeing safety and liveness under Byzantine faults, up to a near-optimal tolerance of f faulty group members among 3f + 2 total. ByzCoin mitigates double spending and selfish mining attacks by producing collectively signed transaction blocks within one minute of transaction submission. Tree-structured communication further reduces this latency to less than 30 seconds. Due to these optimizations, ByzCoin achieves a throughput higher than Paypal currently handles, with a confirmation latency of 15-20 seconds.}, author = {Kokoris Kogias, Eleftherios and Jovanovic, Philipp and Gailly, Nicolas and Khoffi, Ismail and Gasser, Linus and Ford, Bryan}, booktitle = {Proceedings of the 25th USENIX Conference on Security Symposium}, isbn = {9781931971324}, location = {Austin, TX, United States}, pages = {279–296}, publisher = {USENIX Association}, title = {{Enhancing bitcoin security and performance with strong consistency via collective signing}}, year = {2016}, } @article{9019, abstract = {Targeting protein–protein interactions has long been considered as a very difficult if impossible task, but over the past decade, front lines have moved. The number of successful examples is exponentially growing. This review presents a rapid overview of recent advances in this field considering the strengths and weaknesses of the small molecule approaches and alternative strategies such as the selection or design of artificial antibodies, peptides or peptidomimetics.}, author = {Bakail, May M and Ochsenbein, Francoise}, issn = {1631-0748}, journal = {Comptes Rendus Chimie}, keywords = {General Chemistry, General Chemical Engineering}, number = {1-2}, pages = {19--27}, publisher = {Elsevier}, title = {{Targeting protein–protein interactions, a wide open field for drug design}}, doi = {10.1016/j.crci.2015.12.004}, volume = {19}, year = {2016}, } @article{9051, abstract = {Biological systems often involve the self-assembly of basic components into complex and functioning structures. Artificial systems that mimic such processes can provide a well-controlled setting to explore the principles involved and also synthesize useful micromachines. Our experiments show that immotile, but active, components self-assemble into two types of structure that exhibit the fundamental forms of motility: translation and rotation. Specifically, micron-scale metallic rods are designed to induce extensile surface flows in the presence of a chemical fuel; these rods interact with each other and pair up to form either a swimmer or a rotor. Such pairs can transition reversibly between these two configurations, leading to kinetics reminiscent of bacterial run-and-tumble motion.}, author = {Davies Wykes, Megan S. and Palacci, Jérémie A and Adachi, Takuji and Ristroph, Leif and Zhong, Xiao and Ward, Michael D. and Zhang, Jun and Shelley, Michael J.}, issn = {1744-6848}, journal = {Soft Matter}, number = {20}, pages = {4584--4589}, publisher = {Royal Society of Chemistry}, title = {{Dynamic self-assembly of microscale rotors and swimmers}}, doi = {10.1039/c5sm03127c}, volume = {12}, year = {2016}, } @article{9052, abstract = {We describe colloidal Janus particles with metallic and dielectric faces that swim vigorously when illuminated by defocused optical tweezers without consuming any chemical fuel. Rather than wandering randomly, these optically-activated colloidal swimmers circulate back and forth through the beam of light, tracing out sinuous rosette patterns. We propose a model for this mode of light-activated transport that accounts for the observed behavior through a combination of self-thermophoresis and optically-induced torque. In the deterministic limit, this model yields trajectories that resemble rosette curves known as hypotrochoids.}, author = {Moyses, Henrique and Palacci, Jérémie A and Sacanna, Stefano and Grier, David G.}, issn = {1744-6848}, journal = {Soft Matter}, keywords = {General Chemistry, Condensed Matter Physics}, number = {30}, pages = {6357--6364}, publisher = {Royal Society of Chemistry }, title = {{Trochoidal trajectories of self-propelled Janus particles in a diverging laser beam}}, doi = {10.1039/c6sm01163b}, volume = {12}, year = {2016}, } @article{9140, abstract = {Expected changes to future extreme precipitation remain a key uncertainty associated with anthropogenic climate change. Extreme precipitation has been proposed to scale with the precipitable water content in the atmosphere. Assuming constant relative humidity, this implies an increase of precipitation extremes at a rate of about 7% °C−1 globally as indicated by the Clausius‐Clapeyron relationship. Increases faster and slower than Clausius‐Clapeyron have also been reported. In this work, we examine the scaling between precipitation extremes and temperature in the present climate using simulations and measurements from surface weather stations collected in the frame of the HyMeX and MED‐CORDEX programs in Southern France. Of particular interest are departures from the Clausius‐Clapeyron thermodynamic expectation, their spatial and temporal distribution, and their origin. Looking at the scaling of precipitation extreme with temperature, two regimes emerge which form a hook shape: one at low temperatures (cooler than around 15°C) with rates of increase close to the Clausius‐Clapeyron rate and one at high temperatures (warmer than about 15°C) with sub‐Clausius‐Clapeyron rates and most often negative rates. On average, the region of focus does not seem to exhibit super Clausius‐Clapeyron behavior except at some stations, in contrast to earlier studies. Many factors can contribute to departure from Clausius‐Clapeyron scaling: time and spatial averaging, choice of scaling temperature (surface versus condensation level), and precipitation efficiency and vertical velocity in updrafts that are not necessarily constant with temperature. But most importantly, the dynamical contribution of orography to precipitation in the fall over this area during the so‐called “Cevenoles” events, explains the hook shape of the scaling of precipitation extremes.}, author = {Drobinski, P. and Alonzo, B. and Bastin, S. and Silva, N. Da and Muller, Caroline J}, issn = {2169-897X}, journal = {Journal of Geophysical Research: Atmospheres}, number = {7}, pages = {3100--3119}, publisher = {American Geophysical Union}, title = {{Scaling of precipitation extremes with temperature in the French Mediterranean region: What explains the hook shape?}}, doi = {10.1002/2015jd023497}, volume = {121}, year = {2016}, } @article{9456, abstract = {The discovery of introns four decades ago was one of the most unexpected findings in molecular biology. Introns are sequences interrupting genes that must be removed as part of messenger RNA production. Genome sequencing projects have shown that most eukaryotic genes contain at least one intron, and frequently many. Comparison of these genomes reveals a history of long evolutionary periods during which few introns were gained, punctuated by episodes of rapid, extensive gain. However, although several detailed mechanisms for such episodic intron generation have been proposed, none has been empirically supported on a genomic scale. Here we show how short, non-autonomous DNA transposons independently generated hundreds to thousands of introns in the prasinophyte Micromonas pusilla and the pelagophyte Aureococcus anophagefferens. Each transposon carries one splice site. The other splice site is co-opted from the gene sequence that is duplicated upon transposon insertion, allowing perfect splicing out of the RNA. The distributions of sequences that can be co-opted are biased with respect to codons, and phasing of transposon-generated introns is similarly biased. These transposons insert between pre-existing nucleosomes, so that multiple nearby insertions generate nucleosome-sized intervening segments. Thus, transposon insertion and sequence co-option may explain the intron phase biases and prevalence of nucleosome-sized exons observed in eukaryotes. Overall, the two independent examples of proliferating elements illustrate a general DNA transposon mechanism that can plausibly account for episodes of rapid, extensive intron gain during eukaryotic evolution.}, author = {Huff, Jason T. and Zilberman, Daniel and Roy, Scott W.}, issn = {1476-4687}, journal = {Nature}, number = {7626}, pages = {533--536}, publisher = {Springer Nature }, title = {{Mechanism for DNA transposons to generate introns on genomic scales}}, doi = {10.1038/nature20110}, volume = {538}, year = {2016}, } @article{9473, abstract = {Cytosine DNA methylation regulates the expression of eukaryotic genes and transposons. Methylation is copied by methyltransferases after DNA replication, which results in faithful transmission of methylation patterns during cell division and, at least in flowering plants, across generations. Transgenerational inheritance is mediated by a small group of cells that includes gametes and their progenitors. However, methylation is usually analyzed in somatic tissues that do not contribute to the next generation, and the mechanisms of transgenerational inheritance are inferred from such studies. To gain a better understanding of how DNA methylation is inherited, we analyzed purified Arabidopsis thaliana sperm and vegetative cells-the cell types that comprise pollen-with mutations in the DRM, CMT2, and CMT3 methyltransferases. We find that DNA methylation dependency on these enzymes is similar in sperm, vegetative cells, and somatic tissues, although DRM activity extends into heterochromatin in vegetative cells, likely reflecting transcription of heterochromatic transposons in this cell type. We also show that lack of histone H1, which elevates heterochromatic DNA methylation in somatic tissues, does not have this effect in pollen. Instead, levels of CG methylation in wild-type sperm and vegetative cells, as well as in wild-type microspores from which both pollen cell types originate, are substantially higher than in wild-type somatic tissues and similar to those of H1-depleted roots. Our results demonstrate that the mechanisms of methylation maintenance are similar between pollen and somatic cells, but the efficiency of CG methylation is higher in pollen, allowing methylation patterns to be accurately inherited across generations.}, author = {Hsieh, Ping-Hung and He, Shengbo and Buttress, Toby and Gao, Hongbo and Couchman, Matthew and Fischer, Robert L. and Zilberman, Daniel and Feng, Xiaoqi}, issn = {1091-6490}, journal = {Proceedings of the National Academy of Sciences}, number = {52}, pages = {15132--15137}, publisher = {National Academy of Sciences}, title = {{Arabidopsis male sexual lineage exhibits more robust maintenance of CG methylation than somatic tissues}}, doi = {10.1073/pnas.1619074114}, volume = {113}, year = {2016}, } @article{9477, abstract = {Cytosine methylation is a DNA modification with important regulatory functions in eukaryotes. In flowering plants, sexual reproduction is accompanied by extensive DNA demethylation, which is required for proper gene expression in the endosperm, a nutritive extraembryonic seed tissue. Endosperm arises from a fusion of a sperm cell carried in the pollen and a female central cell. Endosperm DNA demethylation is observed specifically on the chromosomes inherited from the central cell in Arabidopsis thaliana, rice, and maize, and requires the DEMETER DNA demethylase in Arabidopsis. DEMETER is expressed in the central cell before fertilization, suggesting that endosperm demethylation patterns are inherited from the central cell. Down-regulation of the MET1 DNA methyltransferase has also been proposed to contribute to central cell demethylation. However, with the exception of three maize genes, central cell DNA methylation has not been directly measured, leaving the origin and mechanism of endosperm demethylation uncertain. Here, we report genome-wide analysis of DNA methylation in the central cells of Arabidopsis and rice—species that diverged 150 million years ago—as well as in rice egg cells. We find that DNA demethylation in both species is initiated in central cells, which requires DEMETER in Arabidopsis. However, we do not observe a global reduction of CG methylation that would be indicative of lowered MET1 activity; on the contrary, CG methylation efficiency is elevated in female gametes compared with nonsexual tissues. Our results demonstrate that locus-specific, active DNA demethylation in the central cell is the origin of maternal chromosome hypomethylation in the endosperm.}, author = {Park, Kyunghyuk and Kim, M. Yvonne and Vickers, Martin and Park, Jin-Sup and Hyun, Youbong and Okamoto, Takashi and Zilberman, Daniel and Fischer, Robert L. and Feng, Xiaoqi and Choi, Yeonhee and Scholten, Stefan}, issn = {1091-6490}, journal = {Proceedings of the National Academy of Sciences}, keywords = {Multidisciplinary}, number = {52}, pages = {15138--15143}, publisher = {National Academy of Sciences}, title = {{DNA demethylation is initiated in the central cells of Arabidopsis and rice}}, doi = {10.1073/pnas.1619047114}, volume = {113}, year = {2016}, } @inproceedings{948, abstract = {Experience constantly shapes neural circuits through a variety of plasticity mechanisms. While the functional roles of some plasticity mechanisms are well-understood, it remains unclear how changes in neural excitability contribute to learning. Here, we develop a normative interpretation of intrinsic plasticity (IP) as a key component of unsupervised learning. We introduce a novel generative mixture model that accounts for the class-specific statistics of stimulus intensities, and we derive a neural circuit that learns the input classes and their intensities. We will analytically show that inference and learning for our generative model can be achieved by a neural circuit with intensity-sensitive neurons equipped with a specific form of IP. Numerical experiments verify our analytical derivations and show robust behavior for artificial and natural stimuli. Our results link IP to non-trivial input statistics, in particular the statistics of stimulus intensities for classes to which a neuron is sensitive. More generally, our work paves the way toward new classification algorithms that are robust to intensity variations.}, author = {Monk, Travis and Savin, Cristina and Lücke, Jörg}, location = {Barcelona, Spaine}, pages = {4285 -- 4293}, publisher = {Neural Information Processing Systems Foundation}, title = {{Neurons equipped with intrinsic plasticity learn stimulus intensity statistics}}, volume = {29}, year = {2016}, } @article{9591, abstract = {We give several results showing that different discrete structures typically gain certain spanning substructures (in particular, Hamilton cycles) after a modest random perturbation. First, we prove that adding linearly many random edges to a dense k-uniform hypergraph ensures the (asymptotically almost sure) existence of a perfect matching or a loose Hamilton cycle. The proof involves an interesting application of Szemerédi's Regularity Lemma, which might be independently useful. We next prove that digraphs with certain strong expansion properties are pancyclic, and use this to show that adding a linear number of random edges typically makes a dense digraph pancyclic. Finally, we prove that perturbing a certain (minimum-degree-dependent) number of random edges in a tournament typically ensures the existence of multiple edge-disjoint Hamilton cycles. All our results are tight.}, author = {Krivelevich, Michael and Kwan, Matthew Alan and Sudakov, Benny}, issn = {1469-2163}, journal = {Combinatorics, Probability and Computing}, number = {6}, pages = {909--927}, publisher = {Cambridge University Press}, title = {{Cycles and matchings in randomly perturbed digraphs and hypergraphs}}, doi = {10.1017/s0963548316000079}, volume = {25}, year = {2016}, } @misc{9704, abstract = {Emerging infectious diseases (EIDs) have contributed significantly to the current biodiversity crisis, leading to widespread epidemics and population loss. Owing to genetic variation in pathogen virulence, a complete understanding of species decline requires the accurate identification and characterization of EIDs. We explore this issue in the Western honeybee, where increasing mortality of populations in the Northern Hemisphere has caused major concern. Specifically, we investigate the importance of genetic identity of the main suspect in mortality, deformed wing virus (DWV), in driving honeybee loss. Using laboratory experiments and a systematic field survey, we demonstrate that an emerging DWV genotype (DWV-B) is more virulent than the established DWV genotype (DWV-A) and is widespread in the landscape. Furthermore, we show in a simple model that colonies infected with DWV-B collapse sooner than colonies infected with DWV-A. We also identify potential for rapid DWV evolution by revealing extensive genome-wide recombination in vivo. The emergence of DWV-B in naive honeybee populations, including via recombination with DWV-A, could be of significant ecological and economic importance. Our findings emphasize that knowledge of pathogen genetic identity and diversity is critical to understanding drivers of species decline.}, author = {Mcmahon, Dino and Natsopoulou, Myrsini and Doublet, Vincent and Fürst, Matthias and Weging, Silvio and Brown, Mark and Gogol Döring, Andreas and Paxton, Robert}, publisher = {Dryad}, title = {{Data from: Elevated virulence of an emerging viral genotype as a driver of honeybee loss}}, doi = {10.5061/dryad.cq7t1}, year = {2016}, } @misc{9710, abstract = {Much of quantitative genetics is based on the ‘infinitesimal model’, under which selection has a negligible effect on the genetic variance. This is typically justified by assuming a very large number of loci with additive effects. However, it applies even when genes interact, provided that the number of loci is large enough that selection on each of them is weak relative to random drift. In the long term, directional selection will change allele frequencies, but even then, the effects of epistasis on the ultimate change in trait mean due to selection may be modest. Stabilising selection can maintain many traits close to their optima, even when the underlying alleles are weakly selected. However, the number of traits that can be optimised is apparently limited to ~4Ne by the ‘drift load’, and this is hard to reconcile with the apparent complexity of many organisms. Just as for the mutation load, this limit can be evaded by a particular form of negative epistasis. A more robust limit is set by the variance in reproductive success. This suggests that selection accumulates information most efficiently in the infinitesimal regime, when selection on individual alleles is weak, and comparable with random drift. A review of evidence on selection strength suggests that although most variance in fitness may be because of alleles with large Nes, substantial amounts of adaptation may be because of alleles in the infinitesimal regime, in which epistasis has modest effects.}, author = {Barton, Nicholas H}, publisher = {Dryad}, title = {{Data from: How does epistasis influence the response to selection?}}, doi = {10.5061/dryad.s5s7r}, year = {2016}, } @misc{9720, abstract = {Summary: Declining populations of bee pollinators are a cause of concern, with major repercussions for biodiversity loss and food security. RNA viruses associated with honeybees represent a potential threat to other insect pollinators, but the extent of this threat is poorly understood. This study aims to attain a detailed understanding of the current and ongoing risk of emerging infectious disease (EID) transmission between managed and wild pollinator species across a wide range of RNA viruses. Within a structured large-scale national survey across 26 independent sites, we quantify the prevalence and pathogen loads of multiple RNA viruses in co-occurring managed honeybee (Apis mellifera) and wild bumblebee (Bombus spp.) populations. We then construct models that compare virus prevalence between wild and managed pollinators. Multiple RNA viruses associated with honeybees are widespread in sympatric wild bumblebee populations. Virus prevalence in honeybees is a significant predictor of virus prevalence in bumblebees, but we remain cautious in speculating over the principle direction of pathogen transmission. We demonstrate species-specific differences in prevalence, indicating significant variation in disease susceptibility or tolerance. Pathogen loads within individual bumblebees may be high and in the case of at least one RNA virus, prevalence is higher in wild bumblebees than in managed honeybee populations. Our findings indicate widespread transmission of RNA viruses between managed and wild bee pollinators, pointing to an interconnected network of potential disease pressures within and among pollinator species. In the context of the biodiversity crisis, our study emphasizes the importance of targeting a wide range of pathogens and defining host associations when considering potential drivers of population decline.}, author = {Mcmahon, Dino and Fürst, Matthias and Caspar, Jesicca and Theodorou, Panagiotis and Brown, Mark and Paxton, Robert}, publisher = {Dryad}, title = {{Data from: A sting in the spit: widespread cross-infection of multiple RNA viruses across wild and managed bees}}, doi = {10.5061/dryad.4b565}, year = {2016}, } @inproceedings{478, abstract = {Magic: the Gathering is a game about magical combat for any number of players. Formally it is a zero-sum, imperfect information stochastic game that consists of a potentially unbounded number of steps. We consider the problem of deciding if a move is legal in a given single step of Magic. We show that the problem is (a) coNP-complete in general; and (b) in P if either of two small sets of cards are not used. Our lower bound holds even for single-player Magic games. The significant aspects of our results are as follows: First, in most real-life game problems, the task of deciding whether a given move is legal in a single step is trivial, and the computationally hard task is to find the best sequence of legal moves in the presence of multiple players. In contrast, quite uniquely our hardness result holds for single step and with only one-player. Second, we establish efficient algorithms for important special cases of Magic.}, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus}, location = {The Hague, Netherlands}, pages = {1432 -- 1439}, publisher = {IOS Press}, title = {{The complexity of deciding legality of a single step of magic: The gathering}}, doi = {10.3233/978-1-61499-672-9-1432}, volume = {285}, year = {2016}, } @inproceedings{480, abstract = {Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is 1. Previous results presented a semi-decision procedure for -approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements.}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, location = {New York, NY, USA}, pages = {247 -- 256}, publisher = {IEEE}, title = {{Perfect-information stochastic games with generalized mean-payoff objectives}}, doi = {10.1145/2933575.2934513}, volume = {05-08-July-2016}, year = {2016}, } @article{510, abstract = {The CLE (CLAVATA3/Embryo Surrounding Region-related) peptides are small secreted signaling peptides that are primarily involved in the regulation of stem cell homeostasis in different plant meristems. Particularly, the characterization of the CLE41-PXY/TDR signaling pathway has greatly advanced our understanding on the potential roles of CLE peptides in vascular development and wood formation. Nevertheless, our knowledge on this gene family in a tree species is limited. In a recent study, we reported on a systematically investigation of the CLE gene family in Populus trichocarpa . The potential roles of PtCLE genes were studied by comparative analysis and transcriptional pro fi ling. Among fi fty PtCLE members, many PtCLE proteins share identical CLE motifs or contain the same CLE motif as that of AtCLEs, while PtCLE genes exhibited either comparable or distinct expression patterns comparing to their Arabidopsis counterparts. These fi ndings indicate the existence of both functional conservation and functional divergence between PtCLEs and their AtCLE orthologues. Our results provide valuable resources for future functional investigations of these critical signaling molecules in woody plants. }, author = {Liu, Zhijun and Yang, Nan and Lv, Yanting and Pan, Lixia and Lv, Shuo and Han, Huibin and Wang, Guodong}, journal = {Plant Signaling & Behavior}, number = {6}, publisher = {Taylor & Francis}, title = {{The CLE gene family in Populus trichocarpa}}, doi = {10.1080/15592324.2016.1191734}, volume = {11}, year = {2016}, } @misc{5445, abstract = {We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs. }, author = {Chatterjee, Krishnendu and Pavlogiannis, Andreas and Velner, Yaron}, issn = {2664-1690}, pages = {33}, publisher = {IST Austria}, title = {{Quantitative interprocedural analysis}}, doi = {10.15479/AT:IST-2016-523-v1-1}, year = {2016}, } @misc{5446, abstract = {We study the problem of developing efficient approaches for proving termination of recursive programs with one-dimensional arrays. Ranking functions serve as a sound and complete approach for proving termination of non-recursive programs without array operations. First, we generalize ranking functions to the notion of measure functions, and prove that measure functions (i) provide a sound method to prove termination of recursive programs (with one-dimensional arrays), and (ii) is both sound and complete over recursive programs without array operations. Our second contribution is the synthesis of measure functions of specific forms in polynomial time. More precisely, we prove that (i) polynomial measure functions over recursive programs can be synthesized in polynomial time through Farkas’ Lemma and Handelman’s Theorem, and (ii) measure functions involving logarithm and exponentiation can be synthesized in polynomial time through abstraction of logarithmic or exponential terms and Handelman’s Theorem. A key application of our method is the worst-case analysis of recursive programs. While previous methods obtain worst-case polynomial bounds of the form O(n^k), where k is an integer, our polynomial time methods can synthesize bounds of the form O(n log n), as well as O(n^x), where x is not an integer. We show the applicability of our automated technique to obtain worst-case complexity of classical recursive algorithms such as (i) Merge-Sort, the divideand- conquer algorithm for the Closest-Pair problem, where we obtain O(n log n) worst-case bound, and (ii) Karatsuba’s algorithm for polynomial multiplication and Strassen’s algorithm for matrix multiplication, where we obtain O(n^x) bound, where x is not an integer and close to the best-known bounds for the respective algorithms. Finally, we present experimental results to demonstrate the effectiveness of our approach.}, author = {Anonymous, 1 and Anonymous, 2 and Anonymous, 3}, issn = {2664-1690}, pages = {26}, publisher = {IST Austria}, title = {{Termination and worst-case analysis of recursive programs}}, year = {2016}, } @misc{5447, abstract = {We consider the problem of developing automated techniques to aid the average-case complexity analysis of programs. Several classical textbook algorithms have quite efficient average-case complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., QUICK-SORT), or completely ineffective (e.g., COUPONCOLLECTOR). Since the main focus of average-case analysis is to obtain efficient bounds, we consider bounds that are either logarithmic, linear, or almost-linear (O(log n), O(n), O(n · log n), respectively, where n represents the size of the input). Our main contribution is a sound approach for deriving such average-case bounds for randomized recursive programs. Our approach is efficient (a simple linear-time algorithm), and it is based on (a) the analysis of recurrence relations induced by randomized algorithms, and (b) a guess-and-check technique. Our approach can infer the asymptotically optimal average-case bounds for classical randomized algorithms, including RANDOMIZED-SEARCH, QUICKSORT, QUICK-SELECT, COUPON-COLLECTOR, where the worstcase bounds are either inefficient (such as linear as compared to logarithmic of average-case, or quadratic as compared to linear or almost-linear of average-case), or ineffective. We have implemented our approach, and the experimental results show that we obtain the bounds efficiently for various classical algorithms.}, author = {Anonymous, 1 and Anonymous, 2 and Anonymous, 3}, issn = {2664-1690}, pages = {20}, publisher = {IST Austria}, title = {{Average-case analysis of programs: Automated recurrence analysis for almost-linear bounds}}, year = {2016}, } @misc{5448, abstract = {We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class. We introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence. 1. For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence. 2. For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence. Finally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes.}, author = {Anonymous, 1 and Anonymous, 2 and Anonymous, 3 and Anonymous, 4}, issn = {2664-1690}, pages = {20}, publisher = {IST Austria}, title = {{Data-centric dynamic partial order reduction}}, year = {2016}, }