ABSTRACT. We report ongoing work on a framework that constructs a compact, formally certified surrogate of a large continuous-time Markov chain (CTMC) for transient reachability analysis: it takes a PRISM model as input and returns a small abstract PRISM model whose induced CTMC approximates the concrete one within a user-specified tolerance.The core idea is to lift predicate abstraction from program verification into the continuous-time stochastic setting, where the new semantic challenge is rate aggregation: choosing a single transition rate for a block of concrete states without losing formal guarantees.The presentation focuses on three ideas: a semantically derived rate aggregation theory; an automated, learning-inspired refinement loop; and an explicit output artifact that is reusable, inspectable, and diagnostic.The corresponding full paper is under review at a leading international conference on automated verification, and its core theorems have been machine-checked in the Lean 4 proof assistant.

ABSTRACT. We present an approach that solves a general class of problems that require combinatorial and probabilistic reasoning, for example, synthesizing a policy that satisfies first-order logical constraints in an underlying uncertain environment modeled as a family of MDPs. Our approach is to embed probabilistic model checking as a theory within an SMT solver. This leverages the practical advantages of both tools. We use the resulting tool to find policies that are robust, i.e., they perform well on perturbations of the MDP, and that satisfy additional structural constraints regarding, e.g., their representation or implementation cost. These constraints can be flexibly specified in a first-order theory over a set of MDPs.

ABSTRACT. Stochastic processes give a mathematical representation of the probabilistic changes of a random system over time. Verification techniques use these representations to reason about quantitative behavioural properties, such as termination probabilities and probabilistic safety guarantees. Under the compositional view of probabilistic modelling in which probability is modelled by a monad, stochastic processes have a natural coalgebraic interpretation as coinductively generated stochastic structures. This allows for a structured and succinct expression of both discrete-time and continuous-time stochastic processes in higher-order probabilistic programming languages admitting lazy structures, such as LazyPPL. In this presentation, I will show that omega Qbs, a mixture of quasi-Borel spaces and complete partial orders, supports these higher order constructions of various stochastic processes, such as i.i.d measures, Markov chains, Brownian motion and stochastic differential equations.

ABSTRACT. In the past two decades, significant research and development effort went into the development of verification tools for individual languages, such as C, C++, and Java. Many of the used verification approaches are in fact language-agnostic and it would be beneficial for the technology transfer to allow for using the implementations also for other programming and modeling languages. To address the problem, we propose SV-LIB, an exchange format and intermediate language for software-verification tasks, including programs, specifications, and verification witnesses. SV-LIB is based on well-known concepts from imperative programming languages and uses SMT-LIB to represent expressions and sorts used in the program. This makes it easy to parse and to build into existing infrastructure, since many verification tools are based on SMT solvers already. Furthermore, SV-LIB defines a witness format for both correct and incorrect SV-LIB programs, together with means for specifying witness-validation tasks. This makes it possible both to implement independent witness validators and to reuse some verifiers also as validators for witnesses. If possible It would be great if this talk could occur during the first day of the workshop, i.e, July 24th.

ABSTRACT. Imprecise probability generalizes standard probability theory by replacing a single distribution with a convex set of possible distributions. We show that this generalization requires no change to the standard BDD compilation and weighted model counting pipeline used by discrete probabilistic languages. An imprecise coin flip is simply a BDD variable whose weight is left free rather than fixed. We introduce “Imp", a Haskell embedded DSL for imprecise probabilistic programming. A graded monad, indexed by finite sets of named sources of epistemic uncertainty, restores the commutativity that the standard convex powerset monad lacks, and GHC's type system enforces this at compile time. Weighted model counting is parametric in the semiring, so the same compiled BDD supports exact, differentiable, and interval-bounded inference.

ABSTRACT. Many real-world systems require balancing several conflicting quantitative objectives simultaneously. For instance, randomized retry protocols must trade off reliability against latency and communication overhead, while autonomous robotic systems must balance safety, energy consumption, and task completion time. Such systems are naturally modeled as probabilistic programs, where quantitative reasoning about multiple objectives becomes essential. We present a predicate transformer approach to multiobjective verification for probabilistic programs. Our work combines ideas from weakest preexpectation calculi and multiobjective model checking to compute Pareto fronts (that is, optimal values for several objectives) directly at the program level.

ABSTRACT. Client server systems are one of the largest programming paradigms. Crypto exchanges with an unbounded number of investors, multiplayer games where the number of players are not known apriori and services with an unbounded customer base are instances of unbounded client server systems. We focus on client server systems with single server and unboundedly many clients, where the number of clients are not known apriori and there can be unbounded concurrent interactions between the clients and server. The major challenges are to identify the suitable model to abstract the behaviour of the systems, to identify suitable logics to specify the properties and to identify formal techniques for verifying the properties on the model. In this talk, we discuss the formal modeling, encoding , verification algorithm to exploit concurrency. We also discuss the suite of formal verification tools for client server systems with unbounded clients using classes of nets and various suitable logics to represent their properties.

ABSTRACT. Weakest pre-expectations are the probabilistic program analogue to weakest preconditions in classical programs. Deductive veri!cation approaches aim to establish bounds on these quantitative expectations. Their automation has been successful in analysing a variety of discrete probabilistic programs. Key routines in that automation require reasoning about (partially unrolled) loops, however, the logical representation of weakest pre-expectations on such unrollings often explodes. In this talk, we will present typed extended decision diagrams (TEDDs), inspired by various extensions to binary decision diagrams in classical planning. We demonstrate computing WPs represented as TEDDs, SMT-based pruning to further shrink their representation, and we lift some proof rules for loops to operate on TEDDs. Experimental results demonstrate that TEDDs boost the scalability of deductive probabilistic program veri!cation by orders of magnitudes over the state of the art.