Searcharxiv⌕ Search

arXiv subjects

Peter Müller

Publications and source records attributed to Peter Müller.

At least 73 records · Page 4Linked to original sources
arXiv2021

VerifyThis 2019: A Program Verification Competition (Extended Report)

VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties -- something that lies beyond the capabilities of fully automatic verification, and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned two days of work. The report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.

cs.LO↗
arXiv2021

Localisation for Delone operators via Bernoulli randomisation

Delone operators are Schrödinger operators in multi-dimensional Euclidean space with a potential given by the sum of all translates of a given "single-site potential" centred at the points of a Delone set. In this paper, we use randomisation to study dynamical localisation for families of Delone operators. We do this by suitably adding more points to a Delone set and by introducing i.i.d. Bernoulli random variables as coupling constants at the additional points. The resulting non-ergodic continuum Anderson model with Bernoulli disorder is accessible to the latest version of the multiscale analysis. The novel ingredient here is the initial length-scale estimate whose proof is hampered due to the non-periodic background potential. It is obtained by the use of a quantitative unique continuation principle. As applications we obtain both probabilistic and topological statements about dynamical localisation. Among others, we show that Delone sets for which the associated Delone operators exhibit dynamical localisation at the bottom of the spectrum are dense in the space of Delone sets.

math-ph↗
arXiv2020

Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification

Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full verification of entire systems is feasible by establishing a refinement relation between an abstract system specification and an executable implementation. Existing approaches however impose severe restrictions on either the abstract system specifications due to their limited expressiveness or versatility, or on the executable code due to their reliance on suboptimal code extraction or inexpressive program logics. We propose a novel methodology that combines the compositional refinement of abstract, event-based models of distributed systems with the verification of full-fledged program code using expressive separation logics, which support features of realistic programming languages like mutable heap data structures and concurrency. The main technical contribution of our work is a formal framework that soundly relates event-based system models to program specifications in separation logics, such that successful verification establishes a refinement relation between the model and the code. We formalized our framework, Igloo, in Isabelle/HOL. Our framework enables the sound combination of tools for protocol development with existing program verifiers. We report on three case studies, a leader election protocol, a replication protocol, and a security protocol, for which we refine formal requirements into program specifications (in Isabelle/HOL) that we implement in Java and Python and prove correct using the VeriFast and Nagini tools.

cs.LO↗
arXiv2020

Bayesian Nonparametric Bivariate Survival Regression for Current Status Data

We consider nonparametric inference for event time distributions based on current status data. We show that in this scenario conventional mixture priors, including the popular Dirichlet process mixture prior, lead to biologically uninterpretable results as they unnaturally skew the probability mass for the event times toward the extremes of the observed data. Simple assumptions on dependent censoring can fix the problem. We then extend the discussion to bivariate current status data with partial ordering of the two outcomes. In addition to dependent censoring, we also exploit some minimal known structure relating the two event times. We design a Markov chain Monte Carlo algorithm for posterior simulation. Applied to a recurrent infection study, the method provides novel insights into how symptoms-related hospital visits are affected by covariates.

stat.ME↗
arXiv2020

Clustering and Prediction with Variable Dimension Covariates

In many applied fields incomplete covariate vectors are commonly encountered. It is well known that this can be problematic when making inference on model parameters, but its impact on prediction performance is less understood. We develop a method based on covariate dependent partition models that seamlessly handles missing covariates while completely avoiding any type of imputation. The method we develop allows in-sample predictions as well as out-of-sample prediction, even if the missing pattern in the new subjects' incomplete covariate vector was not seen in the training data. Any data type, including categorical or continuous covariates are permitted. In simulation studies the proposed method compares favorably. We illustrate the method in two application examples.

stat.ME↗
arXiv2020

Stability of the enhanced area law of the entanglement entropy

We consider a multi-dimensional continuum Schrödinger operator which is given by a perturbation of the negative Laplacian by a compactly supported potential. We establish both an upper and a lower bound on the bipartite entanglement entropy of the ground state of the corresponding quasi-free Fermi gas. The bounds prove that the scaling behaviour of the entanglement entropy remains a logarithmically enhanced area law as in the unperturbed case of the free Fermi gas. The central idea for the upper bound is to use a limiting absorption principle for such kinds of Schrödinger operators.

math-ph↗
arXiv2019

A Semi-parametric Bayesian Approach to Population Finding with Time-to-Event and Toxicity Data in a Randomized Clinical Trial

