@inproceedings{21280,
  abstract     = {We give an algorithm that, with high probability, maintains a (1-ε)-approximate s-t maximum flow in undirected, uncapacitated n-vertex graphs undergoing m edge insertions in Õ(m+ n F^*/ε) total update time, where F^{*} is the maximum flow on the final graph. This is the first algorithm to achieve polylogarithmic amortized update time for dense graphs (m = Ω(n²)), and more generally, for graphs where F^* = Õ(m/n). At the heart of our incremental algorithm is the residual graph sparsification technique of Karger and Levine [SICOMP '15], originally designed for computing exact maximum flows in the static setting. Our main contributions are (i) showing how to maintain such sparsifiers for approximate maximum flows in the incremental setting and (ii) generalizing the cut sparsification framework of Fung et al. [SICOMP '19] from undirected graphs to balanced directed graphs.},
  author       = {Goranci, Gramoz and Henzinger, Monika H and Räcke, Harald and Sricharan, A.},
  booktitle    = {52nd International Colloquium on Automata, Languages, and Programming},
  isbn         = {9783959773720},
  location     = {Aarhus, Denmark},
  pages        = {91:1--91:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Incremental approximate maximum flow via residual graph sparsification}},
  doi          = {10.4230/lipics.icalp.2025.91},
  volume       = {334},
  year         = {2025},
}

@inproceedings{21262,
  abstract     = {Continuous Group Key Agreement (CGKA) is the primitive underlying secure group messaging. It allows a large group of N users to maintain a shared secret key that is frequently rotated by the
group members in order to achieve forward secrecy and post compromise security. The group messaging scheme Messaging Layer Security (MLS) standardized by the IETF makes use of a CGKA called TreeKEM which arranges the N group members in a binary tree. Here, each node is associated with a public-key, each user is assigned one of the leaves, and a user knows the corresponding secret keys from their leaf to the root. To update the key material known to them, a user must just replace keys at log(N) nodes, which requires them to create and upload log(N) ciphertexts. Such updates must be processed sequentially by all users, which for large groups is impractical. To allow for concurrent updates, TreeKEM uses the “propose and commit” paradigm, where multiple users can concurrently propose to update (by just sampling a fresh leaf key), and a single user can then commit to all proposals at once. Unfortunately, this process destroys the binary tree structure as the tree gets pruned and some nodes must be “blanked” at the cost of increasing the in-degree of others, which makes the commit operation, as well as, future commits more costly. In the worst case, the update cost (in terms of uploaded ciphertexts) per user can grow from log(N) to Ω(N). In this work we provide two main contributions. First, we show that MLS’ communication complexity is bad not only in the worst case but also if the proposers and committers are chosen at random: even if there’s just one update proposal for every commit the expected cost is already over √N, and it approaches N as this ratio changes towards more proposals. Our second contribution is a new variant of propose and commit for
TreeKEM which for moderate amounts of update proposals per commit provably achieves an update cost of Θ(log(N)) assuming the proposers and committers are chosen at random.},
  author       = {Auerbach, Benedikt and Cueto Noval, Miguel and Erol, Boran and Pietrzak, Krzysztof Z},
  booktitle    = {45th Annual International Cryptology Conference},
  isbn         = {9783032019127},
  issn         = {1611-3349},
  location     = {Santa Barbara, CA, United States},
  pages        = {141--172},
  publisher    = {Springer Nature},
  title        = {{Continuous group-key agreement: Concurrent updates without pruning}},
  doi          = {10.1007/978-3-032-01913-4_5},
  volume       = {16007},
  year         = {2025},
}

