@article{19703, abstract = {An enlarged brain underlies the complex central nervous system of vertebrates. The dramatic expansion of the brain that diverges its shape from the spinal cord follows neural tube closure during embryonic development. Here, we show that this differential deformation is encoded by a pre-pattern of tissue material properties in chicken embryos. Using magnetic droplets and atomic force microscopy, we demonstrate that the dorsal hindbrain is more fluid than the dorsal spinal cord, resulting in a thinning versus a resisting response to increasing lumen pressure, respectively. The dorsal hindbrain exhibits reduced apical actin and a disorganized laminin matrix consistent with tissue fluidization. Blocking the activity of neural-crest-associated matrix metalloproteinases inhibits hindbrain expansion. Transplanting dorsal hindbrain cells to the spinal cord can locally create an expanded brain-like morphology in some cases. Our findings raise questions in vertebrate head evolution and suggest a general role of mechanical pre-patterning in sculpting epithelial tubes.}, author = {Mclaren, Susannah B.P. and Xue, Shi-lei and Ding, Siyuan and Winkel, Alexander K. and Baldwin, Oscar and Dwarakacherla, Shreya and Franze, Kristian and Hannezo, Edouard B and Xiong, Fengzhu}, issn = {1878-1551}, journal = {Developmental Cell}, number = {17}, pages = {2237--2247.e4}, publisher = {Elsevier}, title = {{Differential tissue deformability underlies fluid pressure-driven shape divergence of the avian embryonic brain and spinal cord}}, doi = {10.1016/j.devcel.2025.04.010}, volume = {60}, year = {2025}, } @inproceedings{19712, abstract = {We study recent algebraic attacks (Briaud-Øygarden EC’23) on the Regular Syndrome Decoding (RSD) problem and the assumptions underlying the correctness of their attacks’ complexity estimates. By relating these assumptions to interesting algebraic-combinatorial problems, we prove that they do not hold in full generality. However, we show that they are (asymptotically) true for most parameter sets, supporting the soundness of algebraic attacks on RSD. Further, we prove—without any heuristics or assumptions—that RSD can be broken in polynomial time whenever the number of error blocks times the square of the size of error blocks is larger than 2 times the square of the dimension of the code. Additionally, we use our methodology to attack a variant of the Learning With Errors problem where each error term lies in a fixed set of constant size. We prove that this problem can be broken in polynomial time, given a sufficient number of samples. This result improves on the seminal work by Arora and Ge (ICALP’11), as the attack’s time complexity is independent of the LWE modulus.}, author = {Cueto Noval, Miguel and Merz, Simon-Philipp and Stählin, Patrick and Ünal, Akin}, booktitle = {44th Annual International Conference on the Theory and Applications of Cryptographic Techniques}, isbn = {9783031910944}, issn = {1611-3349}, location = {Madrid, Spain}, pages = {385--415}, publisher = {Springer Nature}, title = {{On the soundness of algebraic attacks against code-based assumptions}}, doi = {10.1007/978-3-031-91095-1_14}, volume = {15606}, year = {2025}, } @article{19713, abstract = {Distributed optimization is the standard way of speeding up machine learning training, and most of the research in the area focuses on distributed first-order, gradient-based methods. Yet, there are settings where some computationally-bounded nodes may not be able to implement first-order, gradient-based optimization, while they could still contribute to joint optimization tasks. In this paper, we initiate the study of hybrid decentralized optimization, studying settings where nodes with zeroth-order and first-order optimization capabilities co-exist in a distributed system, and attempt to jointly solve an optimization task over some data distribution. We essentially show that, under reasonable parameter settings, such a system can not only withstand noisier zeroth-order agents but can even benefit from integrating such agents into the optimization process, rather than ignoring their information. At the core of our approach is a new analysis of distributed optimization with noisy and possibly-biased gradient estimators, which may be of independent interest. Our results hold for both convex and non-convex objectives. Experimental results on standard optimization tasks confirm our analysis, showing that hybrid first-zeroth order optimization can be practical, even when training deep neural networks.}, author = {Talaei, Shayan and Ansaripour, Matin and Nadiradze, Giorgi and Alistarh, Dan-Adrian}, issn = {2374-3468}, journal = {Proceedings of the 39th AAAI Conference on Artificial Intelligence}, number = {19}, pages = {20778--20786}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Hybrid decentralized optimization: Leveraging both first- and zeroth-order optimizers for faster convergence}}, doi = {10.1609/aaai.v39i19.34290}, volume = {39}, year = {2025}, } @unpublished{19717, abstract = {Radial glial progenitors (RGPs) generate all projection neurons (PNs) in the cerebral cortex through incompletely understood processes. Herein, we combine Mosaic Analysis with Double Markers (MADM)-based clonal analysis at embryonic days 12.5 and 13.5 with early postnatal callosal tracing to reveal a lineage progression that challenges the inside-outside model of cortical development and the conventional view of an invariable sequence of asymmetric neurogenic divisions. Our data demonstrate that early multipotent RGPs generate all extra-telencephalic (ET) and intra-telencephalic (IT) PNs across all layers through parallel sublineages and the random specification, during the earliest neurogenic divisions, of fate-restricted daughter RGPs. While the neuronal production of the parental multipotent RGPs consists of small ET-PN or IT-PN outputs, fate-restricted RGPs produce larger translaminar outputs spanning deep and upper layers of only IT-PNs, the predominant mammalian PN subtype. We further show that the emergence of IT-PN fate-restricted RGPs also leads to quantitatively and temporally stereotyped neurogenesis population-wise.}, author = {Varela-Martínez, I and Villalba Requena, Ana and Garcia-Marqués, J. and Hippenmeyer, Simon and Nieto, M.}, booktitle = {bioRxiv}, title = {{Early emergence of projection-subtype fate-restricted radial glial progenitors orchestrates neocortical neurogenesis}}, doi = {10.1101/2025.05.07.652665}, year = {2025}, } @article{19725, abstract = {Protein-protein interactions (PPIs) mediate many fundamental cellular processes. Control of PPIs through optically or chemically responsive protein domains has had a profound impact on basic research and some clinical applications. Most chemogenetic methods induce the association, i.e., dimerization or oligomerization, of target proteins, whilst the few available dissociation approaches either break large oligomeric protein clusters or heteromeric complexes. Here, we have exploited the controlled dissociation of a homodimeric oxidoreductase from mycobacteria (MSMEG_2027) by its native cofactor, F420, which is not present in mammals, as a bioorthogonal monomerization switch. Using X-ray crystallography, we found that in the absence of F420 MSMEG_2027 forms a unique domain-swapped dimer that occludes the cofactor binding site. Rearrangement of the N-terminal helix upon F420 binding results in the dissolution of the dimer. We then showed that MSMEG_2027 can be fused to proteins of interest in human cells and applied it as a tool to induce and release MAPK/ERK signalling downstream of a chimeric fibroblast growth factor receptor 1 (FGFR1) tyrosine kinase. This F420-dependent chemogenetic de-homodimerization tool is stoichiometric and based on a single domain and thus represents a novel mechanism to investigate protein complexes in situ.}, author = {Antoney, James and Kainrath, Stephanie and Dubowsky, Joshua G. and Ahmed, F. Hafna and Kang, Suk Woo and Mackie, Emily R.R. and Bracho Granado, Gustavo and Soares Da Costa, Tatiana P. and Jackson, Colin J. and Janovjak, Harald L}, issn = {1089-8638}, journal = {Journal of Molecular Biology}, number = {17}, publisher = {Elsevier}, title = {{A F420-dependent single domain chemogenetic tool for protein de-dimerization}}, doi = {10.1016/j.jmb.2025.169184}, volume = {437}, year = {2025}, } @article{19726, abstract = {The oxidation of biomass-derived compounds such as glucose within electrochemical cells enables both the energy-efficient production of hydrogen and the generation of additional added-value chemicals from biomass. However, for this biomass valorization approach to become commercially viable, selective, cost-effective, and highly active electrooxidation catalysts need to be developed. In this work, we detail the synthesis of a nickel (Ni) and zinc (Zn)-based electrocatalyst for the glucose oxidation reaction (GOR) to formic acid (FoA) via calcination of a Zn-based zeolitic imidazole framework (ZIF) functionalized with ethylenediamine and doped with Ni. The structure, morphology, and electrochemical performance of the catalysts towards the anodic GOR to FoA coupled with the cathodic hydrogen evolution reaction (HER) are subsequently studied. Chronopotentiometry tests with 0.1 M of glucose show a conversion of 94 % at 250 mA in only 70 min, with a Faradaic efficiency (FE) of 91 % toward the production of FoA. Meanwhile, at the cathode, the HER FE is close to 98 %.}, author = {Mejia-Centeno, Karol V. and Montaña-Mora, Guillem and Chacón-Borrero, Jesús and Xue, Qian and Gong, Li and Martí-Sánchez, Sara and Berlanga-Vázquez, Armando and Llorca, Jordi and Ibáñez, Maria and Arbiol, Jordi and Qi, Xueqiang and Martinez-Alanis, Paulina R. and Cabot, Andreu}, issn = {1385-8947}, journal = {Chemical Engineering Journal}, publisher = {Elsevier}, title = {{Glucose electrooxidation with simultaneous H2 production on nickel-zinc electrocatalysts derived from an ethylenediamine-functionalized zeolitic imidazole framework}}, doi = {10.1016/j.cej.2025.163491}, volume = {515}, year = {2025}, } @article{19727, abstract = {By studying some Clausen-like multiple Dirichlet series, we complete the proof of Manin's conjecture for sufficiently split smooth equivariant compactifications of the translation-dilation group over the rationals. Secondary terms remain elusive in general.}, author = {Wang, Victor}, issn = {1090-2082}, journal = {Advances in Mathematics}, publisher = {Elsevier}, title = {{Asymptotic growth of translation-dilation orbits}}, doi = {10.1016/j.aim.2025.110341}, volume = {475}, year = {2025}, } @article{19729, abstract = {From anthropogenic litter carried by ocean currents to plant stems travelling through the atmosphere, geophysical flows are often seeded with elongated, fibre-like particles. In this study, we used a large-scale laboratory model of a tidal current – representative of a widespread class of geophysical flows – to investigate the tumbling motion of long, slender and floating fibres in the complex turbulence generated by flow interactions with a tidal inlet. Despite the non-stationary, non-homogeneous and anisotropic nature of this turbulence, we find that long fibres statistically rotate at the same frequency as eddies of similar size, a phenomenon called scale selection, which is known to occur in ideal turbulence. Furthermore, we report that the signal of the instantaneous transverse velocity difference between the fibre ends changes significantly from the signal produced by the flow in the fibre surroundings, although the two are statistically equivalent. These observations have twofold implications. On the one hand, they confirm the reliability of using the end-to-end velocity signal of rigid fibres to probe the two-point transverse statistics of the flow, even under realistic conditions: oceanographers could exploit this observation to measure transverse velocity differences through elongated floats in the field, where superdiffusion complicates collecting sufficient data to probe two-point turbulence statistics at a fixed separation effectively. On the other hand, by addressing the dynamics of inertial range particles floating in the coastal zone, these observations are crucial to improving our ability to predict the fate of meso- and macro-litter, a size class that is currently understudied.}, author = {De Leo, Annalisa and Brizzolara, Stefano and Cavaiola, Mattia and He, Junlin and Stocchino, Alessandro}, issn = {1469-7645}, journal = {Journal of Fluid Mechanics}, publisher = {Cambridge University Press}, title = {{Rigid fibre transport in a periodic non-homogeneous geophysical turbulent flow}}, doi = {10.1017/jfm.2025.362}, volume = {1011}, year = {2025}, } @article{19730, abstract = {Feigenbaum universality is shown to occur in subcritical shear flows. Our testing ground is the counter-rotation regime of the Taylor–Couette flow, where numerical calculations are performed within a small periodic domain. The accurate computation of up to the seventh period-doubling bifurcation, assisted by a purposely defined Poincaré section, has enabled us to reproduce the two Feigenbaum universal constants with unprecedented accuracy in a fluid flow problem. We have further devised a method to predict the bifurcation diagram up to the accumulation point of the cascade based on the detailed inspection of just the first few period-doubling bifurcations. Remarkably, the method is applicable beyond the accumulation point, with predictions remaining valid, in a statistical sense, for the chaotic dynamics that follows.}, author = {Wang, Baoying and Ayats López, Roger and Deguchi, K. and Meseguer, A. and Mellibovsky, F.}, issn = {1469-7645}, journal = {Journal of Fluid Mechanics}, publisher = {Cambridge University Press}, title = {{Feigenbaum universality in subcritical Taylor-Couette flow}}, doi = {10.1017/jfm.2025.278}, volume = {1010}, year = {2025}, } @article{19731, abstract = {In an era of high-resolution displays, powerful design software, and automated plotting tools, one would think that scientific figures would be clearer than ever. Yet, despite numerous editorials, guidelines, and workshops dedicated to improving figure design, poorly constructed figures remain a persistent issue. Editors and experienced researchers have repeatedly highlighted key pitfalls such as cluttered layouts, inconsistent formatting, poor color choices, and misleading visuals. (1−8) Yet, the aforementioned graphical shortcomings continue to plague even high-impact journals. Why? The problem is not a lack of technology; it is a combination of poor design habits, rushed deadlines, and a tendency to treat figures as mere “data dumps” rather than as essential storytelling tools. Many people process information more effectively through visuals, naturally associating concepts easily when presented graphically. A well-crafted figure serves as a narrative within the larger story, making complex ideas more accessible. Unfortunately, visual storytelling often takes a backseat in scientific communication. Scientists are trained to analyze and interpret data, but many default to software-generated plots without considering accessibility or how their figures will be perceived by readers outside their immediate field. Without thoughtful design, figures lose their power to enhance understanding, ultimately limiting the significance of the research itself. In this editorial, we examine the challenges that, in our view, hamper scientific figure design and discuss how thoughtful refinements driven by feedback, iteration, and design principles can enhance clarity and impact visual communication.}, author = {Rayaroth Puthiyaveettil, Aiswarya and Fiedler, Christine and Ibáñez, Maria}, issn = {2694-2461}, journal = {ACS Materials Au}, number = {3}, pages = {438--440}, publisher = {American Chemical Society}, title = {{Let us FIGURE it out: Why do scientists still make “bad” figures?}}, doi = {10.1021/acsmaterialsau.5c00037}, volume = {5}, year = {2025}, } @article{19732, abstract = {The transition to chaos in the subcritical regime of counter-rotating Taylor–Couette flow is investigated using a minimal periodic domain capable of sustaining coherent structures. Following a Feigenbaum cascade, the dynamics is found to be remarkably well approximated by a simple discrete map that admits rigorous proof of its chaotic nature. The chaotic set that arises for the map features densely distributed periodic points that are in one-to-one correspondence with unstable periodic orbits (UPOs) of the Navier–Stokes system. This supports the increasingly accepted view that UPOs may serve as the backbone of turbulence and, indeed, we demonstrate that it is possible to reconstruct every statistical property of chaotic fluid flow from UPOs.}, author = {Wang, Baoying and Ayats López, Roger and Deguchi, K. and Meseguer, A. and Mellibovsky, F.}, issn = {1469-7645}, journal = {Journal of Fluid Mechanics}, publisher = {Cambridge University Press}, title = {{Mathematically established chaos and forecast of statistics with recurrent patterns in Taylor-Couette flow}}, doi = {10.1017/jfm.2025.151}, volume = {1011}, year = {2025}, } @article{19733, abstract = {One of the most striking quantum phenomena is superposition, where one particle simultaneously inhabits different states. Most methods to verify coherent superposition are indirect, in that they require the distinct states to be recombined. Here, we adapt an xor game, in which a “test” photon is placed in a superposition of two orthogonal spatial modes, and each mode is sent to separated parties who perform local measurements on their modes without reinterfering the original modes. We show that by using a second identical “measurement” photon the parties are nonetheless able to verify if the test photon was placed in coherent superposition of the two spatial modes. We then turn this game into a resource-efficient verification scheme, obtaining a confidence that the particle is superposed which approaches unity exponentially fast. We demonstrate our scheme using a single photon, obtaining a 99% confidence that the particle is superposed with only 37 copies. Our work shows the utility of xor games to verify quantum resources, allowing us to efficiently detect quantum superposition without reinterfering the superposed modes.}, author = {Kun, Daniel and Strömberg, Karl T and Spagnolo, Michele and Dakić, Borivoje and Rozema, Lee A. and Walther, Philip}, issn = {2469-9934}, journal = {Physical Review A}, number = {5}, publisher = {American Physical Society}, title = {{Direct and efficient detection of quantum superposition}}, doi = {10.1103/PhysRevA.111.L050402}, volume = {111}, year = {2025}, } @article{19736, abstract = {The phytohormone auxin is a major signal coordinating growth and development in plants. The variety of its effects arises from its ability to form local auxin maxima and gradients within tissues, generated through directional cell-to-cell transport and elaborate metabolic control. These auxin distribution patterns instruct cells in a context-dependent manner to undergo predefined developmental transitions. In this Review, we discuss advances in auxin action at the level of homeostasis and signalling. We highlight key insights into the structural basis of PIN-mediated intercellular auxin transport and explore two novel non-transcriptional auxin signalling mechanisms: one involving intracellular Ca2+ transients and another involving cell-surface auxin perception that mediates global, ultrafast phosphorylation. Furthermore, we examine emerging evidence indicating the involvement of cyclic adenosine monophosphate as a second messenger in the transcriptional auxin response. Together, these recent developments in auxin research have profoundly deepened our understanding of the complex and diverse activities of auxin in plant growth and development.}, author = {Vanneste, Steffen and Pei, Yuanrong and Friml, Jiří}, issn = {1471-0080}, journal = {Nature Reviews Molecular Cell Biology}, publisher = {Springer Nature}, title = {{Mechanisms of auxin action in plant growth and development}}, doi = {10.1038/s41580-025-00851-2}, year = {2025}, } @article{19737, abstract = {For general large non–Hermitian random matrices X and deterministic normal deformations A, we prove that the local eigenvalue statistics of A + X close to the critical edge points of its spectrum are universal. This concludes the proof of the third and last remaining typical universality class for non–Hermitian random matrices (for normal deformations), after bulk and sharp edge universalities have been established in recent years.}, author = {Cipolloni, Giorgio and Erdös, László and Ji, Hong Chang}, issn = {1432-2064}, journal = {Probability Theory and Related Fields}, publisher = {Springer Nature}, title = {{Non–Hermitian spectral universality at critical points}}, doi = {10.1007/s00440-025-01384-7}, year = {2025}, } @inproceedings{19738, abstract = {Garbling is a fundamental cryptographic primitive, with numerous theoretical and practical applications. Since the first construction by Yao (FOCS’82, ’86), a line of work has concerned itself with reducing the communication and computational complexity of that construction. One of the most efficient garbling schemes presently is the ‘Half Gates’ scheme by Zahur, Rosulek, and Evans (Eurocrypt’15). Despite its widespread adoption, the provable security of this scheme has been based on assumptions whose only instantiations are in idealized models. For example, in their original paper, Zahur, Rosulek, and Evans showed that hash functions satisfying a notion called circular correlation robustness (CCR) suffice for this task, and then proved that CCR secure hash functions can be instantiated in the random permutation model. In this work, we show how to securely instantiate the Half Gates scheme in the standard model. To this end, we first show how this scheme can be securely instantiated given a (family of) weak CCR hash function, a notion that we introduce. Furthermore, we show how a weak CCR hash function can be used to securely instantiate other efficient garbling schemes, namely the ones by Rosulek and Roy (Crypto’21) and Heath (Eurocrypt’24). Thus we believe this notion to be of independent interest. Finally, we construct such weak CCR hash functions using indistinguishability obfuscation and one-way functions. The security proof of this construction constitutes our main technical contribution. While our construction is not practical, it serves as a proof of concept supporting the soundness of these garbling schemes, which we regard to be particularly important given the recent initiative by NIST to standardize garbling, and the optimizations in Half Gates being potentially adopted.}, author = {Acharya, Anasuya and Azari, Karen and Baig, Mirza Ahad and Hofheinz, Dennis and Kamath, Chethan}, booktitle = {28th IACR International Conference on Practice and Theory of Public-Key Cryptography}, isbn = {9783031918285}, issn = {1611-3349}, location = {Roros, Norway}, pages = {37--75}, publisher = {Springer Nature}, title = {{Securely instantiating ‘Half Gates’ garbling in the standard model}}, doi = {10.1007/978-3-031-91829-2_2}, volume = {15677}, year = {2025}, } @inproceedings{19739, abstract = {Cooperative verification is gaining momentum in recent years. The usual setup in cooperative verification is that a verifier A is run with some pre-defined resources, and if it is not able to verify the program, the verification task is passed to a verifier B together with information learned about the program by verifier A, then the chain can continue to a verifier C, and so on. This scheme is static: tools run one after another in a fixed pre-defined order and fixed parameters and resource limits (the scheme may differ for properties to be analyzed, though). Bubaak is a program analysis tool that allows to run multiple program verifiers in a dynamically changing combination of parallel and sequential portfolios. Bubaak starts the verification process by invoking an initial set of tasks; every task, when it is done (e.g., because of hitting a time limit or finishing its job), rewrites itself into one or more successor tasks. New tasks can be also spawned upon events generated by other tasks. This all happens dynamically based on the information gathered by finished and running tasks. During their execution, tasks that run in parallel can exchange (partial) verification artifacts, either directly or with Bubaak as an intermediary.}, author = {Chalupa, Marek and Richter, Cedric}, booktitle = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783031906596}, issn = {1611-3349}, location = {Hamilton, ON, Canada}, pages = {212--216}, publisher = {Springer Nature}, title = {{BUBAAK: Dynamic cooperative verification}}, doi = {10.1007/978-3-031-90660-2_14}, volume = {15698}, 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{19742, abstract = {Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The modes SMC tool implements our methods and recommendations, which we use to experimentally confirm our results.}, author = {Budde, Carlos E. and Hartmanns, Arnd and Meggendorfer, Tobias and Weininger, Maximilian and Wienhöft, Patrick}, booktitle = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783031906428}, issn = {1611-3349}, location = {Hamilton, ON, Canada}, pages = {167--190}, publisher = {Springer Nature}, title = {{Sound statistical model checking for probabilities and expected rewards}}, doi = {10.1007/978-3-031-90643-5_9}, volume = {15696}, 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{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}, }