Martin Avanzini, Michael Schaper, Georg Moser
We are concerned with the average case runtime complexity analysis of a prototypical imperative language endowed with primitives for sampling and probabilistic choice. Taking inspiration from known approaches from to the modular resource analysis of non-probabilistic programs, we investigate how a modular runtime analysis is obtained for probabilistic programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable approaches for program analysis often rely on modularity as their theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule) of Floyd-Hoare logic provides the foundation for modular analysis. Extension of this rule to almost-sure termination of probabilistic programs is quite tricky, and a probabilistic variant was proposed in [Fioriti and Hermanns 2015]. While the proposed probabilistic varia…
Modular Responsiveness Verification of Rust Async Runtimes
针对Rust异步运行时，提出轻量级模块化证明技术，通过静态分析验证任务最终进展的活性属性，并应用于多个运行时关键组件。
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
提出Coneris，首个高阶并发分离逻辑，通过随机逻辑原子性支持并发概率程序的错误概率界模块化推理，并在Rocq和Iris中机械化验证。
Modular Probabilistic Models via Algebraic Effects
针对概率编程语言中模型可重用性和可组合性受限的问题，本文以Haskell为宿主语言，提出一种基于代数效应的嵌入式领域特定语言，使概率模型成为模块化、一等公民且可重用于模拟与推断，并利用代数效应处理器将模拟和推断表达为可组合的程序转换。
Modular probabilistic programming with algebraic effects (MSc Thesis 2019)
本文提出Koka Bayes库，结合代数效应处理与模块化设计，解决概率编程中推理算法的模块化实现问题。
Lightweight, source-to-source transformation approaches to implementing MCMC for probabilistic programming languages are popular for their simplicity, support of existing deterministic code, and ability to execute on existing fast runtimes. However, they are also slow, requiring a complete re-execution of the program on every Metropolis Hastings proposal. We present a new extension to the lightweight approach, C3, which enables efficient, incrementalized re-execution of MH proposals. C3 is based on two core ideas: transforming probabilistic programs into continuation passing style (CPS), and c…
We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our rule is simple in the sense that loop body semantics need to be applied only finitely often in order to verify that the candidates are indeed lower bounds. In particular, it is not necessary to find the limit of a sequence as in many previous rules.
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
本文提出一种适用于复杂通用编程语言中差分隐私实现验证的程序逻辑，支持隐私预算作为分离逻辑资源的推理，可处理隐私过滤器和缓存等常见编程模式，并通过实现验证的差分隐私库展示其通用性和可重用性。
We present a tool-based approach for the runtime analysis of communicating processes grounded on probabilistic binary session types. We synthesise a monitor out of a probabilistic session type where each choice point is decorated by a probability distribution. The monitor observes the execution of a process, infers its probabilistic behaviour and issues warnings when the observed behaviour deviates from the one specified by the probabilistic session type.
We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory -- a quantum algorithm for generating …
Probabilistic programming is a programming paradigm for expressing flexible probabilistic models. Implementations of probabilistic programming languages employ a variety of inference algorithms, where sequential Monte Carlo methods are commonly used. A problem with current state-of-the-art implementations using sequential Monte Carlo inference is the alignment of program synchronization points. We propose a new static analysis approach based on the 0-CFA algorithm for automatically aligning higher-order probabilistic programs. We evaluate the automatic alignment on a phylogenetic model, showin…
An Iris for Expected Cost Analysis
本文提出ExpIris，一个基于Iris的参数化分离逻辑框架，通过期望势能方法支持概率程序的摊还期望成本分析，并兼顾正确性推理，成功验证了快速排序和概率二进制计数器的期望运行时。
A probabilistic program defines a probability measure over its semantic structures. One common goal of probabilistic programming languages (PPLs) is to compute posterior probabilities for arbitrary models and queries, given observed evidence, using a generic inference engine. Most PPL inference engines---even the compiled ones---incur significant runtime interpretation overhead, especially for contingent and open-universe models. This paper describes Swift, a compiler for the BLOG PPL. Swift-generated code incorporates optimizations that eliminate interpretation overhead, maintain dynamic depe…
DeGAS: Gradient-Based Optimization of Probabilistic Programs without Sampling
DeGAS通过可微的高斯近似语义实现无需采样的概率程序优化，提供高效的端到端优化方法，适用于包含连续和离散组件的模型。
We present a thread-modular abstract interpretation(TMAI) technique to verify programs under the release-acquire (RA) memory model for safety property violations. The main contributions of our work are: we capture the execution order of program statements as an abstract domain, and propose a sound upper approximation over this domain to efficiently reason over RA concurrency. The proposed domain is general in its application and captures the ordering relations as a first-class feature in the abstract interpretation theory. In particular, the domain represents a set of sequences of modification…
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。