@article{19278,
  abstract     = {When two insulating, neutral materials are contacted and separated, they exchange electrical charge1. Experiments have long suggested that this ‘contact electrification’ is transitive, with different materials ordering into ‘triboelectric series’ based on the sign of charge acquired2. At the same time, the effect is plagued by unpredictability, preventing consensus on the mechanism and casting doubt on the rhyme and reason that series imply3. Here we expose an unanticipated connection between the unpredictability and order in contact electrification: nominally identical materials initially exchange charge randomly and intransitively, but—over repeated experiments—order into triboelectric series. We find that this evolution is driven by the act of contact itself—samples with more contacts in their history charge negatively to ones with fewer contacts. Capturing this ‘contact bias’ in a minimal model, we recreate both the initial randomness and ultimate order in numerical simulations and use it experimentally to force the appearance of a triboelectric series of our choosing. With a set of surface-sensitive techniques to search for the underlying alterations contact creates, we only find evidence of nanoscale morphological changes, pointing to a mechanism strongly coupled with mechanics. Our results highlight the centrality of contact history in contact electrification and suggest that focusing on the unpredictability that has long plagued the effect may hold the key to understanding it.},
  author       = {Sobarzo Ponce, Juan Carlos A and Pertl, Felix and Balazs, Daniel and Costanzo, Tommaso and Sauer, Markus and Foelske, Annette and Ostermann, Markus and Pichler, Christian M. and Wang, Yongkang and Nagata, Yuki and Bonn, Mischa and Waitukaitis, Scott R},
  issn         = {1476-4687},
  journal      = {Nature},
  number       = {8051},
  publisher    = {Springer Nature},
  title        = {{Spontaneous ordering of identical materials into a triboelectric series}},
  doi          = {10.1038/s41586-024-08530-6},
  volume       = {638},
  year         = {2025},
}

@article{20481,
  abstract     = {Kelvin probe force microscopy (KPFM) is widely used in stationary and dynamic studies of contact electrification. An obvious question that connects these two has been overlooked: when are charge dynamics too fast for stationary studies to be meaningful? Using a rapid transfer system to quickly perform KPFM after contact, we find the dynamics are too fast in all but the best insulators. Our data further suggest that dynamics are caused by bulk as opposed to surface conductivity, and that charge-transfer heterogeneity is less prevalent than previously suggested.},
  author       = {Pertl, Felix and Lenton, Isaac C and Cramer, Tobias and Waitukaitis, Scott R},
  issn         = {1079-7114},
  journal      = {Physical Review Letters},
  number       = {14},
  publisher    = {American Physical Society},
  title        = {{No time for surface charge: How bulk conductivity hides charge patterns from Kelvin probe force microscopy in contact-electrified surfaces}},
  doi          = {10.1103/lcsm-xxty},
  volume       = {135},
  year         = {2025},
}

@article{20452,
  abstract     = {Accurate modeling of long-range forces is critical in atomistic simulations, as they play a central role in determining the properties of material and chemical systems. However, standard machine learning interatomic potentials (MLIPs) often rely on short-range approximations, limiting their applicability to systems with significant electrostatics and dispersion forces. We recently introduced the Latent Ewald Summation (LES) method, which captures long-range electrostatics without explicitly learning atomic charges or charge equilibration. We benchmark LES on diverse and challenging systems, including charged molecules, ionic liquids, electrolyte solutions, polar dipeptides, surface adsorption, electrolyte/solid interfaces, and solid-solid interfaces. Here we show that LES can reproduce the exact atomic charges for classical systems with fixed charges and can infer dipole and quadrupole moments, as well as the dipole derivative with respect to atomic positions, for quantum mechanical systems. Moreover, LES can achieve better accuracy in energy and force predictions compared to methods that explicitly learn from charges.},
  author       = {King, Daniel S. and Kim, Dongjin and Zhong, Peichen and Cheng, Bingqing},
  issn         = {2041-1723},
  journal      = {Nature Communications},
  publisher    = {Springer Nature},
  title        = {{Machine learning of charges and long-range interactions from energies and forces}},
  doi          = {10.1038/s41467-025-63852-x},
  volume       = {16},
  year         = {2025},
}

@misc{22770,
  author       = {Cheng, Bingqing and King, Daniel and Kim, Dongjin and Zhong, Peichen},
  publisher    = {Repository},
  title        = {{BingqingCheng/cace-lr-fit: V0}},
  doi          = {10.5281/zenodo.16415060},
  year         = {2025},
}

