@article{14402, abstract = {Alpha oscillations are a distinctive feature of the awake resting state of the human brain. However, their functional role in resting-state neuronal dynamics remains poorly understood. Here we show that, during resting wakefulness, alpha oscillations drive an alternation of attenuation and amplification bouts in neural activity. Our analysis indicates that inhibition is activated in pulses that last for a single alpha cycle and gradually suppress neural activity, while excitation is successively enhanced over a few alpha cycles to amplify neural activity. Furthermore, we show that long-term alpha amplitude fluctuations—the “waxing and waning” phenomenon—are an attenuation-amplification mechanism described by a power-law decay of the activity rate in the “waning” phase. Importantly, we do not observe such dynamics during non-rapid eye movement (NREM) sleep with marginal alpha oscillations. The results suggest that alpha oscillations modulate neural activity not only through pulses of inhibition (pulsed inhibition hypothesis) but also by timely enhancement of excitation (or disinhibition).}, author = {Lombardi, Fabrizio and Herrmann, Hans J. and Parrino, Liborio and Plenz, Dietmar and Scarpetta, Silvia and Vaudano, Anna Elisabetta and De Arcangelis, Lucilla and Shriki, Oren}, issn = {2211-1247}, journal = {Cell Reports}, number = {10}, publisher = {Elsevier}, title = {{Beyond pulsed inhibition: Alpha oscillations modulate attenuation and amplification of neural activity in the awake resting state}}, doi = {10.1016/j.celrep.2023.113162}, volume = {42}, year = {2023}, } @article{13267, abstract = {Three-dimensional (3D) reconstruction of living brain tissue down to an individual synapse level would create opportunities for decoding the dynamics and structure–function relationships of the brain’s complex and dense information processing network; however, this has been hindered by insufficient 3D resolution, inadequate signal-to-noise ratio and prohibitive light burden in optical imaging, whereas electron microscopy is inherently static. Here we solved these challenges by developing an integrated optical/machine-learning technology, LIONESS (live information-optimized nanoscopy enabling saturated segmentation). This leverages optical modifications to stimulated emission depletion microscopy in comprehensively, extracellularly labeled tissue and previous information on sample structure via machine learning to simultaneously achieve isotropic super-resolution, high signal-to-noise ratio and compatibility with living tissue. This allows dense deep-learning-based instance segmentation and 3D reconstruction at a synapse level, incorporating molecular, activity and morphodynamic information. LIONESS opens up avenues for studying the dynamic functional (nano-)architecture of living brain tissue.}, author = {Velicky, Philipp and Miguel Villalba, Eder and Michalska, Julia M and Lyudchik, Julia and Wei, Donglai and Lin, Zudi and Watson, Jake and Troidl, Jakob and Beyer, Johanna and Ben Simon, Yoav and Sommer, Christoph M and Jahr, Wiebke and Cenameri, Alban and Broichhagen, Johannes and Grant, Seth G.N. and Jonas, Peter M and Novarino, Gaia and Pfister, Hanspeter and Bickel, Bernd and Danzl, Johann G}, issn = {1548-7105}, journal = {Nature Methods}, pages = {1256--1265}, publisher = {Springer Nature}, title = {{Dense 4D nanoscale reconstruction of living brain tissue}}, doi = {10.1038/s41592-023-01936-6}, volume = {20}, year = {2023}, } @misc{14502, abstract = {A precise quantitative description of the ultrastructural characteristics underlying biological mechanisms is often key to their understanding. This is particularly true for dynamic extra- and intracellular filamentous assemblies, playing a role in cell motility, cell integrity, cytokinesis, tissue formation and maintenance. For example, genetic manipulation or modulation of actin regulatory proteins frequently manifests in changes of the morphology, dynamics, and ultrastructural architecture of actin filament-rich cell peripheral structures, such as lamellipodia or filopodia. However, the observed ultrastructural effects often remain subtle and require sufficiently large datasets for appropriate quantitative analysis. The acquisition of such large datasets has been enabled by recent advances in high-throughput cryo-electron tomography (cryo-ET) methods. This also necessitates the development of complementary approaches to maximize the extraction of relevant biological information. We have developed a computational toolbox for the semi-automatic quantification of segmented and vectorized fila- mentous networks from pre-processed cryo-electron tomograms, facilitating the analysis and cross-comparison of multiple experimental conditions. GUI-based components simplify the processing of data and allow users to obtain a large number of ultrastructural parameters describing filamentous assemblies. We demonstrate the feasibility of this workflow by analyzing cryo-ET data of untreated and chemically perturbed branched actin filament networks and that of parallel actin filament arrays. In principle, the computational toolbox presented here is applicable for data analysis comprising any type of filaments in regular (i.e. parallel) or random arrangement. We show that it can ease the identification of key differences between experimental groups and facilitate the in-depth analysis of ultrastructural data in a time-efficient manner.}, author = {Dimchev, Georgi A and Amiri, Behnam and Fäßler, Florian and Falcke, Martin and Schur, Florian KM}, keywords = {cryo-electron tomography, actin cytoskeleton, toolbox}, publisher = {Institute of Science and Technology Austria}, title = {{Computational toolbox for ultrastructural quantitative analysis of filament networks in cryo-ET data}}, doi = {10.15479/AT:ISTA:14502}, year = {2023}, } @article{13212, abstract = {Auxin is the major plant hormone regulating growth and development (Friml, 2022). Forward genetic approaches in the model plant Arabidopsis thaliana have identified major components of auxin signalling and established the canonical mechanism mediating transcriptional and thus developmental reprogramming. In this textbook view, TRANSPORT INHIBITOR RESPONSE 1 (TIR1)/AUXIN-SIGNALING F-BOX (AFBs) are auxin receptors, which act as F-box subunits determining the substrate specificity of the Skp1-Cullin1-F box protein (SCF) type E3 ubiquitin ligase complex. Auxin acts as a “molecular glue” increasing the affinity between TIR1/AFBs and the Aux/IAA repressors. Subsequently, Aux/IAAs are ubiquitinated and degraded, thus releasing auxin transcription factors from their repression making them free to mediate transcription of auxin response genes (Yu et al., 2022). Nonetheless, accumulating evidence suggests existence of rapid, non-transcriptional responses downstream of TIR1/AFBs such as auxin-induced cytosolic calcium (Ca2+) transients, plasma membrane depolarization and apoplast alkalinisation, all converging on the process of root growth inhibition and root gravitropism (Li et al., 2022). Particularly, these rapid responses are mostly contributed by predominantly cytosolic AFB1, while the long-term growth responses are mediated by mainly nuclear TIR1 and AFB2-AFB5 (Li et al., 2021; Prigge et al., 2020; Serre et al., 2021). How AFB1 conducts auxin-triggered rapid responses and how it is different from TIR1 and AFB2-AFB5 remains elusive. Here, we compare the roles of TIR1 and AFB1 in transcriptional and rapid responses by modulating their subcellular localization in Arabidopsis and by testing their ability to mediate transcriptional responses when part of the minimal auxin circuit reconstituted in yeast.}, author = {Chen, Huihuang and Li, Lanxin and Zou, Minxia and Qi, Linlin and Friml, Jiří}, issn = {1674-2052}, journal = {Molecular Plant}, number = {7}, pages = {1117--1119}, publisher = {Elsevier}, title = {{Distinct functions of TIR1 and AFB1 receptors in auxin signalling.}}, doi = {10.1016/j.molp.2023.06.007}, volume = {16}, year = {2023}, } @article{13209, abstract = {The phytohormone auxin plays central roles in many growth and developmental processes in plants. Development of chemical tools targeting the auxin pathway is useful for both plant biology and agriculture. Here we reveal that naproxen, a synthetic compound with anti-inflammatory activity in humans, acts as an auxin transport inhibitor targeting PIN-FORMED (PIN) transporters in plants. Physiological experiments indicate that exogenous naproxen treatment affects pleiotropic auxin-regulated developmental processes. Additional cellular and biochemical evidence indicates that naproxen suppresses auxin transport, specifically PIN-mediated auxin efflux. Moreover, biochemical and structural analyses confirm that naproxen binds directly to PIN1 protein via the same binding cavity as the indole-3-acetic acid substrate. Thus, by combining cellular, biochemical, and structural approaches, this study clearly establishes that naproxen is a PIN inhibitor and elucidates the underlying mechanisms. Further use of this compound may advance our understanding of the molecular mechanisms of PIN-mediated auxin transport and expand our toolkit in auxin biology and agriculture.}, author = {Xia, Jing and Kong, Mengjuan and Yang, Zhisen and Sun, Lianghanxiao and Peng, Yakun and Mao, Yanbo and Wei, Hong and Ying, Wei and Gao, Yongxiao and Friml, Jiří and Weng, Jianping and Liu, Xin and Sun, Linfeng and Tan, Shutang}, issn = {2590-3462}, journal = {Plant Communications}, number = {6}, publisher = {Elsevier}, title = {{Chemical inhibition of Arabidopsis PIN-FORMED auxin transporters by the anti-inflammatory drug naproxen}}, doi = {10.1016/j.xplc.2023.100632}, volume = {4}, year = {2023}, } @inproceedings{13162, author = {Elefante, Stefano and Stadlbauer, Stephan and Alexander, Michael F and Schlögl, Alois}, booktitle = {ASHPC23 - Austrian-Slovenian HPC Meeting 2023}, location = {Maribor, Slovenia}, pages = {42--42}, publisher = {EuroCC Austria}, title = {{Cryo-EM software packages: A sys-admins point of view}}, year = {2023}, } @inproceedings{13161, author = {Schlögl, Alois and Elefante, Stefano and Hodirnau, Victor-Valentin}, booktitle = {ASHPC23 - Austrian-Slovenian HPC Meeting 2023}, location = {Maribor, Slovenia}, pages = {59--59}, publisher = {EuroCC Austria}, title = {{Running Windows-applications on a Linux HPC cluster using WINE}}, year = {2023}, } @article{13268, abstract = {We give a simple argument to prove Nagai’s conjecture for type II degenerations of compact hyperkähler manifolds and cohomology classes of middle degree. Under an additional assumption, the techniques yield the conjecture in arbitrary degree. This would complete the proof of Nagai’s conjecture in general, as it was proved already for type I degenerations by Kollár, Laza, Saccà, and Voisin [10] and independently by Soldatenkov [18], while it is immediate for type III degenerations. Our arguments are close in spirit to a recent paper by Harder [8] proving similar results for the restrictive class of good degenerations.}, author = {Huybrechts, D. and Mauri, Mirko}, issn = {1945-001X}, journal = {Mathematical Research Letters}, number = {1}, pages = {125--141}, publisher = {International Press of Boston}, title = {{On type II degenerations of hyperkähler manifolds}}, doi = {10.4310/mrl.2023.v30.n1.a6}, volume = {30}, year = {2023}, } @inproceedings{14609, abstract = {Distributed Key Generation (DKG) is a technique to bootstrap threshold cryptosystems without a trusted party. DKG is an essential building block to many decentralized protocols such as randomness beacons, threshold signatures, Byzantine consensus, and multiparty computation. While significant progress has been made recently, existing asynchronous DKG constructions are inefficient when the reconstruction threshold is larger than one-third of the total nodes. In this paper, we present a simple and concretely efficient asynchronous DKG (ADKG) protocol among n = 3t + 1 nodes that can tolerate up to t malicious nodes and support any reconstruction threshold ℓ ≥ t. Our protocol has an expected O(κn3) communication cost, where κ is the security parameter, and only assumes the hardness of the Discrete Logarithm. The core ingredient of our ADKG protocol is an asynchronous protocol to secret share a random polynomial of degree ℓ ≥ t, which has other applications, such as asynchronous proactive secret sharing and asynchronous multiparty computation. We implement our high-threshold ADKG protocol and evaluate it using a network of up to 128 geographically distributed nodes. Our evaluation shows that our high-threshold ADKG protocol reduces the running time by 90% and bandwidth usage by 80% over the state-of-the-art.}, author = {Das, Sourav and Xiang, Zhuolun and Kokoris Kogias, Eleftherios and Ren, Ling}, booktitle = {32nd USENIX Security Symposium}, isbn = {9781713879497}, location = {Anaheim, CA, United States}, pages = {5359--5376}, publisher = {Usenix Association}, title = {{Practical asynchronous high-threshold distributed key generation and distributed polynomial sampling}}, volume = {8}, year = {2023}, } @inproceedings{14718, abstract = {Binary decision diagrams (BDDs) are one of the fundamental data structures in formal methods and computer science in general. However, the performance of BDD-based algorithms greatly depends on memory latency due to the reliance on large hash tables and thus, by extension, on the speed of random memory access. This hinders the full utilisation of resources available on modern CPUs, since the absolute memory latency has not improved significantly for at least a decade. In this paper, we explore several implementation techniques that improve the performance of BDD manipulation either through enhanced memory locality or by partially eliminating random memory access. On a benchmark suite of 600+ BDDs derived from real-world applications, we demonstrate runtime that is comparable or better than parallelising the same operations on eight CPU cores. }, author = {Pastva, Samuel and Henzinger, Thomas A}, booktitle = {Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design}, isbn = {9783854480600}, location = {Ames, IA, United States}, pages = {122--131}, publisher = {TU Wien Academic Press}, title = {{Binary decision diagrams on modern hardware}}, doi = {10.34727/2023/isbn.978-3-85448-060-0_20}, year = {2023}, } @article{14799, abstract = {A round-robin study has been carried out to estimate the impact of the human element in small-angle scattering data analysis. Four corrected datasets were provided to participants ready for analysis. All datasets were measured on samples containing spherical scatterers, with two datasets in dilute dispersions and two from powders. Most of the 46 participants correctly identified the number of populations in the dilute dispersions, with half of the population mean entries within 1.5% and half of the population width entries within 40%. Due to the added complexity of the structure factor, far fewer people submitted answers on the powder datasets. For those that did, half of the entries for the means and widths were within 44 and 86%, respectively. This round-robin experiment highlights several causes for the discrepancies, for which solutions are proposed.}, author = {Pauw, Brian R. and Smales, Glen J. and Anker, Andy S. and Annadurai, Venkatasamy and Balazs, Daniel and Bienert, Ralf and Bouwman, Wim G. and Breßler, Ingo and Breternitz, Joachim and Brok, Erik S. and Bryant, Gary and Clulow, Andrew J. and Crater, Erin R. and De Geuser, Frédéric and Giudice, Alessandra Del and Deumer, Jérôme and Disch, Sabrina and Dutt, Shankar and Frank, Kilian and Fratini, Emiliano and Garcia, Paulo R.A.F. and Gilbert, Elliot P. and Hahn, Marc B. and Hallett, James and Hohenschutz, Max and Hollamby, Martin and Huband, Steven and Ilavsky, Jan and Jochum, Johanna K. and Juelsholt, Mikkel and Mansel, Bradley W. and Penttilä, Paavo and Pittkowski, Rebecca K. and Portale, Giuseppe and Pozzo, Lilo D. and Rochels, Leonhard and Rosalie, Julian M. and Saloga, Patrick E.J. and Seibt, Susanne and Smith, Andrew J. and Smith, Gregory N. and Spiering, Glenn A. and Stawski, Tomasz M. and Taché, Olivier and Thünemann, Andreas F. and Toth, Kristof and Whitten, Andrew E. and Wuttke, Joachim}, issn = {1600-5767}, journal = {Journal of Applied Crystallography}, number = {6}, pages = {1618--1629}, publisher = {International Union of Crystallography}, title = {{The human factor: Results of a small-angle scattering data analysis round robin}}, doi = {10.1107/S1600576723008324}, volume = {56}, year = {2023}, } @inproceedings{14243, abstract = {Two-player zero-sum "graph games" are central in logic, verification, and multi-agent systems. The game proceeds by placing a token on a vertex of a graph, and allowing the players to move it to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In "bidding games", however, the players have budgets and in each turn, an auction (bidding) determines which player moves the token. So far, bidding games have only been studied as full-information games. In this work we initiate the study of partial-information bidding games: we study bidding games in which a player's initial budget is drawn from a known probability distribution. We show that while for some bidding mechanisms and objectives, it is straightforward to adapt the results from the full-information setting to the partial-information setting, for others, the analysis is significantly more challenging, requires new techniques, and gives rise to interesting results. Specifically, we study games with "mean-payoff" objectives in combination with "poorman" bidding. We construct optimal strategies for a partially-informed player who plays against a fully-informed adversary. We show that, somewhat surprisingly, the "value" under pure strategies does not necessarily exist in such games.}, author = {Avni, Guy and Jecker, Ismael R and Zikelic, Dorde}, booktitle = {Proceedings of the 37th AAAI Conference on Artificial Intelligence}, isbn = {9781577358800}, location = {Washington, DC, United States}, number = {5}, pages = {5464--5471}, publisher = {AAAI Press}, title = {{Bidding graph games with partially-observable budgets}}, doi = {10.1609/aaai.v37i5.25679}, volume = {37}, year = {2023}, } @inproceedings{15364, abstract = {Clustering is a fundamental problem in unsupervised machine learning with many applications in data analysis. Popular clustering algorithms such as Lloyd's algorithm and k-means++ can make Ω(ndk) time when clustering n points in a d-dimensional space (represented by an n×d matrix X) into k clusters. On massive datasets with moderate to large k, the multiplicative k factor can become very expensive. We introduce a simple randomized clustering algorithm that provably runs in expected time O(nnz(X)+nlogn) for arbitrary k. Here nnz(X) is the total number of non-zero entries in the input dataset X, which is upper bounded by nd and can be significantly smaller for sparse datasets. We prove that our algorithm achieves approximation ratio ˜O(k4) on any input dataset for the k-means objective, and our experiments show that the quality of the clusters found by our algorithm is usually much better than this worst-case bound. We use our algorithm for k-means clustering and for coreset construction; our experiments show that it gives a new tradeoff between running time and cluster quality compared to previous state-of-the-art methods for these tasks. Our theoretical analysis is based on novel results of independent interest. We show that the approximation ratio achieved after a random one-dimensional projection can be lifted to the original points and that k-means++ seeding can be implemented in expected time O(nlogn) in one dimension.}, author = {Charikar, Moses and Hu, Lunjia and Henzinger, Monika H and Vötsch, Maximilian and Waingarten, Erik}, booktitle = {37th Conference on Neural Information Processing Systems}, issn = {1049-5258}, location = {New Orleans, LA, United States}, publisher = {Neural Information Processing Systems Foundation}, title = {{Simple, scalable and effective clustering via one-dimensional projections}}, volume = {36}, year = {2023}, } @inproceedings{15363, abstract = {Knowledge distillation is a popular approach for enhancing the performance of "student" models, with lower representational capacity, by taking advantage of more powerful "teacher" models. Despite its apparent simplicity, the underlying mechanics behind knowledge distillation (KD) are not yet fully understood. In this work, we shed new light on the inner workings of this method, by examining it from an optimization perspective. Specifically, we show that, in the context of linear and deep linear models, KD can be interpreted as a novel type of stochastic variance reduction mechanism. We provide a detailed convergence analysis of the resulting dynamics, which hold under standard assumptions for both strongly-convex and non-convex losses, showing that KD acts as a form of \emph{partial variance reduction}, which can reduce the stochastic gradient noise, but may not eliminate it completely, depending on the properties of the teacher'' model. Our analysis puts further emphasis on the need for careful parametrization of KD, in particular w.r.t. the weighting of the distillation loss, and is validated empirically on both linear models and deep neural networks.}, author = {Safaryan, Mher and Peste, Elena-Alexandra and Alistarh, Dan-Adrian}, booktitle = {36th Conference on Neural Information Processing Systems}, issn = {1049-5258}, location = {New Orleans, LA, United States}, publisher = {Neural Information Processing Systems Foundation}, title = {{Knowledge distillation performs partial variance reduction}}, volume = {36}, year = {2023}, } @inproceedings{15023, abstract = {Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph’s sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.}, author = {Zikelic, Dorde and Lechner, Mathias and Verma, Abhinav and Chatterjee, Krishnendu and Henzinger, Thomas A}, booktitle = {37th Conference on Neural Information Processing Systems}, issn = {1049-5258}, location = {New Orleans, LO, United States}, publisher = {Neural Information Processing Systems Foundation}, title = {{Compositional policy learning in stochastic control systems with formal guarantees}}, year = {2023}, } @inproceedings{14921, abstract = {Neural collapse (NC) refers to the surprising structure of the last layer of deep neural networks in the terminal phase of gradient descent training. Recently, an increasing amount of experimental evidence has pointed to the propagation of NC to earlier layers of neural networks. However, while the NC in the last layer is well studied theoretically, much less is known about its multi-layered counterpart - deep neural collapse (DNC). In particular, existing work focuses either on linear layers or only on the last two layers at the price of an extra assumption. Our paper fills this gap by generalizing the established analytical framework for NC - the unconstrained features model - to multiple non-linear layers. Our key technical contribution is to show that, in a deep unconstrained features model, the unique global optimum for binary classification exhibits all the properties typical of DNC. This explains the existing experimental evidence of DNC. We also empirically show that (i) by optimizing deep unconstrained features models via gradient descent, the resulting solution agrees well with our theory, and (ii) trained networks recover the unconstrained features suitable for the occurrence of DNC, thus supporting the validity of this modeling principle.}, author = {Súkeník, Peter and Mondelli, Marco and Lampert, Christoph}, booktitle = {37th Conference on Neural Information Processing Systems}, issn = {1049-5258}, location = {New Orleans, LA, United States}, publisher = {Neural Information Processing Systems Foundation}, title = {{Deep neural collapse is provably optimal for the deep unconstrained features model}}, year = {2023}, } @inproceedings{14260, abstract = {This paper presents Lincheck, a new practical and user-friendly framework for testing concurrent algorithms on the Java Virtual Machine (JVM). Lincheck provides a simple and declarative way to write concurrent tests: instead of describing how to perform the test, users specify what to test by declaring all the operations to examine; the framework automatically handles the rest. As a result, tests written with Lincheck are concise and easy to understand. The framework automatically generates a set of concurrent scenarios, examines them using stress-testing or bounded model checking, and verifies that the results of each invocation are correct. Notably, if an error is detected via model checking, Lincheck provides an easy-to-follow trace to reproduce it, significantly simplifying the bug investigation. To the best of our knowledge, Lincheck is the first production-ready tool on the JVM that offers such a simple way of writing concurrent tests, without requiring special skills or expertise. We successfully integrated Lincheck in the development process of several large projects, such as Kotlin Coroutines, and identified new bugs in popular concurrency libraries, such as a race in Java’s standard ConcurrentLinkedDeque and a liveliness bug in Java’s AbstractQueuedSynchronizer framework, which is used in most of the synchronization primitives. We believe that Lincheck can significantly improve the quality and productivity of concurrent algorithms research and development and become the state-of-the-art tool for checking their correctness.}, author = {Koval, Nikita and Fedorov, Alexander and Sokolova, Maria and Tsitelov, Dmitry and Alistarh, Dan-Adrian}, booktitle = {35th International Conference on Computer Aided Verification}, isbn = {9783031377051}, issn = {1611-3349}, location = {Paris, France}, pages = {156--169}, publisher = {Springer Nature}, title = {{Lincheck: A practical framework for testing concurrent data structures on JVM}}, doi = {10.1007/978-3-031-37706-8_8}, volume = {13964}, year = {2023}, } @inproceedings{14259, abstract = {We provide a learning-based technique for guessing a winning strategy in a parity game originating from an LTL synthesis problem. A cheaply obtained guess can be useful in several applications. Not only can the guessed strategy be applied as best-effort in cases where the game’s huge size prohibits rigorous approaches, but it can also increase the scalability of rigorous LTL synthesis in several ways. Firstly, checking whether a guessed strategy is winning is easier than constructing one. Secondly, even if the guess is wrong in some places, it can be fixed by strategy iteration faster than constructing one from scratch. Thirdly, the guess can be used in on-the-fly approaches to prioritize exploration in the most fruitful directions. In contrast to previous works, we (i) reflect the highly structured logical information in game’s states, the so-called semantic labelling, coming from the recent LTL-to-automata translations, and (ii) learn to reflect it properly by learning from previously solved games, bringing the solving process closer to human-like reasoning.}, author = {Kretinsky, Jan and Meggendorfer, Tobias and Prokop, Maximilian and Rieder, Sabine}, booktitle = {35th International Conference on Computer Aided Verification}, isbn = {9783031377051}, issn = {1611-3349}, location = {Paris, France}, pages = {390--414}, publisher = {Springer Nature}, title = {{Guessing winning policies in LTL synthesis by semantic learning}}, doi = {10.1007/978-3-031-37706-8_20}, volume = {13964}, year = {2023}, } @misc{14995, abstract = {Lincheck is a new practical and user-friendly framework for testing concurrent data structures on the Java Virtual Machine (JVM). It provides a simple and declarative way to write concurrent tests. Instead of describing how to perform the test, users specify what to test by declaring all the operations to examine; the framework automatically handles the rest. As a result, tests written with Lincheck are concise and easy to understand. The artifact presents a collection of Lincheck tests that discover new bugs in popular libraries and implementations from the concurrency literature -- they are listed in Table 1, Section 3. To evaluate the performance of Lincheck analysis, the collection of tests also includes those which check correct data structures and, thus, always succeed. Similarly to Table 2, Section 3, the experiments demonstrate the reasonable time to perform a test. Finally, Lincheck provides user-friendly output with an easy-to-follow trace to reproduce a detected error, significantly simplifying further investigation.}, author = {Koval, Nikita and Fedorov, Alexander and Sokolova, Maria and Tsitelov, Dmitry and Alistarh, Dan-Adrian}, publisher = {Zenodo}, title = {{Lincheck: A practical framework for testing concurrent data structures on JVM}}, doi = {10.5281/ZENODO.7877757}, year = {2023}, } @article{12960, abstract = {Isomanifolds are the generalization of isosurfaces to arbitrary dimension and codimension, i.e., submanifolds of Rd defined as the zero set of some multivariate multivalued smooth function f:Rd→Rd−n, where n is the intrinsic dimension of the manifold. A natural way to approximate a smooth isomanifold M=f−1(0) is to consider its piecewise linear (PL) approximation M^ based on a triangulation T of the ambient space Rd. In this paper, we describe a simple algorithm to trace isomanifolds from a given starting point. The algorithm works for arbitrary dimensions n and d, and any precision D. Our main result is that, when f (or M) has bounded complexity, the complexity of the algorithm is polynomial in d and δ=1/D (and unavoidably exponential in n). Since it is known that for δ=Ω(d2.5), M^ is O(D2)-close and isotopic to M , our algorithm produces a faithful PL-approximation of isomanifolds of bounded complexity in time polynomial in d. Combining this algorithm with dimensionality reduction techniques, the dependency on d in the size of M^ can be completely removed with high probability. We also show that the algorithm can handle isomanifolds with boundary and, more generally, isostratifolds. The algorithm for isomanifolds with boundary has been implemented and experimental results are reported, showing that it is practical and can handle cases that are far ahead of the state-of-the-art. }, author = {Boissonnat, Jean Daniel and Kachanovich, Siargey and Wintraecken, Mathijs}, issn = {1095-7111}, journal = {SIAM Journal on Computing}, number = {2}, pages = {452--486}, publisher = {Society for Industrial and Applied Mathematics}, title = {{Tracing isomanifolds in Rd in time polynomial in d using Coxeter–Freudenthal–Kuhn triangulations}}, doi = {10.1137/21M1412918}, volume = {52}, year = {2023}, }