scholarly journals ARCH-COMP18 Category Report: Stochastic Modelling

10.29007/7ks7 ◽  
2018 ◽  
Author(s):  
Alessandro Abate ◽  
Henk Blom ◽  
Nathalie Cauchi ◽  
Sofie Haesaert ◽  
Arnd Hartmanns ◽  
...  
Keyword(s):  
Formal Verification ◽  
Stochastic Modelling ◽  
Benchmark Problems ◽  
Alphabetical Order ◽  
Current State ◽  
Push Forward ◽  
Mc Simulation ◽  
Different Levels ◽  
Friendly Competition ◽  
Future Plans

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In this first edition, we present five benchmarks with different levels of complexities and stochastic flavours. We make use of six different tools and frameworks (in alphabetical order): Barrier Certificates, FAUST2, FIRM-GDTL, Modest, SDCPN modelling & MC simulation and SReachTools; and attempt to solve instances of the five different benchmark problems. Through these benchmarks, we capture a snapshot on the current state-of the art tools and frameworks within the stochastic modelling domain. We also present the challenges encountered within this domain and highlight future plans which will push forward the development of more tools and methodologies for performing formal verification and optimal policy synthesis of stochastic processes.

scholarly journals ARCH-COMP18 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics

10.29007/73mb ◽  
2018 ◽  
Author(s):  
Matthias Althoff ◽  
Stanley Bak ◽  
Xin Chen ◽  
Chuchu Fan ◽  
Marcelo Forets ◽  
...  
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Safety Verification ◽  
Alphabetical Order ◽  
Friendly Competition

This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In its second edition, 9 tools have been applied to solve six different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA, CORA/SX, C2E2, Flow*, HyDRA, Hylaa, Hylaa-Continuous, JuliaReach, SpaceEx, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.

scholarly journals ARCH-COMP17 Category Report: Bounded Model Checking of Hybrid Systems with Piecewise Constant Dynamics

10.29007/rvk6 ◽  
2018 ◽  
Author(s):  
Lei Bu ◽  
Rajarshi Ray ◽  
Stefan Schupp
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Hybrid Systems ◽  
Bounded Model Checking ◽  
Benchmark Problems ◽  
Future Event ◽  
Alphabetical Order ◽  
Piecewise Constant ◽  
The Future ◽  
Friendly Competition

This report presents results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, three tools have been applied to solve three different benchmark problems in the category ofbounded model checking of hybrid systems with piecewise constant dynamics (in alphabetical order): BACH, HyDRA, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools and we also welcome more tools to join in this friendly competition in the future event.

scholarly journals ARCH-COMP19 Category Report: Bounded Model Checking of Hybrid Systems with Piecewise Constant Dynamics

10.29007/g965 ◽  
2019 ◽  
Author(s):  
Lei Bu ◽  
Rajarshi Ray ◽  
Stefan Schupp
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Hybrid Systems ◽  
Bounded Model Checking ◽  
Optimization Techniques ◽  
Benchmark Problems ◽  
Future Event ◽  
Alphabetical Order ◽  
Piecewise Constant ◽  
Friendly Competition

This report presents results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In its third edition, three tools have been applied to solve three different benchmark problems in the category ofbounded model checking of hybrid systems with piecewise constant dynamics (in alphabetical order): BACH, HyDRA, and XSpeed. Compare to last year, HyDRA is equipped with new optimization techniques and the performance is improved accordingly. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools and we also welcome more tools to join in this friendly competition in the future event.

scholarly journals ARCH-COMP18 Category Report: Bounded Model Checking of Hybrid Systems with Piecewise Constant Dynamics

10.29007/q5tq ◽  
2018 ◽  
Author(s):  
Lei Bu ◽  
Rajarshi Ray ◽  
Stefan Schupp
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Hybrid Systems ◽  
Bounded Model Checking ◽  
Benchmark Problems ◽  
Future Event ◽  
Alphabetical Order ◽  
Piecewise Constant ◽  
The Future ◽  
Friendly Competition

This report presents results of a friendly competition for formal verification of contin- uous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In its second edition, three tools have been applied to solve three differ- ent benchmark problems in the category ofbounded model checking of hybrid systems with piecewise constant dynamics (in alphabetical order): BACH, HyDRA, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools and we also welcome more tools to join in this friendly competition in the future event.