@phdthesis{19684,
  abstract     = {The overarching goal of this thesis is to break down the complexity of turbulent flows in terms of enumerable, coherent structures and patterns. In a five-paper series, we adopt a variety of perspectives and techniques to relate the properties of systems of increasing complexity to their underlying coherent structures. 

Initially, we take a dynamical systems point of view, seeing turbulent flow as a chaotic trajectory bouncing between exact unstable solutions of the underlying equations of motion. Using persistent homology, the main tool of topological data analysis capturing the persistence across scales of topological features in a point cloud, we introduce a method that quantifies visits of turbulent trajectories to unstable time-periodic solutions, also called periodic orbits. We demonstrate this method first in the Rössler and Kuramoto–Sivashinsky systems. Using this method in 3D Kolmogorov flow, we extract a Markov chain from turbulent data, where each node corresponds to the neighbourhood of a periodic orbit. The invariant distribution of this Markov chain reproduces expectation values on turbulent data when it is used to weight averages on the respective periodic orbits.

In more realistic, wall-bounded settings, such as plane-Couette flow (pcf) driven by the relative motion of the walls, or plane-Poiseuille flow (ppf) driven by a pressure gradient, finding exact solutions is difficult. We use dynamic mode decomposition (DMD), a dimensionality reduction method for sequential data, to identify and approximate low-dimensional dynamics without knowing any exact solutions. Most spatially-extended systems are equivariant under translations, and in such cases spatial drifts dominate DMD, hindering its use in the search for and modelling of low-dimensional dynamics. We augment DMD with a symmetry reduction method trained on turbulent data to stop it from seeing translations as a feature, improving its ability to extract dynamical information in translation-equivariant systems. We find segments of turbulent trajectories that linearize well with their symmetry-reduced DMD spectra, akin to dynamics near exact solutions. Searching for harmonics in the spectra gives leads for periodic orbits with spatial drifts, one of which converges to a new solution.

In larger domains, turbulence can localize and coexist with surrounding laminar flow. Our preceding approaches are global, taking all of a domain into account at once, and cannot readily treat each localized patch individually. Working first in a minimal oblique domain that can host a single 1D-localized turbulent patch, we find that turbulence in ppf is connected to a stable periodic orbit at a flow velocity much lower than when turbulence is first onset. We show that, well in advance of sustained turbulence, chaos sets in explosively, and for long time horizons, time series are consistent with that of a random process.

Finally, in much larger domains, we study and compare 2D-localized turbulence that appears as large-scale inclined structures, called stripes, in ppf and pcf. While appearing similar, we find that stripes in these two settings differ significantly in terms of how they sustain themselves, and in higher velocities, how they proliferate.},
  author       = {Yalniz, Gökhan},
  issn         = {2663-337X},
  pages        = {155},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Transition to turbulence: Data-, solution-, and pattern-driven approaches}},
  doi          = {10.15479/AT-ISTA-19684},
  year         = {2025},
}

@article{19795,
  abstract     = {Super-resolution microscopy often entails long acquisition times of minutes to hours. Since drifts during the acquisition adversely affect data quality, active sample stabilization is commonly used for some of these techniques to reach their full potential. Although drifts in the lateral plane can often be corrected after acquisition, this is not always possible or may come with drawbacks. Therefore, it is appealing to stabilize sample position in three dimensions (3D) during acquisition. Various schemes for active sample stabilization have been demonstrated previously, with some reaching sub-nanometer stability in 3D. Here, we present a scheme for active drift correction that delivers the nanometer-scale 3D stability demanded by state-of-the-art super-resolution techniques and is straightforward to implement compared to previous schemes capable of reaching this level of stabilization precision. Using a refined algorithm that can handle various types of reference structure, without sparse signal peaks being mandatory, we stabilized sample position to ∼1 nm in 3D using objective lenses both with high and low numerical aperture. Our implementation requires only the addition of a simple widefield imaging path and we provide an open-source control software with graphical user interface to facilitate easy adoption of the module. Finally, we demonstrate how this has the potential to enhance data collection for diffraction-limited and super-resolution imaging techniques using single-molecule localization microscopy and cryo-confocal imaging as showcases.},
  author       = {Vorlaufer, Jakob and Semenov, Nikolai and Kreuzinger, Caroline and Javoor, Manjunath and Zens, Bettina and Agudelo Duenas, Nathalie and Tavakoli, Mojtaba and Suplata, Marek and Jahr, Wiebke and Lyudchik, Julia and Wartak, Andreas and Schur, Florian Km and Danzl, Johann G},
  issn         = {2667-0747},
  journal      = {Biophysical Reports},
  number       = {2},
  publisher    = {Elsevier},
  title        = {{Image-based 3D active sample stabilization on the nanometer scale for optical microscopy}},
  doi          = {10.1016/j.bpr.2025.100211},
  volume       = {5},
  year         = {2025},
}