A utility-based Bayesian population finding (BaPoFi) method was proposed by Morita and Müller (2017, Biometrics, 1355-1365) to analyze data from a randomized clinical trial with the aim of identifying good predictive baseline covariates for optimizing the target population for a future study. The approach casts the population finding process as a formal decision problem together with a flexible probability model using a random forest to define a regression mean function. BaPoFi is constructed to handle a single continuous or binary outcome variable. In this paper, we develop BaPoFi-TTE as an extension of the earlier approach for clinically important cases of time-to-event (TTE) data with censoring, and also accounting for a toxicity outcome. We model the association of TTE data with baseline covariates using a semi-parametric failure time model with a Pólya tree prior for an unknown error term and a random forest for a flexible regression mean function. We define a utility function that addresses a trade-off between efficacy and toxicity as one of the important clinical considerations for population finding. We examine the operating characteristics of the proposed method in extensive simulation studies. For illustration, we apply the proposed method to data from a randomized oncology clinical trial. Concerns in a preliminary analysis of the same data based on a parametric model motivated the proposed more general approach.

stat.AP↗
arXiv2019

Modular Verification of Heap Reachability Properties in Separation Logic

The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between objects in the heap. Reasoning about reachability is difficult for two main reasons. First, any heap modification may affect an unbounded number of reference chains, which complicates modular verification, in particular, framing. Second, general graph reachability is not supported by SMT solvers, which impedes automatic verification. In this paper, we present a modular specification and verification technique for reachability properties in separation logic. For each method, we specify reachability only locally within the fragment of the heap on which the method operates. A novel form of reachability framing for relatively convex subheaps allows one to extend reachability properties from the heap fragment of a callee to the larger fragment of its caller, enabling precise procedure-modular reasoning. Our technique supports practically important heap structures, namely acyclic graphs with a bounded outdegree as well as (potentially cyclic) graphs with at most one path (modulo cycles) between each pair of nodes. The integration into separation logic allows us to reason about reachability and other properties in a uniform way, to verify concurrent programs, and to automate our technique via existing separation logic verifiers. We demonstrate that our verification technique is amenable to SMT-based verification by encoding a number of benchmark examples into the Viper verification infrastructure.

cs.PL↗
arXiv2019

A Bayesian Nonparametric Approach for Evaluating the Causal Effect of Treatment in Randomized Trials with Semi-Competing Risks

We develop a Bayesian nonparametric (BNP) approach to evaluate the causal effect of treatment in a randomized trial where a nonterminal event may be censored by a terminal event, but not vice versa (i.e., semi-competing risks). Based on the idea of principal stratification, we define a novel estimand for the causal effect of treatment on the nonterminal event. We introduce identification assumptions, indexed by a sensitivity parameter, and show how to draw inference using our BNP approach. We conduct simulation studies and illustrate our methodology using data from a brain cancer trial.

stat.ME↗
arXiv2019

Perturbations of continuum random Schrödinger operators with applications to Anderson orthogonality and the spectral shift function

We study effects of a bounded and compactly supported perturbation on multi-dimensional continuum random Schrödinger operators in the region of complete localisation. Our main emphasis is on Anderson orthogonality for random Schrödinger operators. Among others, we prove that Anderson orthogonality does occur for Fermi energies in the region of complete localisation with a non-zero probability. This partially confirms recent non-rigorous findings [V. Khemani et al., Nature Phys. 11, 560-565 (2015)]. The spectral shift function plays an important role in our analysis of Anderson orthogonality. We identify it with the index of the corresponding pair of spectral projections and explore the consequences thereof. All our results rely on the main technical estimate of this paper which guarantees separate exponential decay of the disorder-averaged Schatten $p$-norm of $χ_{a}(f(H) - f(H^τ)) χ_{b}$ in $a$ and $b$. Here, $H^τ$ is a perturbation of the random Schrödinger operator $H$, $χ_{a}$ is the multiplication operator corresponding to the indicator function of a unit cube centred about $a\in\mathbb{R}^{d}$, and $f$ is in a suitable class of functions of bounded variation with distributional derivative supported in the region of complete localisation for $H$.

math-ph↗
arXiv2019

Nuclear Charge Radii of $^{10,11}$B

