A Deductive Verification Infrastructure for Probabilistic Programs

scientific article published on 16 October 2023

A Greedy Approach for the Efficient Repair of Stochastic Models

article published in 2015

A Model Checker for AADL

artículo científico publicado en 2010

A Semantics for Every GSPN

article published in 2013

A Statistical Approach for Timed Reachability in AADL Models

A compositional modelling and analysis framework for stochastic hybrid systems

article

A design model for open distributed processing systems

A linear process-algebraic format with data for probabilistic automata

artículo científico publicado en 2012

A theory of Stochastic systems. Part II: Process algebra

scholarly article by Pedro R. D’Argenio & Joost-Pieter Katoen published November 2005 in Information and Computation

A theory of stochastic systems part I: Stochastic automata

article published in 2005

A tool for model-checking Markov chains

article published in 2003

Abstract Probabilistic Automata

Abstract Probabilistic Automata

Abstraction for Stochastic Systems by Erlang’s Method of Stages

Accelerating Parametric Probabilistic Verification

Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates

Analysing and Improving Energy Efficiency of Distributed Slotted Aloha

article

Analysis of Timed and Long-Run Objectives for Markov Automata ⬇️

Analyzing Energy Consumption in a Gossiping MAC Protocol

article published in 2010

Approximate Model Checking of Stochastic Hybrid Systems

article

Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability

Automated Termination Analysis of Polynomial Probabilistic Programs

artículo científico publicado en 2021

Automated compositional Markov chain generation for a plain-old telephone system

article

Bisimulation and Simulation Relations for Markov Chains

Causal ambiguity and partial orders in event structures

Codesign of dependable systems: A component-based modeling language

artículo científico publicado en 2009

Comparative branching-time semantics for Markov chains

Compositional Abstraction Techniques for Probabilistic Automata

article

Compositional Analysis Using Component-Oriented Interpolation

article

Conditioning in Probabilistic Programming

Confluence reduction for Markov automata

Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey

Counterexamples for Expected Rewards

DTMC Model Checking by SCC Reduction

Delayed Nondeterminism in Continuous-Time Markov Decision Processes

article

Efficient CTMC Model Checking of Linear Real-Time Objectives

article

Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components

Efficient Modelling and Generation of Markov Automata

artículo científico publicado en 2012

Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions

artículo científico publicado en 2024

Exponentially timed SADF

Fault Trees on a Diet

article by Sebastian Junges et al published 2015 in Lecture Notes in Computer Science

Formal correctness, safety, dependability, and performance analysis of a satellite

GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components

GSPNs Revisited: Simple Semantics and New Analysis Algorithms

scholarly article published June 2012

Generative Datalog with Continuous Distributions

artículo científico publicado en 2022

Guest editors’ introduction: Advancements and extensions of verification techniques

Guest editors’ introduction: Model checking in a nutshell

article

Guest editors’ introduction: quantitative analysis of real-time embedded systems

Hierarchical Counterexamples for Discrete-Time Markov Chains

High-Level Counterexamples for Probabilistic Automata

High-level Counterexamples for Probabilistic Automata

How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison

Inferring Covariances for Probabilistic Programs

article published in 2016

Juggrnaut: using graph grammars for abstracting unbounded heap structures

LTL Model Checking of Time-Inhomogeneous Markov Chains

Layered Reduction for Abstract Probabilistic Automata

Layered Reduction for Modal Specification Theories

Layered reasoning for randomized distributed algorithms

scholarly article by Mani Swaminathan et al published 29 June 2012 in Formal Aspects of Computing

Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption

Learning Communicating Automata from MSCs

Let this Graph Be Your Witness!

Linear-Invariant Generation for Probabilistic Programs:

Lower Bounds for Possibly Divergent Probabilistic Programs

artículo científico publicado en 2023

Maximizing system lifetime by battery scheduling

Metric semantics for true concurrent real time

article by Joost-Pieter Katoen et al published March 2001 in Theoretical Computer Science

Minimal Critical Subsystems for Discrete-Time Markov Models

Minimal counterexamples for linear-time probabilistic verification

Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains

Model Checking Markov Chains Using Krylov Subspace Methods: An Experience Report

Model Checking of Open Interval Markov Chains

Model Checking: One Can Do Much More Than You Think!

article

