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

Links

Artifact for CAV '21 paper: https://github.com/choshina/ForeSee

Last commit date

30 May 2021

Related papers

https://doi.org/10.1007/978-3-030-81685-8_29 (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to in CAV '21 paper: Breach

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.