@inproceedings{8272, abstract = {We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. We establish determinacy of such games and present strategy and computational complexity results. For strategy complexity, we show that lexicographically optimal strategies exist that are deterministic and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in NP∩coNP , matching the current known bound for single objectives; and in general the decision problem is PSPACE -hard and can be solved in NEXPTIME∩coNEXPTIME . We present an algorithm that computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. We have implemented our algorithm and report experimental results on various case studies.}, author = {Chatterjee, Krishnendu and Katoen, Joost P and Weininger, Maximilian and Winkler, Tobias}, booktitle = {International Conference on Computer Aided Verification}, isbn = {9783030532901}, issn = {1611-3349}, pages = {398--420}, publisher = {Springer Nature}, title = {{Stochastic games with lexicographic reachability-safety objectives}}, doi = {10.1007/978-3-030-53291-8_21}, volume = {12225}, year = {2020}, } @article{8674, abstract = {Extrasynaptic actions of glutamate are limited by high-affinity transporters expressed by perisynaptic astroglial processes (PAPs): this helps maintain point-to-point transmission in excitatory circuits. Memory formation in the brain is associated with synaptic remodeling, but how this affects PAPs and therefore extrasynaptic glutamate actions is poorly understood. Here, we used advanced imaging methods, in situ and in vivo, to find that a classical synaptic memory mechanism, long-term potentiation (LTP), triggers withdrawal of PAPs from potentiated synapses. Optical glutamate sensors combined with patch-clamp and 3D molecular localization reveal that LTP induction thus prompts spatial retreat of astroglial glutamate transporters, boosting glutamate spillover and NMDA-receptor-mediated inter-synaptic cross-talk. The LTP-triggered PAP withdrawal involves NKCC1 transporters and the actin-controlling protein cofilin but does not depend on major Ca2+-dependent cascades in astrocytes. We have therefore uncovered a mechanism by which a memory trace at one synapse could alter signal handling by multiple neighboring connections.}, author = {Henneberger, Christian and Bard, Lucie and Panatier, Aude and Reynolds, James P. and Kopach, Olga and Medvedev, Nikolay I. and Minge, Daniel and Herde, Michel K. and Anders, Stefanie and Kraev, Igor and Heller, Janosch P. and Rama, Sylvain and Zheng, Kaiyu and Jensen, Thomas P. and Sanchez-Romero, Inmaculada and Jackson, Colin J. and Janovjak, Harald L and Ottersen, Ole Petter and Nagelhus, Erlend Arnulf and Oliet, Stephane H.R. and Stewart, Michael G. and Nägerl, U. VAlentin and Rusakov, Dmitri A. }, issn = {1097-4199}, journal = {Neuron}, number = {5}, pages = {P919--936.E11}, publisher = {Elsevier}, title = {{LTP induction boosts glutamate spillover by driving withdrawal of perisynaptic astroglia}}, doi = {10.1016/j.neuron.2020.08.030}, volume = {108}, year = {2020}, } @inproceedings{8339, abstract = {Discrete Gaussian distributions over lattices are central to lattice-based cryptography, and to the computational and mathematical aspects of lattices more broadly. The literature contains a wealth of useful theorems about the behavior of discrete Gaussians under convolutions and related operations. Yet despite their structural similarities, most of these theorems are formally incomparable, and their proofs tend to be monolithic and written nearly “from scratch,” making them unnecessarily hard to verify, understand, and extend. In this work we present a modular framework for analyzing linear operations on discrete Gaussian distributions. The framework abstracts away the particulars of Gaussians, and usually reduces proofs to the choice of appropriate linear transformations and elementary linear algebra. To showcase the approach, we establish several general properties of discrete Gaussians, and show how to obtain all prior convolution theorems (along with some new ones) as straightforward corollaries. As another application, we describe a self-reduction for Learning With Errors (LWE) that uses a fixed number of samples to generate an unlimited number of additional ones (having somewhat larger error). The distinguishing features of our reduction are its simple analysis in our framework, and its exclusive use of discrete Gaussians without any loss in parameters relative to a prior mixed discrete-and-continuous approach. As a contribution of independent interest, for subgaussian random matrices we prove a singular value concentration bound with explicitly stated constants, and we give tighter heuristics for specific distributions that are commonly used for generating lattice trapdoors. These bounds yield improvements in the concrete bit-security estimates for trapdoor lattice cryptosystems.}, author = {Genise, Nicholas and Micciancio, Daniele and Peikert, Chris and Walter, Michael}, booktitle = {23rd IACR International Conference on the Practice and Theory of Public-Key Cryptography}, isbn = {9783030453732}, issn = {1611-3349}, location = {Edinburgh, United Kingdom}, pages = {623--651}, publisher = {Springer Nature}, title = {{Improved discrete Gaussian and subgaussian analysis for lattice cryptography}}, doi = {10.1007/978-3-030-45374-9_21}, volume = {12110}, year = {2020}, } @inproceedings{8987, abstract = {Currently several projects aim at designing and implementing protocols for privacy preserving automated contact tracing to help fight the current pandemic. Those proposal are quite similar, and in their most basic form basically propose an app for mobile phones which broadcasts frequently changing pseudorandom identifiers via (low energy) Bluetooth, and at the same time, the app stores IDs broadcast by phones in its proximity. Only if a user is tested positive, they upload either the beacons they did broadcast (which is the case in decentralized proposals as DP-3T, east and west coast PACT or Covid watch) or received (as in Popp-PT or ROBERT) during the last two weeks or so. Vaudenay [eprint 2020/399] observes that this basic scheme (he considers the DP-3T proposal) succumbs to relay and even replay attacks, and proposes more complex interactive schemes which prevent those attacks without giving up too many privacy aspects. Unfortunately interaction is problematic for this application for efficiency and security reasons. The countermeasures that have been suggested so far are either not practical or give up on key privacy aspects. We propose a simple non-interactive variant of the basic protocol that (security) Provably prevents replay and (if location data is available) relay attacks. (privacy) The data of all parties (even jointly) reveals no information on the location or time where encounters happened. (efficiency) The broadcasted message can fit into 128 bits and uses only basic crypto (commitments and secret key authentication). Towards this end we introduce the concept of “delayed authentication”, which basically is a message authentication code where verification can be done in two steps, where the first doesn’t require the key, and the second doesn’t require the message.}, author = {Pietrzak, Krzysztof Z}, booktitle = {Progress in Cryptology}, isbn = {9783030652760}, issn = {1611-3349}, location = {Bangalore, India}, pages = {3--15}, publisher = {Springer Nature}, title = {{Delayed authentication: Preventing replay and relay attacks in private contact tracing}}, doi = {10.1007/978-3-030-65277-7_1}, volume = {12578}, year = {2020}, } @inproceedings{8322, abstract = {Reverse firewalls were introduced at Eurocrypt 2015 by Miro-nov and Stephens-Davidowitz, as a method for protecting cryptographic protocols against attacks on the devices of the honest parties. In a nutshell: a reverse firewall is placed outside of a device and its goal is to “sanitize” the messages sent by it, in such a way that a malicious device cannot leak its secrets to the outside world. It is typically assumed that the cryptographic devices are attacked in a “functionality-preserving way” (i.e. informally speaking, the functionality of the protocol remains unchanged under this attacks). In their paper, Mironov and Stephens-Davidowitz construct a protocol for passively-secure two-party computations with firewalls, leaving extension of this result to stronger models as an open question. In this paper, we address this problem by constructing a protocol for secure computation with firewalls that has two main advantages over the original protocol from Eurocrypt 2015. Firstly, it is a multiparty computation protocol (i.e. it works for an arbitrary number n of the parties, and not just for 2). Secondly, it is secure in much stronger corruption settings, namely in the active corruption model. More precisely: we consider an adversary that can fully corrupt up to 𝑛−1 parties, while the remaining parties are corrupt in a functionality-preserving way. Our core techniques are: malleable commitments and malleable non-interactive zero-knowledge, which in particular allow us to create a novel protocol for multiparty augmented coin-tossing into the well with reverse firewalls (that is based on a protocol of Lindell from Crypto 2001).}, author = {Chakraborty, Suvradip and Dziembowski, Stefan and Nielsen, Jesper Buus}, booktitle = {Advances in Cryptology – CRYPTO 2020}, isbn = {9783030568795}, issn = {1611-3349}, location = {Santa Barbara, CA, United States}, pages = {732--762}, publisher = {Springer Nature}, title = {{Reverse firewalls for actively secure MPCs}}, doi = {10.1007/978-3-030-56880-1_26}, volume = {12171}, year = {2020}, } @inproceedings{9103, abstract = {We introduce LRT-NG, a set of techniques and an associated toolset that computes a reachtube (an over-approximation of the set of reachable states over a given time horizon) of a nonlinear dynamical system. LRT-NG significantly advances the state-of-the-art Langrangian Reachability and its associated tool LRT. From a theoretical perspective, LRT-NG is superior to LRT in three ways. First, it uses for the first time an analytically computed metric for the propagated ball which is proven to minimize the ball’s volume. We emphasize that the metric computation is the centerpiece of all bloating-based techniques. Secondly, it computes the next reachset as the intersection of two balls: one based on the Cartesian metric and the other on the new metric. While the two metrics were previously considered opposing approaches, their joint use considerably tightens the reachtubes. Thirdly, it avoids the "wrapping effect" associated with the validated integration of the center of the reachset, by optimally absorbing the interval approximation in the radius of the next ball. From a tool-development perspective, LRT-NG is superior to LRT in two ways. First, it is a standalone tool that no longer relies on CAPD. This required the implementation of the Lohner method and a Runge-Kutta time-propagation method. Secondly, it has an improved interface, allowing the input model and initial conditions to be provided as external input files. Our experiments on a comprehensive set of benchmarks, including two Neural ODEs, demonstrates LRT-NG’s superior performance compared to LRT, CAPD, and Flow*.}, author = {Gruenbacher, Sophie and Cyranka, Jacek and Lechner, Mathias and Islam, Md Ariful and Smolka, Scott A. and Grosu, Radu}, booktitle = {Proceedings of the 59th IEEE Conference on Decision and Control}, isbn = {9781728174471}, issn = {0743-1546}, location = {Jeju Islang, Korea (South)}, pages = {1556--1563}, publisher = {IEEE}, title = {{Lagrangian reachtubes: The next generation}}, doi = {10.1109/CDC42340.2020.9304042}, volume = {2020}, year = {2020}, } @inproceedings{8194, abstract = {Fixed-point arithmetic is a popular alternative to floating-point arithmetic on embedded systems. Existing work on the verification of fixed-point programs relies on custom formalizations of fixed-point arithmetic, which makes it hard to compare the described techniques or reuse the implementations. In this paper, we address this issue by proposing and formalizing an SMT theory of fixed-point arithmetic. We present an intuitive yet comprehensive syntax of the fixed-point theory, and provide formal semantics for it based on rational arithmetic. We also describe two decision procedures for this theory: one based on the theory of bit-vectors and the other on the theory of reals. We implement the two decision procedures, and evaluate our implementations using existing mature SMT solvers on a benchmark suite we created. Finally, we perform a case study of using the theory we propose to verify properties of quantized neural networks.}, author = {Baranowski, Marek and He, Shaobo and Lechner, Mathias and Nguyen, Thanh Son and Rakamarić, Zvonimir}, booktitle = {Automated Reasoning}, isbn = {9783030510732}, issn = {1611-3349}, location = {Paris, France}, pages = {13--31}, publisher = {Springer Nature}, title = {{An SMT theory of fixed-point arithmetic}}, doi = {10.1007/978-3-030-51074-9_2}, volume = {12166}, year = {2020}, } @article{7684, author = {Gridchyn, Igor and Schönenberger, Philipp and O'Neill, Joseph and Csicsvari, Jozsef L}, issn = {1097-4199}, journal = {Neuron}, number = {2}, pages = {291--300.e6}, publisher = {Elsevier}, title = {{Assembly-specific disruption of hippocampal replay leads to selective memory deficit}}, doi = {10.1016/j.neuron.2020.01.021}, volume = {106}, year = {2020}, } @inproceedings{7808, abstract = {Quantization converts neural networks into low-bit fixed-point computations which can be carried out by efficient integer-only hardware, and is standard practice for the deployment of neural networks on real-time embedded devices. However, like their real-numbered counterpart, quantized networks are not immune to malicious misclassification caused by adversarial attacks. We investigate how quantization affects a network’s robustness to adversarial attacks, which is a formal verification question. We show that neither robustness nor non-robustness are monotonic with changing the number of bits for the representation and, also, neither are preserved by quantization from a real-numbered network. For this reason, we introduce a verification method for quantized neural networks which, using SMT solving over bit-vectors, accounts for their exact, bit-precise semantics. We built a tool and analyzed the effect of quantization on a classifier for the MNIST dataset. We demonstrate that, compared to our method, existing methods for the analysis of real-numbered networks often derive false conclusions about their quantizations, both when determining robustness and when detecting attacks, and that existing methods for quantized networks often miss attacks. Furthermore, we applied our method beyond robustness, showing how the number of bits in quantization enlarges the gender bias of a predictor for students’ grades.}, author = {Giacobbe, Mirco and Henzinger, Thomas A and Lechner, Mathias}, booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783030452360}, issn = {1611-3349}, location = {Dublin, Ireland}, pages = {79--97}, publisher = {Springer Nature}, title = {{How many bits does it take to quantize your neural network?}}, doi = {10.1007/978-3-030-45237-7_5}, volume = {12079}, year = {2020}, } @article{7586, abstract = {CLC chloride/proton exchangers may support acidification of endolysosomes and raise their luminal Cl− concentration. Disruption of endosomal ClC‐3 causes severe neurodegeneration. To assess the importance of ClC‐3 Cl−/H+ exchange, we now generate Clcn3unc/unc mice in which ClC‐3 is converted into a Cl− channel. Unlike Clcn3−/− mice, Clcn3unc/unc mice appear normal owing to compensation by ClC‐4 with which ClC‐3 forms heteromers. ClC‐4 protein levels are strongly reduced in Clcn3−/−, but not in Clcn3unc/unc mice because ClC‐3unc binds and stabilizes ClC‐4 like wild‐type ClC‐3. Although mice lacking ClC‐4 appear healthy, its absence in Clcn3unc/unc/Clcn4−/− mice entails even stronger neurodegeneration than observed in Clcn3−/− mice. A fraction of ClC‐3 is found on synaptic vesicles, but miniature postsynaptic currents and synaptic vesicle acidification are not affected in Clcn3unc/unc or Clcn3−/− mice before neurodegeneration sets in. Both, Cl−/H+‐exchange activity and the stabilizing effect on ClC‐4, are central to the biological function of ClC‐3.}, author = {Weinert, Stefanie and Gimber, Niclas and Deuschel, Dorothea and Stuhlmann, Till and Puchkov, Dmytro and Farsi, Zohreh and Ludwig, Carmen F. and Novarino, Gaia and López-Cayuqueo, Karen I. and Planells-Cases, Rosa and Jentsch, Thomas J.}, issn = {1460-2075}, journal = {EMBO Journal}, publisher = {EMBO Press}, title = {{Uncoupling endosomal CLC chloride/proton exchange causes severe neurodegeneration}}, doi = {10.15252/embj.2019103358}, volume = {39}, year = {2020}, } @article{6761, abstract = {In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability.}, author = {Avni, Guy and Henzinger, Thomas A and Kupferman, Orna}, issn = {0304-3975}, journal = {Theoretical Computer Science}, pages = {42--55}, publisher = {Elsevier}, title = {{Dynamic resource allocation games}}, doi = {10.1016/j.tcs.2019.06.031}, volume = {807}, year = {2020}, } @article{7623, abstract = {A two-dimensional mathematical model for cells migrating without adhesion capabilities is presented and analyzed. Cells are represented by their cortex, which is modeled as an elastic curve, subject to an internal pressure force. Net polymerization or depolymerization in the cortex is modeled via local addition or removal of material, driving a cortical flow. The model takes the form of a fully nonlinear degenerate parabolic system. An existence analysis is carried out by adapting ideas from the theory of gradient flows. Numerical simulations show that these simple rules can account for the behavior observed in experiments, suggesting a possible mechanical mechanism for adhesion-independent motility.}, author = {Jankowiak, Gaspard and Peurichard, Diane and Reversat, Anne and Schmeiser, Christian and Sixt, Michael K}, issn = {0218-2025}, journal = {Mathematical Models and Methods in Applied Sciences}, number = {3}, pages = {513--537}, publisher = {World Scientific Publishing}, title = {{Modeling adhesion-independent cell migration}}, doi = {10.1142/S021820252050013X}, volume = {30}, year = {2020}, } @phdthesis{8386, abstract = {Form versus function is a long-standing debate in various design-related fields, such as architecture as well as graphic and industrial design. A good design that balances form and function often requires considerable human effort and collaboration among experts from different professional fields. Computational design tools provide a new paradigm for designing functional objects. In computational design, form and function are represented as mathematical quantities, with the help of numerical and combinatorial algorithms, they can assist even novice users in designing versatile models that exhibit their desired functionality. This thesis presents three disparate research studies on the computational design of functional objects: The appearance of 3d print—we optimize the volumetric material distribution for faithfully replicating colored surface texture in 3d printing; the dynamic motion of mechanical structures— our design system helps the novice user to retarget various mechanical templates with different functionality to complex 3d shapes; and a more abstract functionality, multistability—our algorithm automatically generates models that exhibit multiple stable target poses. For each of these cases, our computational design tools not only ensure the functionality of the results but also permit the user aesthetic freedom over the form. Moreover, fabrication constraints were taken into account, which allow for the immediate creation of physical realization via 3D printing or laser cutting.}, author = {Zhang, Ran}, issn = {2663-337X}, pages = {148}, publisher = {Institute of Science and Technology Austria}, title = {{Structure-aware computational design and its application to 3D printable volume scattering, mechanism, and multistability}}, doi = {10.15479/AT:ISTA:8386}, year = {2020}, } @inproceedings{7966, abstract = {For 1≤m≤n, we consider a natural m-out-of-n multi-instance scenario for a public-key encryption (PKE) scheme. An adversary, given n independent instances of PKE, wins if he breaks at least m out of the n instances. In this work, we are interested in the scaling factor of PKE schemes, SF, which measures how well the difficulty of breaking m out of the n instances scales in m. That is, a scaling factor SF=ℓ indicates that breaking m out of n instances is at least ℓ times more difficult than breaking one single instance. A PKE scheme with small scaling factor hence provides an ideal target for mass surveillance. In fact, the Logjam attack (CCS 2015) implicitly exploited, among other things, an almost constant scaling factor of ElGamal over finite fields (with shared group parameters). For Hashed ElGamal over elliptic curves, we use the generic group model to argue that the scaling factor depends on the scheme's granularity. In low granularity, meaning each public key contains its independent group parameter, the scheme has optimal scaling factor SF=m; In medium and high granularity, meaning all public keys share the same group parameter, the scheme still has a reasonable scaling factor SF=√m. Our findings underline that instantiating ElGamal over elliptic curves should be preferred to finite fields in a multi-instance scenario. As our main technical contribution, we derive new generic-group lower bounds of Ω(√(mp)) on the difficulty of solving both the m-out-of-n Gap Discrete Logarithm and the m-out-of-n Gap Computational Diffie-Hellman problem over groups of prime order p, extending a recent result by Yun (EUROCRYPT 2015). We establish the lower bound by studying the hardness of a related computational problem which we call the search-by-hypersurface problem.}, author = {Auerbach, Benedikt and Giacon, Federico and Kiltz, Eike}, booktitle = {Advances in Cryptology – EUROCRYPT 2020}, isbn = {9783030457266}, issn = {1611-3349}, pages = {475--506}, publisher = {Springer Nature}, title = {{Everybody’s a target: Scalability in public-key encryption}}, doi = {10.1007/978-3-030-45727-3_16}, volume = {12107}, year = {2020}, } @inproceedings{8623, abstract = {We introduce the monitoring of trace properties under assumptions. An assumption limits the space of possible traces that the monitor may encounter. An assumption may result from knowledge about the system that is being monitored, about the environment, or about another, connected monitor. We define monitorability under assumptions and study its theoretical properties. In particular, we show that for every assumption A, the boolean combinations of properties that are safe or co-safe relative to A are monitorable under A. We give several examples and constructions on how an assumption can make a non-monitorable property monitorable, and how an assumption can make a monitorable property monitorable with fewer resources, such as integer registers.}, author = {Henzinger, Thomas A and Sarac, Naci E}, booktitle = {Runtime Verification}, isbn = {9783030605070}, issn = {1611-3349}, location = {Los Angeles, CA, United States}, pages = {3--18}, publisher = {Springer Nature}, title = {{Monitorability under assumptions}}, doi = {10.1007/978-3-030-60508-7_1}, volume = {12399}, year = {2020}, } @inbook{10865, abstract = {We introduce the notion of Witness Maps as a cryptographic notion of a proof system. A Unique Witness Map (UWM) deterministically maps all witnesses for an NP statement to a single representative witness, resulting in a computationally sound, deterministic-prover, non-interactive witness independent proof system. A relaxation of UWM, called Compact Witness Map (CWM), maps all the witnesses to a small number of witnesses, resulting in a “lossy” deterministic-prover, non-interactive proof-system. We also define a Dual Mode Witness Map (DMWM) which adds an “extractable” mode to a CWM. Our main construction is a DMWM for all NP relations, assuming sub-exponentially secure indistinguishability obfuscation ( iO ), along with standard cryptographic assumptions. The DMWM construction relies on a CWM and a new primitive called Cumulative All-Lossy-But-One Trapdoor Functions (C-ALBO-TDF), both of which are in turn instantiated based on iO and other primitives. Our instantiation of a CWM is in fact a UWM; in turn, we show that a UWM implies Witness Encryption. Along the way to constructing UWM and C-ALBO-TDF, we also construct, from standard assumptions, Puncturable Digital Signatures and a new primitive called Cumulative Lossy Trapdoor Functions (C-LTDF). The former improves up on a construction of Bellare et al. (Eurocrypt 2016), who relied on sub-exponentially secure iO and sub-exponentially secure OWF. As an application of our constructions, we show how to use a DMWM to construct the first leakage and tamper-resilient signatures with a deterministic signer, thereby solving a decade old open problem posed by Katz and Vaikunthanathan (Asiacrypt 2009), by Boyle, Segev and Wichs (Eurocrypt 2011), as well as by Faonio and Venturi (Asiacrypt 2016). Our construction achieves the optimal leakage rate of 1−o(1) .}, author = {Chakraborty, Suvradip and Prabhakaran, Manoj and Wichs, Daniel}, booktitle = {Public-Key Cryptography}, editor = {Kiayias, A}, isbn = {9783030453732}, issn = {1611-3349}, pages = {220--246}, publisher = {Springer Nature}, title = {{Witness maps and applications}}, doi = {10.1007/978-3-030-45374-9_8}, volume = {12110}, year = {2020}, } @article{6649, abstract = {While Hartree–Fock theory is well established as a fundamental approximation for interacting fermions, it has been unclear how to describe corrections to it due to many-body correlations. In this paper we start from the Hartree–Fock state given by plane waves and introduce collective particle–hole pair excitations. These pairs can be approximately described by a bosonic quadratic Hamiltonian. We use Bogoliubov theory to construct a trial state yielding a rigorous Gell-Mann–Brueckner–type upper bound to the ground state energy. Our result justifies the random-phase approximation in the mean-field scaling regime, for repulsive, regular interaction potentials. }, author = {Benedikter, Niels P and Nam, Phan Thành and Porta, Marcello and Schlein, Benjamin and Seiringer, Robert}, issn = {1432-0916}, journal = {Communications in Mathematical Physics}, pages = {2097–2150}, publisher = {Springer Nature}, title = {{Optimal upper bound for the correlation energy of a Fermi gas in the mean-field regime}}, doi = {10.1007/s00220-019-03505-5}, volume = {374}, year = {2020}, } @article{7866, abstract = {In this paper, we establish convergence to equilibrium for a drift–diffusion–recombination system modelling the charge transport within certain semiconductor devices. More precisely, we consider a two-level system for electrons and holes which is augmented by an intermediate energy level for electrons in so-called trapped states. The recombination dynamics use the mass action principle by taking into account this additional trap level. The main part of the paper is concerned with the derivation of an entropy–entropy production inequality, which entails exponential convergence to the equilibrium via the so-called entropy method. The novelty of our approach lies in the fact that the entropy method is applied uniformly in a fast-reaction parameter which governs the lifetime of electrons on the trap level. Thus, the resulting decay estimate for the densities of electrons and holes extends to the corresponding quasi-steady-state approximation.}, author = {Fellner, Klemens and Kniely, Michael}, issn = {2296-9039}, journal = {Journal of Elliptic and Parabolic Equations}, pages = {529--598}, publisher = {Springer Nature}, title = {{Uniform convergence to equilibrium for a family of drift–diffusion models with trap-assisted recombination and the limiting Shockley–Read–Hall model}}, doi = {10.1007/s41808-020-00068-8}, volume = {6}, year = {2020}, } @article{21640, abstract = {Conventional computing architectures have no known efficient algorithms for combinatorial optimization tasks such as the Ising problem, which requires finding the ground state spin configuration of an arbitrary Ising graph. Physical Ising machines have recently been developed as an alternative to conventional exact and heuristic solvers; however, these machines typically suffer from decreased ground state convergence probability or universality for high edge- density graphs or arbitrary graph weights, respectively. We experimentally demonstrate a proof-of-principle integrated nanophotonic recurrent Ising sampler (INPRIS), using a hybrid scheme combining electronics and silicon-on-insulator photonics, that is capable of converging to the ground state of various four-spin graphs with high probability. The INPRIS results indicate that noise may be used as a resource to speed up the ground state search and to explore larger regions of the phase space, thus allowing one to probe noise-dependent physical observables. Since the recurrent pho- tonic transformation that our machine imparts is a fixed function of the graph problem and therefore compatible with optoelectronic architectures that support GHz clock rates (such as passive or non-volatile photonic circuits that do not require reprogramming at each iteration), this work suggests the potential for future systems that could achieve orders- of-magnitude speedups in exploring the solution space of combinatorially hard problems. }, author = {Prabhu, Mihika and Roques-Carmes, Charles and Shen, Yichen and Harris, Nicholas and Jing, Li and Carolan, Jacques and Hamerly, Ryan and Baehr-Jones, Tom and Hochberg, Michael and Čeperić, Vladimir and Joannopoulos, John D. and Englund, Dirk R. and Soljačić, Marin}, issn = {2334-2536}, journal = {Optica}, number = {5}, pages = {551--558}, publisher = {Optica Publishing Group}, title = {{Accelerating recurrent Ising machines in photonic integrated circuits}}, doi = {10.1364/optica.386613}, volume = {7}, year = {2020}, } @article{21637, abstract = {We demonstrate new axisymmetric inverse-design techniques that can solve problems radically different from traditional lenses, including reconfigurable lenses (that shift a multi-frequency focal spot in response to refractive-index changes) and widely separated multi-wavelength lenses (λ = 1 µm and 10 µm). We also present experimental validation for an axisymmetric inverse-designed monochrome lens in the near-infrared fabricated via two-photon polymerization. Axisymmetry allows fullwave Maxwell solvers to be scaled up to structures hundreds or even thousands of wavelengths in diameter before requiring domain-decomposition approximations, while multilayer topology optimization with ∼105 degrees of freedom can tackle challenging design problems even when restricted to axisymmetric structures.}, author = {Christiansen, Rasmus E. and Lin, Zin and Roques-Carmes, Charles and Salamin, Yannick and Kooi, Steven E. and Joannopoulos, John D. and Soljačić, Marin and Johnson, Steven G.}, issn = {1094-4087}, journal = {Optics Express}, number = {23}, pages = {33854--33868}, publisher = {Optica Publishing Group}, title = {{Fullwave Maxwell inverse design of axisymmetric, tunable, and multi-scale multi-wavelength metalenses}}, doi = {10.1364/oe.403192}, volume = {28}, year = {2020}, }