@inproceedings{20668,
  abstract     = {The Message Layer Security (MLS) protocol has recently been standardized by the IETF. MLS is a scalable secure group messaging protocol expected to run more efficiently compared to the Signal protocol at scale, while offering a similar level of strong security. Even though MLS has undergone extensive examination by researchers, the majority of the works have focused on confidentiality.

In this work, we focus on the authenticity of the application messages exchanged in MLS. Currently, MLS authenticates every application message with an EdDSA signature and while manageable, the overhead is greatly amplified in the post-quantum setting as the NIST-recommended Dilithium signature results in a 40x increase in size. We view this as an invitation to explore new authentication modes that can be used instead. We start by taking a systematic view on how application messages are authenticated in MLS and categorize authenticity into four different security notions. We then propose several authentication modes, offering a range of different efficiency and security profiles. For instance, in one of our modes, COSMOS++, we replace signatures with one-time tokens and a MAC tag, offering roughly a 75x savings in the post-quantum communication overhead. While this comes at the cost of weakening security compared to the authentication mode used by MLS, the lower communication overhead seems to make it a worthwhile trade-off with security.},
  author       = {Hashimoto, Keitaro and Katsumata, Shuichi and Pascual Perez, Guillermo},
  booktitle    = {34th Usenix Security Symposium},
  isbn         = {9781939133526},
  location     = {Seattle, WA, USA},
  pages        = {6699--6716},
  publisher    = {Usenix Association},
  title        = {{Exploring how to authenticate application messages in MLS: More efficient, post-quantum, and anonymous blocklistable}},
  year         = {2025},
}

@article{22774,
  abstract     = {We consider the problem of certifying the feasibility of a (possibly degenerate) semidefinite programming problem represented by rational input data together with a numerical solution that is guaranteed to be sufficiently close to an exact solution of maximal rank. Our method constructs a polynomial system whose set of real solutions has an isolated point that satisfies the input program. An experimental comparison between the corresponding symbolic-numerical algorithm and the purely symbolic algorithm from [3, 5] shows that the hybrid algorithm is able to certify instances where the exact method fails.},
  author       = {Kolmogorov, Vladimir and Naldi, Simone and Zapata, Jeferson},
  issn         = {1932-2240},
  journal      = {ACM Communications in Computer Algebra},
  number       = {4},
  pages        = {147--152},
  publisher    = {ACM},
  title        = {{Certifying solutions of degenerate semidefinite programs}},
  doi          = {10.1145/3832046.3832063},
  volume       = {59},
  year         = {2025},
}

@article{18710,
  abstract     = {We present an ab initio theoretical method to calculate the resonant Auger spectrum in the presence of ultrafast dissociation. The method is demonstrated by deriving the L-VV resonant Auger spectrum mediated by the 2p3/2−1σ* resonance in HCl, where the electronic Auger decay and nuclear dissociation occur on the same time scale. The Auger decay rates are calculated within the one-center approximation and are shown to vary significantly with the inter-nuclear distance. A quantum-mechanical description of dissociation is effectuated by propagating the corresponding Franck–Condon factors. The calculated profiles of Auger spectral lines resemble those of atomic Auger decay but here the characteristic tails extend towards lower electron kinetic energies, which reflect specific features of the potential energy curves. The presented method can describe the resonant Auger spectrum for an arbitrary speed of dissociation and simplifies to known approximations in the limiting cases.},
  author       = {Hrast, Mateja and Ljubotina, Marko and Zitnik, Matjaz},
  issn         = {1463-9076},
  journal      = {Physical Chemistry Chemical Physics},
  number       = {3},
  pages        = {1473--1482},
  publisher    = {Royal Society of Chemistry},
  title        = {{Ab initio Auger spectrum of the ultrafast dissociating 2p3/2−1σ* resonance in HCl}},
  doi          = {10.1039/d4cp03727h},
  volume       = {27},
  year         = {2025},
}

