# Tool

news

## The 2022 prize of ARCH-COMP was awarded to PSY-TaLiRo.

The 2022 prize of ARCH-COMP was awarded to PSY-TaLiRo. The jury, consisting of group leaders and workshop participants, appreciated the technical achievements embodied in PSY-TaLiRo and furthermore recognised the long and continuous stream of contributions that the team has made to the community. The award comes with a 500 USD prize.

news

## ARCH 2021 Best Result Award

The ARCH 2021 Best Result Award goes to Katherine Cordwell, Aditi Kabra, Jonathan Laurent, Stefan Mitsch, Andre Platzer, William Simmons, Yong Kiam Tan, and Noah Abou El Wafa (in alphabetical order) for their verification tool KeYmaera X. The award comes with a 500 Euro prize. Congratulations!
news

## ARCH 2020 Best Result Award

The ARCH 2020 Best Result Award goes to Luis Benet, Marcelo Forets, Daniel Freire, David P. Sanders, and Christian Schilling (in alphabetical order) for their verification tool JuliaReach. The award comes with a 500 Euro prize. Congratulations!

news

## ARCH 2019 Best Result Award

The ARCH 2019 Best Result Award goes to Fabian Immler for his verification tool Isabelle/HOL-ODE-Numerics. The award comes with a 650 Euro prize sponsored by Bosch. Since Fabian couldn't be at the ceremony, Matthias Althoff accepted the certificate on his behalf, from Arne Hamann of Bosch.

news

## ARCH 2018 Best Friendly Competition Result

It is our pleasure to announce that Marcelo Forets and Christian Schilling receive the ARCH 2018 Best Friendly Competition Result. They develop the tool JuliaReach, which showed significant improvements for computing reachable sets of linear continuous systems. The award comes with a 500 Euro prize from Bosch. Goran Frehse received the prize from Thomas Heinz of Bosch on their behalf.

forum

## finite-time reachability of a class of discrete-time PWA systems over a class of polyhedra

The problem is as follows. Given a model, a set of initial conditions X(0) and a time horizon N, we want to compute the states reachable at time 1, 2, ..., N. In other words, we want to determine X(1), X(2), ..., X(N).

The model is a class of discrete-time PWA systems:

x(k+1) = A_i x(k) + b_i, if x(k) \in R_i where i \in {1,...,M}

For each i \in {1,...,M}, there is a single element in each row of matrix A_i with the value of 1 and the others are 0.

news