arXiv subjects

Peter Müller

Publications and source records attributed to Peter Müller.

At least 37 records · Page 2Linked to original sources

arXiv2025

SIMBA -- A Bayesian Decision Framework for the Identification of Optimal Biomarker Subgroups for Cancer Basket Clinical Trials

We consider basket trials in which a biomarker-targeting drug may be efficacious for patients across different disease indications. Patients are enrolled if their cells exhibit some levels of biomarker expression. The threshold level is allowed to vary by indication. The proposed SIMBA method uses a decision framework to identify optimal biomarker subgroups (OBS) defined by an optimal biomarker threshold for each indication. The optimality is achieved through minimizing a posterior expected loss that balances estimation accuracy and investigator preference for broadly effective therapeutics. A Bayesian hierarchical model is proposed to adaptively borrow information across indications and enhance the accuracy in the estimation of the OBS. The operating characteristics of SIMBA are assessed via simulations and compared against a simplified version and an existing alternative method, both of which do not borrow information. SIMBA is expected to improve the identification of patient sub-populations that may benefit from a biomarker-driven therapeutics.

stat.AP↗

arXiv2025

Borrowing strength between unaligned binary time-series via Bayesian nonparametric rescaling of Unified Skewed Normal priors

We define a Bayesian semi-parametric model to effectively conduct inference with unaligned longitudinal binary data. The proposed strategy is motivated by data from the Human Epilepsy Project (HEP), which collects seizure occurrence data for epilepsy patients, together with relevant covariates. The model is designed to flexibly accommodate the particular challenges that arise with such data. First, epilepsy data require models that can allow for extensive heterogeneity, across both patients and time. With this regard, state space models offer a flexible, yet still analytically amenable class of models. Nevertheless, seizure time-series might share similar behavioral patterns, such as local prolonged periods of elevated seizure presence, which we refer to as "clumping". Such similarities can be used to share strength across patients and define subgroups. However, due to the lack of alignment, straightforward hierarchical modeling of latent state space parameters is not practicable. To overcome this constraint, we construct a strategy that preserves the flexibility of individual trajectories while also exploiting similarities across individuals to borrow information through a nonparametric prior. On the one hand, heterogeneity is ensured by (almost) subject-specific state-space submodels. On the other, borrowing of information is obtained by introducing a Pitman-Yor prior on group-specific probabilities for patterns of clinical interest. We design a posterior sampling strategy that leverages recent developments of binary state space models using the Unified Skewed Normal family (SUN). The model, which allows the sharing of information across individuals with similar disease traits over time, can more generally be adapted to any setting characterized by unaligned binary longitudinal data.

stat.ME↗

arXiv2025

The Widom-Sobolev formula for discontinuous matrix-valued symbols

We prove the Widom-Sobolev formula for the asymptotic behaviour of truncated Wiener-Hopf operators with discontinuous matrix-valued symbols for three different classes of test functions. The symbols may depend on both position and momentum except when closing the asymptotics for twice differentiable test functions with Hölder singularities. The cut-off domains are allowed to have piecewise differentiable boundaries. In contrast to the case where the symbol is smooth in one variable, the resulting coefficient in the enhanced area law we obtain here remains as explicit for matrix-valued symbols as it is for scalar-valued symbols.

math.SP↗

arXiv2025

Another Proof of Segre's Theorem about Ovals

In 1955 B. Segre showed that any oval in a projective plane over a finite field of odd order is a conic. His proof constructs a conic which matches the oval in some points and tangents, and then shows that it actually coincides with the oval. The different proof given here parametrizes an affine piece of the oval and shows directly that the parametrization is given by a polynomial of degree $2$.

math.NT↗

arXiv2025

On the return probability of the simple random walk on Galton-Watson trees

We consider the simple random walk on Galton-Watson trees with supercritical offspring distribution, conditioned on non-extinction. In case the offspring distribution has finite support, we prove an upper bound for the annealed return probability to the root which decays subexponentially in time with exponent 1/3. This exponent is optimal. Our result improves the previously known subexponential upper bound with exponent 1/5 by Piau [Ann. Probab. 26, 1016-1040 (1998)]. For offspring distributions with unbounded support but sufficiently fast decay, our method also yields improved subexponential upper bounds.

math.PR↗

arXiv2024

Formal Foundations for Translational Separation Logic Verifiers (extended version)

Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3. The resulting IVL program is then verified using an existing back-end verifier. A soundness proof for such a translational verifier needs to relate the input program and verification logic to the semantics of the IVL, which in turn needs to be connected with the verification logic implemented in the back-end verifiers. Performing such proofs is challenging due to the large semantic gap between the input and output programs and logics, especially for complex verification logics such as separation logic. This paper presents a formal framework for reasoning about translational separation logic verifiers. At its center is a generic core IVL that captures the essence of different separation logics. We define its operational semantics and formally connect it to two different back-end verifiers, which use symbolic execution and verification condition generation, resp. Crucially, this semantics uses angelic non-determinism to enable the application of different proof search algorithms and heuristics in the back-end verifiers. An axiomatic semantics for the core IVL simplifies reasoning about the front-end translation by performing essential proof steps once and for all in the equivalence proof with the operational semantics rather than for each concrete front-end translation. We illustrate the usefulness of our formal framework by instantiating our core IVL with elements of Viper and connecting it to two Viper back-ends as well as a front-end for concurrent separation logic. All our technical results have been formalized in Isabelle/HOL, including the core IVL and its semantics, the semantics of two back-ends for a subset of Viper, and all proofs.