@inproceedings{22826,
  abstract     = {Large Language Models (LLMs) have demonstrated the ability to tackle increasingly complex tasks through advanced reasoning, long-form content generation,
and tool use. Solving these tasks often involves long inference-time computations.
In human problem solving, a common strategy to expedite work is collaboration: by
dividing the problem into sub-tasks, exploring different strategies concurrently, etc.
Recent research has shown that LLMs can also operate in parallel by implementing
explicit cooperation frameworks, such as voting mechanisms or the explicit creation of independent sub-tasks that can be executed in parallel. However, each of
these frameworks may not be suitable for all types of tasks, which can hinder their
applicability. In this work, we propose a different design approach: we run LLM
“workers” in parallel , allowing them to synchronize via a concurrently-updated
attention cache and prompt these workers to decide how best to collaborate. Our
approach allows the LLM instances to come up with their own collaboration strategy for the problem at hand, all the while “seeing” each other’s memory in the
concurrent KV cache. We implement this approach via Hogwild! Inference: a
parallel LLM inference engine where multiple instances of the same LLM run in
parallel with the same attention cache, with “instant” access to each other’s memory.1 Hogwild! Inference takes advantage of Rotary Position Embeddings (RoPE)
to avoid recomputation while improving parallel hardware utilization. We find that
modern reasoning-capable LLMs can perform inference with shared Key-Value
cache out of the box, without additional fine-tuning.},
  author       = {Rodionov, Gleb and Garipov, Roman and Shutova, Alina and Yakushev, George and Schultheis, Erik and Egiazarian, Vage and Sinitsin, Anton and Kuznedelev, Denis and Alistarh, Dan-Adrian},
  booktitle    = {39th Conference on Neural Information Processing Systems},
  isbn         = {9798331338275},
  issn         = {1049-5258},
  location     = {San Diego, CA, United States},
  pages        = {52014--52055},
  publisher    = {Neural Information Processing Systems Foundation},
  title        = {{Hogwild! Inference: Parallel LLM generation via concurrent attention}},
  doi          = {10.52202/085713-1551},
  volume       = {38},
  year         = {2025},
}

@inproceedings{22825,
  abstract     = {The empirical emergence of neural collapse—a surprising symmetry in the feature representations of the training data in the penultimate layer of deep neural
networks—has spurred a line of theoretical research aimed at its understanding.
However, existing work focuses on data-agnostic models or, when data structure is
taken into account, it remains limited to multi-layer perceptrons. Our paper fills
both these gaps by analyzing modern architectures in a data-aware regime: we
prove that global optima of deep regularized transformers and residual networks
(ResNets) with LayerNorm trained with cross entropy or mean squared error loss
are approximately collapsed, and the approximation gets tighter as the depth grows.
More generally, we formally reduce any end-to-end large-depth ResNet or transformer training into an equivalent unconstrained features model, thus justifying its
wide use in the literature even beyond data-agnostic settings. Our theoretical results
are supported by experiments on computer vision and language datasets showing
that, as the depth grows, neural collapse indeed becomes more prominent.},
  author       = {Súkeník, Peter and Lampert, Christoph and Mondelli, Marco},
  booktitle    = {39th Conference on Neural Information Processing Systems},
  isbn         = {9798331338275},
  issn         = {1049-5258},
  location     = {San Diego, CA, United States},
  pages        = {48646--48677},
  publisher    = {Neural Information Processing Systems Foundation},
  title        = {{Neural collapse is globally optimal in deep regularized ResNets and transformers}},
  doi          = {10.52202/085713-1450},
  volume       = {38},
  year         = {2025},
}

