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

artículo científico publicado en 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

artículo científico publicado en 2011

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

artículo científico publicado en 2009

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

artículo científico publicado en 2021

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

scholarly article

Introducing Asynchronicity to Probabilistic Hyperproperties

artículo científico publicado en 2023

Minimal Critical Subsystems for Discrete-Time Markov Models

Minimal counterexamples for linear-time probabilistic verification

Model checking hyperproperties for Markov decision processes

artículo científico publicado en 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

artículo científico publicado en 2020

Probabilistic Hyperproperties with Rewards

artículo científico publicado en 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