cs.PL↗

arXiv2024

A Multivariate Polya Tree Model for Meta-Analysis with Event Time Distributions

We develop a non-parametric Bayesian prior for a family of random probability measures by extending the Polya tree ($PT$) prior to a joint prior for a set of probability measures $G_1,\dots,G_n$, suitable for meta-analysis with event time outcomes. In the application to meta-analysis $G_i$ is the event time distribution specific to study $i$. The proposed model defines a regression on study-specific covariates by introducing increased correlation for any pair of studies with similar characteristics. The desired multivariate $PT$ model is constructed by introducing a hierarchical prior on the conditional splitting probabilities in the $PT$ construction for each of the $G_i$. The hierarchical prior replaces the independent beta priors for the splitting probability in the $PT$ construction with a Gaussian process prior for corresponding (logit) splitting probabilities across all studies. The Gaussian process is indexed by study-specific covariates, introducing the desired dependence with increased correlation for similar studies. The main feature of the proposed construction is (conditionally) conjugate posterior updating with commonly reported inference summaries for event time data. The construction is motivated by a meta-analysis over cancer immunotherapy studies.

stat.ME↗

arXiv2024

Towards certifiable AI in aviation: landscape, challenges, and opportunities

Artificial Intelligence (AI) methods are powerful tools for various domains, including critical fields such as avionics, where certification is required to achieve and maintain an acceptable level of safety. General solutions for safety-critical systems must address three main questions: Is it suitable? What drives the system's decisions? Is it robust to errors/attacks? This is more complex in AI than in traditional methods. In this context, this paper presents a comprehensive mind map of formal AI certification in avionics. It highlights the challenges of certifying AI development with an example to emphasize the need for qualification beyond performance metrics.

cs.LG↗

arXiv2024

A note about solvable and non-solvable finite groups of the same order type

Two finite groups are said to have the same order type if for each positive integer $n$ both groups have the same number of elements of order $n$. In 1987 John G. Thompson asked if in this case the solvability of one group implies the solvability of the other group. In 2024 Pawel Piwek gave a negative example. He constructed two groups of order $2^{365}\cdot3^{105}\cdot7^{104}\approx7.3\cdot10^{247}$ of the same order type, where only one is solvable. In this note we produce a much smaller example of order $2^{13}\cdot3^4\cdot7^3=227598336$.

math.GR↗

arXiv2024

Verification Algorithms for Automated Separation Logic Verifiers

Most automated program verifiers for separation logic use either symbolic execution or verification condition generation to extract proof obligations, which are then handed over to an SMT solver. Existing verification algorithms are designed to be sound, but differ in performance and completeness. These characteristics may also depend on the programs and properties to be verified. Consequently, developers and users of program verifiers have to select a verification algorithm carefully for their application domain. Taking an informed decision requires a systematic comparison of the performance and completeness characteristics of the verification algorithms used by modern separation logic verifiers, but such a comparison does not exist. This paper describes five verification algorithms for separation logic, three that are used in existing tools and two novel algorithms that combine characteristics of existing symbolic execution and verification condition generation algorithms. A detailed evaluation of implementations of these five algorithms in the Viper infrastructure assesses their performance and completeness for different classes of input programs. Based on the experimental results, we identify candidate portfolios of algorithms that maximize completeness and performance.

cs.PL↗

arXiv2024

Enhanced area law in the Widom-Sobolev formula for the free Dirac operator in arbitrary dimension

We prove a logarithmically enhanced area law for all Rényi entanglement entropies of the ground state of a free gas of relativistic Dirac fermions. Such asymptotics occur in any dimension if the modulus of the Fermi energy is larger than the mass of the particles and in the massless case at Fermi energy zero in one space dimension. In all other cases of mass, Fermi energy and dimension, the entanglement entropy grows no faster than the area of the involved spatial region. The result is established for a general class of test functions which includes the ones corresponding to Rényi entropies and relies on a recently proved extension of the Widom-Sobolev formula to matrix-valued symbols by the authors.

math-ph↗

arXiv2024

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities

Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not change (i.e., are framed) across function calls. However, these type guarantees do not hold in the presence of interior mutability (e.g., when interacting with any concurrent data structure). As a consequence, existing verification techniques for safe code such as Prusti and Creusot are either unsound or fundamentally incomplete if applied to this setting. In this work, we present the first technique capable of automatically verifying safe clients of existing interiorly mutable types. At the core of our approach, we identify a novel notion of implicit capabilities: library-defined properties that cannot be expressed using Rust's types. We propose new annotations to specify these capabilities and a first-order logic encoding suitable for program verification. We have implemented our technique in a verifier called Mendel and used it to prove absence of panics in Rust programs that make use of popular standard-library types with interior mutability, including Rc, Arc, Cell, RefCell, AtomicI32, Mutex and RwLock. Our evaluation shows that these library annotations are useful for verifying usages of real-world libraries, and powerful enough to require zero client-side annotations in many of the verified programs.