@inproceedings{22824,
  abstract     = {We present new fast-rate PAC-Bayesian generalization bounds for multi-task and
meta-learning in the unbalanced setting, i.e. when the tasks have training sets of
different sizes, as is typically the case in real-world scenarios. Previously, only
standard-rate bounds were known for this situation, while fast-rate bounds were
limited to the setting where all training sets are of equal size. Our new bounds
are numerically computable as well as interpretable, and we demonstrate their
flexibility in handling a number of cases where they give stronger guarantees
than previous bounds. Besides the bounds themselves, we also make conceptual
contributions: we demonstrate that the unbalanced multi-task setting has different
statistical properties than the balanced situation, specifically that proofs from
the balanced situation do not carry over to the unbalanced setting. Additionally,
we shed light on the fact that the unbalanced situation allows two meaningful
definitions of multi-task risk, depending on whether all tasks should be considered
equally important or if sample-rich tasks should receive more weight than samplepoor ones.},
  author       = {Zakerinia, Hossein and Lampert, Christoph},
  booktitle    = {39th Conference on Neural Information Processing Systems},
  isbn         = {9798331338275},
  issn         = {1049-5258},
  location     = {San Diego, CA, United States},
  pages        = {9062--9093},
  publisher    = {Neural Information Processing Systems Foundation},
  title        = {{Fast rate bounds for multi-task and meta-learning with different sample sizes}},
  doi          = {10.52202/085713-0278},
  volume       = {38},
  year         = {2025},
}

@inproceedings{22830,
  abstract     = {We introduce AutoJudge, a method that accelerates large language model (LLM) inference with task-specific lossy speculative decoding. Instead of matching the original model output distribution token-by-token, we identify the generated tokens that affect the downstream quality of the response, relaxing the distribution match guarantee so that the "unimportant" tokens can be generated faster. Our approach relies on a semi‑greedy search algorithm to test which of the mismatches between target and draft models should be corrected to preserve quality and which ones may be skipped. We then train a lightweight classifier based on existing LLM embeddings to predict, at inference time, which mismatching tokens can be safely accepted without compromising the final answer quality. We evaluate AutoJudge with multiple draft/target model pairs on mathematical reasoning and programming benchmarks, achieving significant speedups at the cost of a minor accuracy reduction. Notably, on GSM8K with the Llama 3.1 70B target model, our approach achieves up to 
≈
2
×
 speedup \textit{over speculative decoding} at the cost of a 
≤
1
%
 drop in accuracy. When applied to the LiveCodeBench benchmark, AutoJudge automatically detects programming-specific important tokens, accepting 
≥
25
 tokens per speculation cycle at a
 
2
%
 drop in Pass@1. Our approach requires no human annotation and is easy to integrate with modern LLM inference frameworks.},
  author       = {Garipov, Roman and Velikonivtsev, Fedor and Ermakov, Ivan and Svirschevski, Ruslan and Egiazarian, Vage and Ryabinin, Max},
  booktitle    = {39th Annual Conference on Neural Information Processing Systems},
  isbn         = {9798331338275},
  issn         = {1049-5258},
  location     = {San Diego, CA, United States},
  pages        = {104904--104941},
  publisher    = {Neural Information Processing Systems Foundation},
  title        = {{AutoJudge: Judge decoding without manual annotation}},
  doi          = {10.52202/085713-3163},
  volume       = {38},
  year         = {2025},
}

@article{19595,
  abstract     = {We investigate the locality of magnetic response in polycyclic aromatic molecules using a novel deep-learning approach. Our method employs graph neural networks (GNNs) with a graph-of-rings representation to predict nucleus independent chemical shifts (NICS) in the space around the molecule. We train a series of models, each time reducing the size of the largest molecules used in training. The accuracy of prediction remains high (MAE < 0.5 ppm), even when training the model only on molecules with up to four rings, thus providing strong evidence for the locality of magnetic response. To overcome the known problem of generalization of GNNs, we implement a k-hop expansion strategy and succeed in achieving accurate predictions for molecules with up to 15 rings (almost 4 times the size of the largest training example). Our findings have implications for understanding the magnetic response in complex molecules and demonstrate a promising approach to overcoming GNN scalability limitations. Furthermore, the trained models enable rapid characterization, without the need for more expensive DFT calculations.},
  author       = {Davidson, Yair and Philipp, Aviad and Chakraborty, Sabyasachi and Bronstein, Alexander and Gershoni-Poranne, Renana},
  issn         = {1089-7690},
  journal      = {Journal of Chemical Physics},
  number       = {14},
  publisher    = {AIP Publishing},
  title        = {{How local is “local”? Deep learning reveals locality of the induced magnetic field of polycyclic aromatic hydrocarbons}},
  doi          = {10.1063/5.0257558},
  volume       = {162},
  year         = {2025},
}