scholarly journals ARCH-COMP17 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics

10.29007/4dcn ◽  
2018 ◽  
Author(s):  
Matthias Althoff ◽  
Stanley Bak ◽  
Dario Cattaruzza ◽  
Xin Chen ◽  
Goran Frehse ◽  
...  
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Safety Verification ◽  
Alphabetical Order ◽  
Friendly Competition

This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, seven tools have been applied to solve three different benchmark problems in the category for linear continuous dynamics (in alphabetical order): Axelerator, CORA, Flow*, HyDRA, Hylaa, SpaceEx, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.

scholarly journals ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics

10.29007/bj1w ◽  
2019 ◽  
Author(s):  
Matthias Althoff ◽  
Stanley Bak ◽  
Marcelo Forets ◽  
Goran Frehse ◽  
Niklas Kochdumper ◽  
...  
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Safety Verification ◽  
Alphabetical Order ◽  
Friendly Competition

This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In its third edition, seven tools have been applied to solve six different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA, CORA/SX, HyDRA, Hylaa, JuliaReach, SpaceEx, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results provide one of the most complete assessments of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.

scholarly journals ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics

10.29007/7dt2 ◽  
2020 ◽  
Author(s):  
Matthias Althoff ◽  
Stanley Bak ◽  
Zongnan Bao ◽  
Marcelo Forets ◽  
Goran Frehse ◽  
...  
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Fourth Edition ◽  
Safety Verification ◽  
Alphabetical Order ◽  
Friendly Competition

We present the results of the ARCH1 2020 friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. In its fourth edition, eight tools have been applied to solve eight different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA, C2E2, HyDRA, Hylaa, Hylaa-Continuous, JuliaReach, SpaceEx, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results provide one of the most complete assessments of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.

scholarly journals ARCH-COMP17 Repeatability Evaluation Report

10.29007/7hvk ◽  
2018 ◽  
Author(s):  
Taylor T. Johnson
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Safety Verification ◽  
Evaluation Report ◽  
Standard Practice ◽  
Friendly Competition

This report presents the results of the repeatability evaluation for a friendly competition for formal verification of continuous and hybrid systems. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, thirteen tools have been applied to solve benchmark problems for the six competition categories, of which, ten tools were evaluated and passed the repeatability evaluation. The repeatability results represent a snapshot of the current landscape of tools and the types of benchmarks for which they are particularly suited and for which others may repeat their analyses. Due to the diversity of problems in verification of continuous and hybrid systems, as well as basing on standard practice in repeatability evaluations, we evaluate the tools with pass and/or failing being repeatable. These re- sults probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems up to this date.

scholarly journals ARCH-COMP18 Category Report: Hybrid Systems with Piecewise Constant Dynamics

10.29007/p11g ◽  
2018 ◽  
Author(s):  
Goran Frehse ◽  
Alessandro Abate ◽  
Dieky Adzkiya ◽  
Lei Bu ◽  
Mirco Giacobbe ◽  
...  
Keyword(s):  
Formal Verification ◽  
Hybrid Systems ◽  
Benchmark Problems ◽  
Safety Verification ◽  
Railway Network ◽  
Piecewise Constant ◽  
Friendly Competition

This report presents results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In this second edition, five tools have been applied to solve five different benchmark problems in the category for piecewise constant dynamics: BACH, Lyse, PHAVer, PHAVer-lite, and VeriSiMPL. Compared to last year, a new tool has participated (PHAVer-lite) and a benchmark has been made more complex (Dutch Railway Network). The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with piecewise constant dynamics up to this date.

scholarly journals ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics

10.29007/zkf6 ◽  
2020 ◽  
Author(s):  
Luca Geretti ◽  
Julien Alexandre Dit Sandretto ◽  
Matthias Althoff ◽  
Luis Benet ◽  
Alexandre Chapoutot ◽  
...  
Keyword(s):  
Nonlinear Dynamics ◽  
Formal Verification ◽  
Hybrid Systems ◽  
Reachability Analysis ◽  
Current Status ◽  
Benchmark Problems ◽  
Hybrid Dynamics ◽  
Friendly Competition

We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. These tools are applied to solve reachability analysis problems on six benchmark problems, two of them featuring hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.

Sign in / Sign up

Export Citation Format

Share Document