$$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⬇️

scientific article published in 2016

A Greedy Approach for the Efficient Repair of Stochastic Models

article published in 2015

Accelerating Parametric Probabilistic Verification

Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems

scientific article published on 01 August 2011

Behavioral interface description of an object-oriented language with futures and promises

scientific article

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

Counterexamples for Expected Rewards

DTMC Model Checking by SCC Reduction

Hierarchical Counterexamples for Discrete-Time Markov Chains

High-Level Counterexamples for Probabilistic Automata

High-level Counterexamples for Probabilistic Automata

HyperProb: A Model Checker for Probabilistic Hyperproperties

scientific article published in 2021

Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics

scholarly article

Introducing Asynchronicity to Probabilistic Hyperproperties

scientific article published in 2023

Minimal Critical Subsystems for Discrete-Time Markov Models

Minimal counterexamples for linear-time probabilistic verification

Model checking hyperproperties for Markov decision processes

scientific article published in November 2022

Modular strategic SMT solving with SMT-RAT

scholarly article

Optimisation of Concentrating Solar Thermal Power Plants with Neural Networks

article

PROPhESY: A PRObabilistic ParamEter SYnthesis Tool

Parameter Synthesis for Probabilistic Hyperproperties

Probabilistic Hyperproperties with Nondeterminism

scientific article published in 2020

Probabilistic Hyperproperties with Rewards

scientific article published in 2022

Symbolic Counterexample Generation for Discrete-Time Markov Chains

article published in 2013

Symbolic counterexample generation for large discrete-time Markov chains

The COMICS Tool – Computing Minimal Counterexamples for DTMCs