@article{17468,
  abstract     = {Oxygen redox chemistry is central to life1 and many human-made technologies, such as in energy storage2,3,4. The large energy gain from oxygen redox reactions is often connected with the occurrence of harmful reactive oxygen species3,5,6. Key species are superoxide and the highly reactive singlet oxygen3,4,5,6,7, which may evolve from superoxide. However, the factors determining the formation of singlet oxygen, rather than the relatively unreactive triplet oxygen, are unknown. Here we report that the release of triplet or singlet oxygen is governed by individual Marcus normal and inverted region behaviour. We found that as the driving force for the reaction increases, the initially dominant evolution of triplet oxygen slows down, and singlet oxygen evolution becomes predominant with higher maximum kinetics. This behaviour also applies to the widely observed superoxide disproportionation, in which one superoxide is oxidized by another, in both non-aqueous and aqueous systems, with Lewis and Brønsted acidity controlling the driving forces. Singlet oxygen yields governed by these conditions are relevant, for example, in batteries or cellular organelles in which superoxide forms. Our findings suggest ways to understand and control spin states and kinetics in oxygen redox chemistry, with implications for fields, including life sciences, pure chemistry and energy storage.},
  author       = {Mondal, Soumyadip and Nguyen, Huyen T.K. and Hauschild, Robert and Freunberger, Stefan Alexander},
  issn         = {1476-4687},
  journal      = {Nature},
  number       = {8085},
  pages        = {601–605},
  publisher    = {Springer Nature},
  title        = {{Marcus kinetics control singlet and triplet oxygen evolving from superoxide}},
  doi          = {10.1038/s41586-025-09587-7},
  volume       = {646},
  year         = {2025},
}

@inproceedings{19743,
  abstract     = {The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates—lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.},
  author       = {Chatterjee, Krishnendu and Quatmann, Tim and Schäffeler, Maximilian and Weininger, Maximilian and Winkler, Tobias and Zilken, Daniel},
  booktitle    = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031906527},
  issn         = {1611-3349},
  location     = {Hamilton, ON, Canada},
  pages        = {130--151},
  publisher    = {Springer Nature},
  title        = {{Fixed point certificates for reachability and expected rewards in MDPs}},
  doi          = {10.1007/978-3-031-90653-4_7},
  volume       = {15697},
  year         = {2025},
}

@inproceedings{19740,
  abstract     = {Two standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic approach for these problems is the Value Iteration (VI) algorithm which iteratively applies local updates called Bellman updates. There are many practical approaches for VI in the literature but they all require exponentially many Bellman updates for MCs in the worst case. A preprocessing step is an algorithm that is discrete, graph-theoretical, and requires linear space. An important open question is whether, after a polynomial-time preprocessing, VI can be achieved with sub-exponentially many Bellman updates. In this work, we present a new approach for VI based on guessing values. Our theoretical contributions are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm after which, along with guessing values, VI requires only subexponentially many Bellman updates. Second, we present an improved analysis of the speed of convergence of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our new approach. Experimental results show that our approach provides a considerable improvement over existing VI-based approaches on several benchmark examples from the literature.},
  author       = {Chatterjee, Krishnendu and Jafariraviz, Mahdi and Saona Urmeneta, Raimundo J and Svoboda, Jakub},
  booktitle    = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031906527},
  issn         = {1611-3349},
  location     = {Hamilton, ON, Canada},
  pages        = {217--236},
  publisher    = {Springer Nature},
  title        = {{Value iteration with guessing for Markov chains and Markov decision processes}},
  doi          = {10.1007/978-3-031-90653-4_11},
  volume       = {15697},
  year         = {2025},
}

@inproceedings{19744,
  abstract     = {We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature.},
  author       = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Novotný, Petr and Zikelic, Dorde},
  booktitle    = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031906527},
  issn         = {1611-3349},
  location     = {Hamilton, ON, Canada},
  pages        = {279--300},
  publisher    = {Springer Nature},
  title        = {{Refuting equivalence in probabilistic programs with conditioning}},
  doi          = {10.1007/978-3-031-90653-4_14},
  volume       = {15697},
  year         = {2025},
}