research
∙
09/06/2023
FMplex: A Novel Method for Solving Linear Real Arithmetic Problems (Extended Version)
In this paper we introduce a novel quantifier elimination method for con...
share
research
∙
07/11/2023
Introducing Asynchronicity to Probabilistic Hyperproperties
Probabilistic hyperproperties express probabilistic relations between di...
research
∙
06/29/2023
Exploiting Strict Constraints in the Cylindrical Algebraic Covering
One of the few available complete methods for checking the satisfiabilit...
research
∙
12/19/2022
Levelwise construction of a single cylindrical algebraic cell
Satisfiability Modulo Theories (SMT) solvers check the satisfiability of...
research
∙
07/14/2022
Robot Swarms as Hybrid Systems: Modelling and Verification
A swarm robotic system consists of a team of robots performing cooperati...
research
∙
09/03/2021
On the proof complexity of MCSAT
Satisfiability Modulo Theories (SMT) and SAT solvers are critical compon...
research
∙
08/11/2021
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
We discuss the topic of unsatisfiability proofs in SMT, particularly wit...
research
∙
05/13/2020
Probabilistic Hyperproperties with Nondeterminism
We study the problem of formalizing and checking probabilistic hyperprop...
research
∙
03/12/2020
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
We present a new algorithm for determining the satisfiability of conjunc...
research
∙
06/17/2019
Multiple Analyses, Requirements Once: simplifying testing & verification in automotive model-based development
In industrial model-based development (MBD) frameworks, requirements are...
research
∙
03/16/2019
Parameter Synthesis for Markov Models
Markov chain analysis is a key technique in reliability engineering. A p...
research
∙
06/19/2018
SMarTplan: a Task Planner for Smart Factories
Smart factories are on the verge of becoming the new industrial paradigm...
research
∙
04/05/2018
HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
In this paper, we propose a new logic for expressing and reasoning about...
research
∙
11/12/2017
On the Synthesis of Guaranteed-Quality Plans for Robot Fleets in Logistics Scenarios via Optimization Modulo Theories
In manufacturing, the increasing involvement of autonomous robots in pro...
research
∙
04/08/2017