Formal methods typically attempt to prove that the worst-case behavior of a system is correct. Their main use is to show the absence of synchronization bugs in a concurrent system consisting of many interacting processes. While trying to adapt these methods to systems performance (cost, timing, power) one needs sometimes to move from worst-case to average-case reasoning, to provide numerical rather than Boolean answer and to relax the coverage of all possible behavior toward random sampling. This informal workshop brings together researchers interested in these issues and their algorithmic implications.
The workshop will be held in May 2nd in Marrakech, co-located with the NETYS conference. The workshop is open to NETYS participants.