PV3 ForeSee: Formula Exploitation by Sequence Tree for falsificationgenerates an input that triggers a violation of the user-specified property

Application domain/field

Expected input

Format:

Simulink model

Expected output

Input that triggers the violation of the specification?

Internals

Falsification: Given a desired temporal specification, try to find an input of violation instead of a proof guarantee.

Comments

License: GPL-3.0
Hybrid system

Links

Related papers

Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to in CAV '21 paper: Breach

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.