@phdthesis{48, abstract = {The hippocampus is a key brain region for spatial memory and navigation and is needed at all stages of memory, including encoding, consolidation, and recall. Hippocampal place cells selectively discharge at specific locations of the environment to form a cognitive map of the space. During the rest period and sleep following spatial navigation and/or learning, the waking activity of the place cells is reactivated within high synchrony events. This reactivation is thought to be important for memory consolidation and stabilization of the spatial representations. The aim of my thesis was to directly test whether the reactivation content encoded in firing patterns of place cells is important for consolidation of spatial memories. In particular, I aimed to test whether, in cases when multiple spatial memory traces are acquired during learning, the specific disruption of the reactivation of a subset of these memories leads to the selective disruption of the corresponding memory traces or through memory interference the other learned memories are disrupted as well. In this thesis, using a modified cheeseboard paradigm and a closed-loop recording setup with feedback optogenetic stimulation, I examined how the disruption of the reactivation of specific spiking patterns affects consolidation of the corresponding memory traces. To obtain multiple distinctive memories, animals had to perform a spatial task in two distinct cheeseboard environments and the reactivation of spiking patterns associated with one of the environments (target) was disrupted after learning during four hours rest period using a real-time decoding method. This real-time decoding method was capable of selectively affecting the firing rates and cofiring correlations of the target environment-encoding cells. The selective disruption led to behavioural impairment in the memory tests after the rest periods in the target environment but not in the other undisrupted control environment. In addition, the map of the target environment was less stable in the impaired memory tests compared to the learning session before than the map of the control environment. However, when the animal relearned the task, the same map recurred in the target environment that was present during learning before the disruption. Altogether my work demonstrated that the reactivation content is important: assembly-related disruption of reactivation can lead to a selective memory impairment and deficiency in map stability. These findings indeed suggest that reactivated assembly patterns reflect processes associated with the consolidation of memory traces. }, author = {Gridchyn, Igor}, issn = {2663-337X}, pages = {104}, publisher = {Institute of Science and Technology Austria}, title = {{Reactivation content is important for consolidation of spatial memory}}, doi = {10.15479/AT:ISTA:th_1042}, year = {2018}, } @article{21, abstract = {Parvalbumin-positive (PV+) GABAergic interneurons in hippocampal microcircuits are thought to play a key role in several higher network functions, such as feedforward and feedback inhibition, network oscillations, and pattern separation. Fast lateral inhibition mediated by GABAergic interneurons may implement a winner-takes-all mechanism in the hippocampal input layer. However, it is not clear whether the functional connectivity rules of granule cells (GCs) and interneurons in the dentate gyrus are consistent with such a mechanism. Using simultaneous patch-clamp recordings from up to seven GCs and up to four PV+ interneurons in the dentate gyrus, we find that connectivity is structured in space, synapse-specific, and enriched in specific disynaptic motifs. In contrast to the neocortex, lateral inhibition in the dentate gyrus (in which a GC inhibits neighboring GCs via a PV+ interneuron) is ~ 10-times more abundant than recurrent inhibition (in which a GC inhibits itself). Thus, unique connectivity rules may enable the dentate gyrus to perform specific higher-order computations}, author = {Espinoza Martinez, Claudia and Guzmán, José and Zhang, Xiaomin and Jonas, Peter M}, journal = {Nature Communications}, number = {1}, publisher = {Nature Publishing Group}, title = {{Parvalbumin+ interneurons obey unique connectivity rules and establish a powerful lateral-inhibition microcircuit in dentate gyrus}}, doi = {10.1038/s41467-018-06899-3}, volume = {9}, year = {2018}, } @article{67, abstract = {Gene regulatory networks evolve through rewiring of individual components—that is, through changes in regulatory connections. However, the mechanistic basis of regulatory rewiring is poorly understood. Using a canonical gene regulatory system, we quantify the properties of transcription factors that determine the evolutionary potential for rewiring of regulatory connections: robustness, tunability and evolvability. In vivo repression measurements of two repressors at mutated operator sites reveal their contrasting evolutionary potential: while robustness and evolvability were positively correlated, both were in trade-off with tunability. Epistatic interactions between adjacent operators alleviated this trade-off. A thermodynamic model explains how the differences in robustness, tunability and evolvability arise from biophysical characteristics of repressor–DNA binding. The model also uncovers that the energy matrix, which describes how mutations affect repressor–DNA binding, encodes crucial information about the evolutionary potential of a repressor. The biophysical determinants of evolutionary potential for regulatory rewiring constitute a mechanistic framework for understanding network evolution.}, author = {Igler, Claudia and Lagator, Mato and Tkacik, Gasper and Bollback, Jonathan P and Guet, Calin C}, journal = {Nature Ecology and Evolution}, number = {10}, pages = {1633 -- 1643}, publisher = {Nature Publishing Group}, title = {{Evolutionary potential of transcription factors for gene regulatory rewiring}}, doi = {10.1038/s41559-018-0651-y}, volume = {2}, year = {2018}, } @misc{5585, abstract = {Mean repression values and standard error of the mean are given for all operator mutant libraries.}, author = {Igler, Claudia and Lagator, Mato and Tkacik, Gasper and Bollback, Jonathan P and Guet, Calin C}, publisher = {Institute of Science and Technology Austria}, title = {{Data for the paper Evolutionary potential of transcription factors for gene regulatory rewiring}}, doi = {10.15479/AT:ISTA:108}, year = {2018}, } @phdthesis{50, abstract = {The Wnt/planar cell polarity (Wnt/PCP) pathway determines planar polarity of epithelial cells in both vertebrates and invertebrates. The role that Wnt/PCP signaling plays in mesenchymal contexts, however, is only poorly understood. While previous studies have demonstrated the capacity of Wnt/PCP signaling to polarize and guide directed migration of mesenchymal cells, it remains unclear whether endogenous Wnt/PCP signaling performs these functions instructively, as it does in epithelial cells. Here we developed a light-switchable version of the Wnt/PCP receptor Frizzled 7 (Fz7) to unambiguously distinguish between an instructive and a permissive role of Wnt/PCP signaling for the directional collective migration of mesendoderm progenitor cells during zebrafish gastrulation. We show that prechordal plate (ppl) cell migration is defective in maternal-zygotic fz7a and fz7b (MZ fz7a,b) double mutant embryos, and that Fz7 functions cell-autonomously in this process by promoting ppl cell protrusion formation and directed migration. We further show that local activation of Fz7 can direct ppl cell migration both in vitro and in vivo. Surprisingly, however, uniform Fz7 activation is sufficient to fully rescue the ppl cell migration defect in MZ fz7a,b mutant embryos, indicating that Wnt/PCP signaling functions permissively rather than instructively in directed mesendoderm cell migration during zebrafish gastrulation.}, author = {Capek, Daniel}, issn = {2663-337X}, pages = {95}, publisher = {Institute of Science and Technology Austria}, title = {{Optogenetic Frizzled 7 reveals a permissive function of Wnt/PCP signaling in directed mesenchymal cell migration}}, doi = {10.15479/AT:ISTA:TH_1031}, year = {2018}, } @phdthesis{6266, abstract = {A major challenge in neuroscience research is to dissect the circuits that orchestrate behavior in health and disease. Proteins from a wide range of non-mammalian species, such as microbial opsins, have been successfully transplanted to specific neuronal targets to override their natural communication patterns. The goal of our work is to manipulate synaptic communication in a manner that closely incorporates the functional intricacies of synapses by preserving temporal encoding (i.e. the firing pattern of the presynaptic neuron) and connectivity (i.e. target specific synapses rather than specific neurons). Our strategy to achieve this goal builds on the use of non-mammalian transplants to create a synthetic synapse. The mode of modulation comes from pre-synaptic uptake of a synthetic neurotransmitter (SN) into synaptic vesicles by means of a genetically targeted transporter selective for the SN. Upon natural vesicular release, exposure of the SN to the synaptic cleft will modify the post-synaptic potential through an orthogonal ligand gated ion channel. To achieve this goal we have functionally characterized a mixed cationic methionine-gated ion channel from Arabidopsis thaliana, designed a method to functionally characterize a synthetic transporter in isolated synaptic vesicles without the need for transgenic animals, identified and extracted multiple prokaryotic uptake systems that are substrate specific for methionine (Met), and established a primary/cell line co-culture system that would allow future combinatorial testing of this orthogonal transmitter-transporter-channel trifecta. Synthetic synapses will provide a unique opportunity to manipulate synaptic communication while maintaining the electrophysiological integrity of the pre-synaptic cell. In this way, information may be preserved that was generated in upstream circuits and that could be essential for concerted function and information processing. }, author = {Mckenzie, Catherine}, issn = {2663-337X}, pages = {95}, publisher = {Institute of Science and Technology Austria}, title = {{Design and characterization of methods and biological components to realize synthetic neurotransmission }}, doi = {10.15479/at:ista:th_1055}, year = {2018}, } @article{5816, abstract = {Solid-state qubit manipulation and read-out fidelities are reaching fault-tolerance, but quantum error correction requires millions of physical qubits and therefore a scalable quantum computer architecture. To solve signal-line bandwidth and fan-out problems, microwave sources required for qubit manipulation might be embedded close to the qubit chip, typically operating at temperatures below 4 K. Here, we perform the first low temperature measurements of a 130 nm BiCMOS based SiGe voltage controlled oscillator at cryogenic temperature. We determined the frequency and output power dependence on temperature and magnetic field up to 5 T and measured the temperature influence on its noise performance. The device maintains its full functionality from 300 K to 4 K. The carrier frequency at 4 K increases by 3% with respect to the carrier frequency at 300 K, and the output power at 4 K increases by 10 dB relative to the output power at 300 K. The frequency tuning range of approximately 20% remains unchanged between 300 K and 4 K. In an in-plane magnetic field of 5 T, the carrier frequency shifts by only 0.02% compared to the frequency at zero magnetic field.}, author = {Hollmann, Arne and Jirovec, Daniel and Kucharski, Maciej and Kissinger, Dietmar and Fischer, Gunter and Schreiber, Lars R.}, issn = {0034-6748}, journal = {Review of Scientific Instruments}, number = {11}, publisher = {AIP Publishing}, title = {{30 GHz-voltage controlled oscillator operating at 4 K}}, doi = {10.1063/1.5038258}, volume = {89}, year = {2018}, } @article{442, abstract = {The rapid auxin-triggered growth of the Arabidopsis hypocotyls involves the nuclear TIR1/AFB-Aux/IAA signaling and is accompanied by acidification of the apoplast and cell walls (Fendrych et al., 2016). Here, we describe in detail the method for analysis of the elongation and the TIR1/AFB-Aux/IAA-dependent auxin response in hypocotyl segments as well as the determination of relative values of the cell wall pH.}, author = {Li, Lanxin and Krens, Gabriel and Fendrych, Matyas and Friml, Jirí}, issn = {2331-8325}, journal = {Bio-protocol}, number = {1}, publisher = {Bio-protocol}, title = {{Real-time analysis of auxin response, cell wall pH and elongation in Arabidopsis thaliana Hypocotyls}}, doi = {10.21769/BioProtoc.2685}, volume = {8}, year = {2018}, } @article{2, abstract = {Indirect reciprocity explores how humans act when their reputation is at stake, and which social norms they use to assess the actions of others. A crucial question in indirect reciprocity is which social norms can maintain stable cooperation in a society. Past research has highlighted eight such norms, called “leading-eight” strategies. This past research, however, is based on the assumption that all relevant information about other population members is publicly available and that everyone agrees on who is good or bad. Instead, here we explore the reputation dynamics when information is private and noisy. We show that under these conditions, most leading-eight strategies fail to evolve. Those leading-eight strategies that do evolve are unable to sustain full cooperation.Indirect reciprocity is a mechanism for cooperation based on shared moral systems and individual reputations. It assumes that members of a community routinely observe and assess each other and that they use this information to decide who is good or bad, and who deserves cooperation. When information is transmitted publicly, such that all community members agree on each other’s reputation, previous research has highlighted eight crucial moral systems. These “leading-eight” strategies can maintain cooperation and resist invasion by defectors. However, in real populations individuals often hold their own private views of others. Once two individuals disagree about their opinion of some third party, they may also see its subsequent actions in a different light. Their opinions may further diverge over time. Herein, we explore indirect reciprocity when information transmission is private and noisy. We find that in the presence of perception errors, most leading-eight strategies cease to be stable. Even if a leading-eight strategy evolves, cooperation rates may drop considerably when errors are common. Our research highlights the role of reliable information and synchronized reputations to maintain stable moral systems.}, author = {Hilbe, Christian and Schmid, Laura and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak, Martin}, journal = {PNAS}, number = {48}, pages = {12241--12246}, publisher = {National Academy of Sciences}, title = {{Indirect reciprocity with private, noisy, and incomplete information}}, doi = {10.1073/pnas.1810565115}, volume = {115}, year = {2018}, } @phdthesis{395, abstract = {Autism spectrum disorders (ASD) are a group of genetic disorders often overlapping with other neurological conditions. Despite the remarkable number of scientific breakthroughs of the last 100 years, the treatment of neurodevelopmental disorders (e.g. autism spectrum disorder, intellectual disability, epilepsy) remains a great challenge. Recent advancements in geno mics, like whole-exome or whole-genome sequencing, have enabled scientists to identify numerous mutations underlying neurodevelopmental disorders. Given the few hundred risk genes that were discovered, the etiological variability and the heterogeneous phenotypic outcomes, the need for genotype -along with phenotype- based diagnosis of individual patients becomes a requisite. Driven by this rationale, in a previous study our group described mutations, identified via whole - exome sequencing, in the gene BCKDK – encoding for a key regulator of branched chain amin o acid (BCAA) catabolism - as a cause of ASD. Following up on the role of BCAAs, in the study described here we show that the solute carrier transporter 7a5 (SLC7A5), a large neutral amino acid transporter localized mainly at the blood brain barrier (BBB), has an essential role in maintaining normal levels of brain BCAAs. In mice, deletion of Slc7a5 from the endothelial cells of the BBB leads to atypical brain amino acid profile, abnormal mRNA translation and severe neurolo gical abnormalities. Additionally, deletion of Slc7a5 from the neural progenitor cell population leads to microcephaly. Interestingly, we demonstrate that BCAA intracerebroventricular administration ameliorates abnormal behaviors in adult mutant mice. Furthermore, whole - exome sequencing of patients diagnosed with neurological dis o r ders helped us identify several patients with autistic traits, microcephaly and motor delay carrying deleterious homozygous mutations in the SLC7A5 gene. In conclusion, our data elucidate a neurological syndrome defined by SLC7A5 mutations and support an essential role for t he BCAA s in human bra in function. Together with r ecent studies (described in chapter two) that have successfully made the transition into clinical practice, our findings on the role of B CAAs might have a crucial impact on the development of novel individualized therapeutic strategies for ASD. }, author = {Tarlungeanu, Dora-Clara}, issn = {2663-337X}, pages = {88}, publisher = {Institute of Science and Technology Austria}, title = {{The branched chain amino acids in autism spectrum disorders }}, doi = {10.15479/AT:ISTA:th_992}, year = {2018}, } @article{47, abstract = {Plant hormones as signalling molecules play an essential role in the control of plant growth and development. Typically, sites of hormonal action are usually distant from the site of biosynthesis thus relying on efficient transport mechanisms. Over the last decades, molecular identification of proteins and protein complexes involved in hormonal transport has started. Advanced screens for genes involved in hormonal transport in combination with transport assays using heterologous systems such as yeast, insect, or tobacco BY2 cells or Xenopus oocytes provided important insights into mechanisms underlying distribution of hormones in plant body and led to identification of principal transporters for each hormone. This review gives a short overview of the mechanisms of hormonal transport and transporters identified in Arabidopsis thaliana.}, author = {Abualia, Rashed and Benková, Eva and Lacombe, Benoît}, journal = {Advances in Botanical Research}, pages = {115 -- 138}, publisher = {Elsevier}, title = {{Transporters and mechanisms of hormone transport in arabidopsis}}, doi = {10.1016/bs.abr.2018.09.007}, volume = {87}, year = {2018}, } @phdthesis{323, abstract = {In the here presented thesis, we explore the role of branched actin networks in cell migration and antigen presentation, the two most relevant processes in dendritic cell biology. Branched actin networks construct lamellipodial protrusions at the leading edge of migrating cells. These are typically seen as adhesive structures, which mediate force transduction to the extracellular matrix that leads to forward locomotion. We ablated Arp2/3 nucleation promoting factor WAVE in DCs and found that the resulting cells lack lamellipodial protrusions. Instead, depending on the maturation state, one or multiple filopodia were formed. By challenging these cells in a variety of migration assays we found that lamellipodial protrusions are dispensable for the locomotion of leukocytes and actually dampen the speed of migration. However, lamellipodia are critically required to negotiate complex environments that DCs experience while they travel to the next draining lymph node. Taken together our results suggest that leukocyte lamellipodia have rather a sensory- than a force transducing function. Furthermore, we show for the first time structure and dynamics of dendritic cell F-actin at the immunological synapse with naïve T cells. Dendritic cell F-actin appears as dynamic foci that are nucleated by the Arp2/3 complex. WAVE ablated dendritic cells show increased membrane tension, leading to an altered ultrastructure of the immunological synapse and severe T cell priming defects. These results point towards a previously unappreciated role of the cellular mechanics of dendritic cells in T cell activation. Additionally, we present a novel cell culture based system for the differentiation of dendritic cells from conditionally immortalized hematopoietic precursors. These precursor cells are genetically tractable via the CRISPR/Cas9 system while they retain their ability to differentiate into highly migratory dendritic cells and other immune cells. This will foster the study of all aspects of dendritic cell biology and beyond. }, author = {Leithner, Alexander F}, issn = {2663-337X}, pages = {99}, publisher = {Institute of Science and Technology Austria}, title = {{Branched actin networks in dendritic cell biology}}, doi = {10.15479/AT:ISTA:th_998}, year = {2018}, } @article{449, abstract = {Auxin is unique among plant hormones due to its directional transport that is mediated by the polarly distributed PIN auxin transporters at the plasma membrane. The canalization hypothesis proposes that the auxin feedback on its polar flow is a crucial, plant-specific mechanism mediating multiple self-organizing developmental processes. Here, we used the auxin effect on the PIN polar localization in Arabidopsis thaliana roots as a proxy for the auxin feedback on the PIN polarity during canalization. We performed microarray experiments to find regulators of this process that act downstream of auxin. We identified genes that were transcriptionally regulated by auxin in an AXR3/IAA17- and ARF7/ARF19-dependent manner. Besides the known components of the PIN polarity, such as PID and PIP5K kinases, a number of potential new regulators were detected, among which the WRKY23 transcription factor, which was characterized in more detail. Gain- and loss-of-function mutants confirmed a role for WRKY23 in mediating the auxin effect on the PIN polarity. Accordingly, processes requiring auxin-mediated PIN polarity rearrangements, such as vascular tissue development during leaf venation, showed a higher WRKY23 expression and required the WRKY23 activity. Our results provide initial insights into the auxin transcriptional network acting upstream of PIN polarization and, potentially, canalization-mediated plant development.}, author = {Prat, Tomas and Hajny, Jakub and Grunewald, Wim and Vasileva, Mina K and Molnar, Gergely and Tejos, Ricardo and Schmid, Markus and Sauer, Michael and Friml, Jirí}, journal = {PLoS Genetics}, number = {1}, publisher = {Public Library of Science}, title = {{WRKY23 is a component of the transcriptional network mediating auxin feedback on PIN polarity}}, doi = {10.1371/journal.pgen.1007177}, volume = {14}, year = {2018}, } @article{191, abstract = {Intercellular distribution of the plant hormone auxin largely depends on the polar subcellular distribution of the plasma membrane PIN-FORMED (PIN) auxin transporters. PIN polarity switches in response to different developmental and environmental signals have been shown to redirect auxin fluxes mediating certain developmental responses. PIN phosphorylation at different sites and by different kinases is crucial for PIN function. Here we investigate the role of PIN phosphorylation during gravitropic response. Loss- and gain-of-function mutants in PINOID and related kinases but not in D6PK kinase as well as mutations mimicking constitutive dephosphorylated or phosphorylated status of two clusters of predicted phosphorylation sites partially disrupted PIN3 phosphorylation and caused defects in gravitropic bending in roots and hypocotyls. In particular, they impacted PIN3 polarity rearrangements in response to gravity and during feed-back regulation by auxin itself. Thus PIN phosphorylation, besides regulating transport activity and apical-basal targeting, is also important for the rapid polarity switches in response to environmental and endogenous signals.}, author = {Grones, Peter and Abas, Melinda F and Hajny, Jakub and Jones, Angharad and Waidmann, Sascha and Kleine Vehn, Jürgen and Friml, Jirí}, journal = {Scientific Reports}, number = {1}, publisher = {Springer}, title = {{PID/WAG-mediated phosphorylation of the Arabidopsis PIN3 auxin transporter mediates polarity switches during gravitropism}}, doi = {10.1038/s41598-018-28188-1}, volume = {8}, year = {2018}, } @article{5914, abstract = {With the advent of optogenetics, it became possible to change the activity of a targeted population of neurons in a temporally controlled manner. To combine the advantages of 60-channel in vivo tetrode recording and laser-based optogenetics, we have developed a closed-loop recording system that allows for the actual electrophysiological signal to be used as a trigger for the laser light mediating the optogenetic intervention. We have optimized the weight, size, and shape of the corresponding implant to make it compatible with the size, force, and movements of a behaving mouse, and we have shown that the system can efficiently block sharp wave ripple (SWR) events using those events themselves as a trigger. To demonstrate the full potential of the optogenetic recording system we present a pilot study addressing the contribution of SWR events to learning in a complex behavioral task.}, author = {Rangel Guerrero, Dámaris K and Donnett, James G. and Csicsvari, Jozsef L and Kovács, Krisztián}, journal = {eNeuro}, number = {4}, publisher = {Society for Neuroscience}, title = {{Tetrode recording from the hippocampus of behaving mice coupled with four-point-irradiation closed-loop optogenetics: A technique to study the contribution of Hippocampal SWR events to learning}}, doi = {10.1523/ENEURO.0087-18.2018}, volume = {5}, year = {2018}, } @inproceedings{66, abstract = {Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payo games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions.}, author = {Chatterjee, Krishnendu and Goharshady, Amir and Ibsen-Jensen, Rasmus and Velner, Yaron}, isbn = {978-3-95977-087-3}, location = {Beijing, China}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Ergodic mean-payoff games for the analysis of attacks in crypto-currencies}}, doi = {10.4230/LIPIcs.CONCUR.2018.11}, volume = {118}, year = {2018}, } @inproceedings{311, abstract = {Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and transfer assets of considerable value (in the form of crypto-currency like Bitcoin). Hence, it is crucial that their implementation is bug-free. We identify the utility (or expected payoff) of interacting with such smart contracts as the basic and canonical quantitative property for such contracts. We present a framework for such quantitative analysis of smart contracts. Such a formal framework poses new and novel research challenges in programming languages, as it requires modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior and modeling utilities which are not specified as standard temporal properties such as safety and termination. While game-theoretic incentives have been analyzed in the security community, their analysis has been restricted to the very special case of stateless games. However, to analyze smart contracts, stateful analysis is required as it must account for the different program states of the protocol. Our main contributions are as follows: we present (i)~a simplified programming language for smart contracts; (ii)~an automatic translation of the programs to state-based games; (iii)~an abstraction-refinement approach to solve such games; and (iv)~experimental results on real-world-inspired smart contracts.}, author = {Chatterjee, Krishnendu and Goharshady, Amir and Velner, Yaron}, location = {Thessaloniki, Greece}, pages = {739 -- 767}, publisher = {Springer}, title = {{Quantitative analysis of smart contracts}}, doi = {10.1007/978-3-319-89884-1_26}, volume = {10801}, year = {2018}, } @inproceedings{6340, abstract = {We present a secure approach for maintaining andreporting credit history records on the Blockchain. Our ap-proach removes third-parties such as credit reporting agen-cies from the lending process and replaces them with smartcontracts. This allows customers to interact directly with thelenders or banks while ensuring the integrity, unmalleabilityand privacy of their credit data. Additionally, each customerhas full control over complete or selective disclosure of hercredit records, eliminating the risk of privacy violations or databreaches. Moreover, our approach provides strong guaranteesfor the lenders as well. A lender can check both correctness andcompleteness of the credit data disclosed to her. This is the firstapproach that can perform all credit reporting tasks withouta central authority or changing the financial mechanisms*.}, author = {Goharshady, Amir Kafshdar and Behrouz, Ali and Chatterjee, Krishnendu}, booktitle = {Proceedings of the IEEE International Conference on Blockchain}, isbn = {978-1-5386-7975-3 }, location = {Halifax, Canada}, pages = {1343--1348}, publisher = {IEEE}, title = {{Secure Credit Reporting on the Blockchain}}, doi = {10.1109/Cybermatics_2018.2018.00231}, year = {2018}, } @article{6009, abstract = {We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks. }, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Goharshady, Amir Kafshdar and Pavlogiannis, Andreas}, issn = {0164-0925}, journal = {ACM Transactions on Programming Languages and Systems}, number = {3}, publisher = {Association for Computing Machinery}, title = {{Algorithms for algebraic path properties in concurrent systems of constant treewidth components}}, doi = {10.1145/3210257}, volume = {40}, year = {2018}, } @inproceedings{5977, abstract = {We consider the stochastic shortest path (SSP)problem for succinct Markov decision processes(MDPs), where the MDP consists of a set of vari-ables, and a set of nondeterministic rules that up-date the variables. First, we show that several ex-amples from the AI literature can be modeled assuccinct MDPs. Then we present computationalapproaches for upper and lower bounds for theSSP problem: (a) for computing upper bounds, ourmethod is polynomial-time in the implicit descrip-tion of the MDP; (b) for lower bounds, we present apolynomial-time (in the size of the implicit descrip-tion) reduction to quadratic programming. Our ap-proach is applicable even to infinite-state MDPs.Finally, we present experimental results to demon-strate the effectiveness of our approach on severalclassical examples from the AI literature.}, author = {Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir and Okati, Nastaran}, booktitle = {Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence}, isbn = {9780999241127}, issn = {1045-0823}, location = {Stockholm, Sweden}, pages = {4700--4707}, publisher = {IJCAI}, title = {{Computational approaches for stochastic shortest path on succinct MDPs}}, doi = {10.24963/ijcai.2018/653}, volume = {2018}, year = {2018}, }