The first determination of the nuclear charge radius by laser spectroscopy for a five-electron system is reported. This is achieved by combining high-accuracy ab initio mass-shift calculations and a high-resolution measurement of the isotope shift in the $2s^2 2p\, ^2\mathrm{P}_{1/2} \rightarrow 2s^2 3s\, ^2\mathrm{S}_{1/2}$ ground state transition in boron atoms. Accuracy is increased by orders of magnitude for the stable isotopes $^{10,11}$B and the results are used to extract their difference in the mean-square charge radius $\langle r^2_\mathrm{c}\rangle^{11} - \langle r^2_\mathrm{c}\rangle^{10} = -0.49\,(12)\,\mathrm{fm}^2$. The result is qualitatively explained by a possible cluster structure of the boron nuclei and quantitatively used as a benchmark for new ab initio nuclear structure calculations using the no-core shell model and Green's function Monte Carlo approaches.

physics.atom-ph↗
arXiv2018

Specification Mining for Smart Contracts with Automatic Abstraction Tuning

Smart contracts are programs that manage digital assets according to a certain protocol, expressing for instance the rules of an auction. Understanding the possible behaviors of a smart contract is difficult, which complicates development, auditing, and the post-mortem analysis of attacks. This paper presents the first specification mining technique for smart contracts. Our technique extracts the possible behaviors of smart contracts from contract executions recorded on a blockchain and expresses them as finite automata. A novel dependency analysis allows us to separate independent interactions with a contract. Our technique tunes the abstractions for the automata construction automatically based on configurable metrics, for instance, to maximize readability or precision. We implemented our technique for the Ethereum blockchain and evaluated its usability on several real-world contracts.

cs.SE↗
arXiv2018

Engineering Collaborative Social Science Toolkits. STS Methods and Concepts as Devices for Interdisciplinary Diplomacy

The smartification of industries is marked by the development of cyber-physical systems, interfaces, and intelligent software featuring knowledge models, empirical real-time data, and feedback-loops. This brings up new requirements and challenges for HMI design and industrial labor. Social sciences can contribute to such engineering projects with their perspectives, concepts and knowledge. Hence, we claim that, in addition to following their own intellectual curiosities, the social sciences can and should contribute to such projects in terms of an 'applied' science, helping to foster interdisciplinary collaboration and providing toolkits and devices for what we call 'interdisciplinary diplomacy'. We illustrate the benefits of such an approach, support them with selected examples of our involvement in such an engineering project and propose using methods as diplomatic devices and concepts as social theory plug-ins. The article ends with an outlook and reflection on the remaining issue of whether and in how far such 'applied' and critical social science can or should be integrated.

cs.HC↗
arXiv2018

Scalable Bayesian Nonparametric Clustering and Classification

We develop a scalable multi-step Monte Carlo algorithm for inference under a large class of nonparametric Bayesian models for clustering and classification. Each step is "embarrassingly parallel" and can be implemented using the same Markov chain Monte Carlo sampler. The simplicity and generality of our approach makes inference for a wide range of Bayesian nonparametric mixture models applicable to large datasets. Specifically, we apply the approach to inference under a product partition model with regression on covariates. We show results for inference with two motivating data sets: a large set of electronic health records (EHR) and a bank telemarketing dataset. We find interesting clusters and favorable classification performance relative to other widely used competing classifiers.

stat.CO↗
arXiv2018

Permission Inference for Array Programs

Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this information provide only partial solutions for the important class of array-manipulating programs. In this paper, we present a static analysis that infers the memory footprint of an array program in terms of permission pre- and postconditions as used, for example, in separation logic. This formulation allows our analysis to handle concurrent programs and produces specifications that can be used by verification tools. Our analysis expresses the permissions required by a loop via maximum expressions over the individual loop iterations. These maximum expressions are then solved by a novel maximum elimination algorithm, in the spirit of quantifier elimination. Our approach is sound and is implemented; an evaluation on existing benchmarks for memory safety of array programs demonstrates accurate results, even for programs with complex access patterns and nested loops.

cs.PL↗
arXiv2018

Automating Deductive Verification for Weak-Memory Programs

Writing correct programs for weak memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logics for the verification of such programs have recently been proposed, but their usage has been limited thus far to manual proofs. Automating proofs in these logics via first-order solvers is non-trivial, due to reasoning features such as higher-order assertions, modalities and rich permission resources. In this paper, we provide the first implementation of a weak memory program logic using existing deductive verification tools. We tackle three recent program logics: Relaxed Separation Logic and two forms of Fenced Separation Logic, and show how these can be encoded using the Viper verification infrastructure. In doing so, we illustrate several novel encoding techniques which could be employed for other logics. Our work is implemented, and has been evaluated on examples from existing papers as well as the Facebook open-source Folly library.

cs.PL↗