cs.PL↗

arXiv2024

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)

Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end generates proof obligations for the IVL program and employs an SMT solver to discharge them. Soundness of such verifiers therefore requires that the front-end translation faithfully captures the semantics of the input program and specification in the IVL program, and that the back-end reports success only if the IVL program is actually correct. For a verification tool to be trustworthy, these soundness conditions must be satisfied by its actual implementation, not just the program logic it uses. In this paper, we present a novel validation methodology that, given a formal semantics for the input language and IVL, provides formal soundness guarantees for front-end implementations. For each run of the verifier, we automatically generate a proof in Isabelle showing that the correctness of the produced IVL program implies the correctness of the input program. This proof can be checked independently from the verifier, in Isabelle, and can be combined with existing work on validating back-ends to obtain an end-to-end soundness result. Our methodology based on forward simulation employs several modularisation strategies to handle the large semantic gap between the input language and the IVL, as well as the intricacies of practical, optimised translations. We present our methodology for the widely-used Viper and Boogie languages. Our evaluation shows that it is effective in validating the translations performed by the existing Viper implementation.

cs.PL↗

arXiv2024

Protocols to Code: Formal Verification of a Next-Generation Internet Router

We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed.

cs.CR↗

arXiv2024

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)

Hoare logics are proof systems that allow one to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (such as functional correctness). Hoare logic has been generalized to prove also properties of multiple executions of a program (so-called hyperproperties, such as determinism or non-interference). These program logics prove the absence of (bad combinations of) executions. On the other hand, program logics similar to Hoare logic have been proposed to disprove program properties (e.g., Incorrectness Logic), by proving the existence of (bad combinations of) executions. All of these logics have in common that they specify program properties using assertions over a fixed number of states, for instance, a single pre- and post-state for functional properties or pairs of pre- and post-states for non-interference. In this paper, we present Hyper Hoare Logic, a generalization of Hoare logic that lifts assertions to properties of arbitrary sets of states. The resulting logic is simple yet expressive: its judgments can express arbitrary program hyperproperties, a particular class of hyperproperties over the set of terminating executions of a program (including properties of individual program executions). By allowing assertions to reason about sets of states, Hyper Hoare Logic can reason about both the absence and the existence of (combinations of) executions, and, thereby, supports both proving and disproving program (hyper-)properties within the same logic, including (hyper-)properties that no existing Hoare logic can express. We prove that Hyper Hoare Logic is sound and complete, and demonstrate that it captures important proof principles naturally. All our technical results have been proved in Isabelle/HOL.

cs.LO↗

arXiv2024

Dir-SPGLM: A Bayesian semiparametric GLM with data-driven reference distribution

The recently developed semi-parametric generalized linear model (SPGLM) offers more flexibility as compared to the classical GLM by including the baseline or reference distribution of the response as an additional parameter in the model. However, some inference summaries are not easily generated under existing maximum-likelihood based inference (ML-SPGLM). This includes uncertainty in estimation for model-derived functionals such as exceedance probabilities. The latter are critical in a clinical diagnostic or decision-making setting. In this article, by placing a Dirichlet prior on the baseline distribution, we propose a Bayesian model-based approach for inference to address these important gaps. We establish consistency and asymptotic normality results for the implied canonical parameter. Simulation studies and an illustration with data from an aging research study confirm that the proposed method performs comparably or better in comparison with ML-SPGLM. The proposed Bayesian framework is most attractive for inference with small sample training data or in sparse-data scenarios.

stat.ME↗

arXiv2023

A note on Galois groups of linearized polynomials

Let $L(X)$ be a monic $q$-linearized polynomial over $F_q$ of degree $q^n$, where $n$ is an odd prime. Recently Gow and McGuire showed that the Galois group of $L(X)/X-t$ over the field of rational functions $F_q(t)$ is $GL_n(q)$ unless $L(X)=X^{q^n}$. The case of even $q$ remained open, but it was conjectured that the result holds too and partial results were given. In this note we settle this conjecture. In fact we use Hensel's Lemma to give a unified proof for all prime powers $q$.

math.NT↗

arXiv2023

Refinement Proofs in Rust Using Ghost Locks

Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate executable code automatically, which generally leads to implementations with sub-optimal performance. Others employ bottom-up program verification to reason about efficient implementations, but impose strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools. In this paper, we present a novel refinement technique that removes these limitations. It supports a wide range of program structures, data representations, and proof structures. Our approach supports reasoning about both safety and liveness properties. We implement our approach in a state-of-the-art verifier for the Rust language, which itself offers a strong foundation for memory safety. We demonstrate the practicality of our approach on a number of substantial case studies.

cs.LO↗