Model checking mobile stochastic logic

Model-checking large structured Markov chains

article

Modelling and statistical model checking of a microgrid

Modelling, Reduction and Analysis of Markov Automata

Monitoring CTMCs by Multi-clock Timed Automata

Multi-cost Bounded Reachability in MDP

Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems

New Results on Abstract Probabilistic Automata

Observing Continuous-Time MDPs by 1-Clock Timed Automata

On Generative Parallel Composition1 1Supported by the NWO/SION project 612-33-006 and the System Validation Centre/CTIT

article

On a Temporal Logic for Object-Based Systems

On the Hardness of Almost–Sure Termination

article

On the hardness of analyzing probabilistic programs

Operational Versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language

Operational versus weakest pre-expectation semantics for the probabilistic guarded command language

PROPhESY: A PRObabilistic ParamEter SYnthesis Tool

Parametric LTL on Markov Chains

Performability assessment by model checking of Markov reward models

article

Performance Analysis of Computing Servers — A Case Study Exploiting a New GSPN Semantics

Performance evaluation and model checking join forces

article

Perspectives in Probabilistic Verification

Prinsys—On a Quest for Probabilistic Loop Invariants

Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow

article

Probabilistic Programming: A True Verification Challenge

article by Joost-Pieter Katoen published 2015 in Lecture Notes in Computer Science

Probabilistic weak simulation is decidable in polynomial time

Probably safe or live

scholarly article published 2014

Process algebra for performance evaluation

scholarly article by Holger Hermanns et al published March 2002 in Theoretical Computer Science

Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs

scientific article published on 05 January 2024

Quantitative Evaluation in Embedded System Design: Trends in Modeling and Analysis Techniques

Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

article

Quantitative Modelling and Analysis

Quantitative Timed Analysis of Interactive Markov Chains

Quantitative automata model checking of autonomous stochastic hybrid systems

article

Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems

Reachability probabilities in Markovian Timed Automata

Regular Expressions for PCTL Counterexamples

article published in 2008

Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning

artículo científico publicado en 2021

Robust PCTL model checking

article

SMA—The Smyle Modeling Approach

SMT-Based Bisimulation Minimisation of Markov Models

Safety-Constrained Reinforcement Learning for MDPs

scholarly article by Sebastian Junges et al published 2016 in Lecture Notes in Computer Science

Scenario-Based Verification of Uncertain MDPs

scientific article published on 17 April 2020

Simulation-Based CTMC Model Checking: An Empirical Evaluation

Smyle: A Tool for Synthesizing Distributed Models from Scenarios by Learning

Sound Value Iteration

Spacecraft early design validation using formal methods

artículo científico publicado en 2014

Symbolic Counterexample Generation for Discrete-Time Markov Chains

article published in 2013

Symbolic counterexample generation for large discrete-time Markov chains

Symmetry reduction for stochastic hybrid systems

Systolic arrays for the recognition of permutation-invariant segments

The COMICS Tool – Computing Minimal Counterexamples for DTMCs

The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems

artículo científico publicado en 2009

The How and Why of Interactive Markov Chains

The Ins and Outs of the Probabilistic Model Checker MRMC

article

The Probabilistic Termination Tool Amber

artículo científico publicado en 2021

The Surprising Robustness of (Closed) Timed Automata against Clock-Drift

The ins and outs of the probabilistic model checker MRMC

article

The probabilistic termination tool amber

artículo científico publicado en 2022

Three-valued abstraction for probabilistic systems

Tight Game Abstractions of Probabilistic Automata

Time-Abstracting Bisimulation for Probabilistic Timed Automata

Time-Bounded Reachability in Tree-Structured QBDs by Abstraction

Time-bounded reachability in tree-structured QBDs by abstraction

Towards Trustworthy Aerospace Systems: An Experience Report

Towards a Logic for Performance and Mobility

article

Understanding Probabilistic Programs

Verification and performance evaluation of aadl models

artículo científico publicado en 2009

Verifying pointer programs using graph grammars

Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs

Weighted Lumpability on Markov Chains

Weighted programming: a programming paradigm for specifying mathematical models

artículo científico publicado en 2022

YMCA

2006 article in Electronic Notes in Theoretical Computer Science

Zero-reachability in probabilistic multi-counter automata

libalf: The Automata Learning Framework