Philipp Wendler

We need to find a place in the UI for this, because now the filters are configured in a column-specific manner, and the proposed kind of filters would be global....

For the record: Since the introduction of the filter sidebar, there is an obvious way where to add the UI for this: On the very top of the filter side...

The [Execution-Time Measurement Protocol](http://raptor.cs.arizona.edu/~rts/pubs/spe16.pdf) is an approach that makes use of multiple executions of the same command for increasing the measurement precision.

I think I found a third solution: We can create a temporary output file in memory with [memfd_create](http://man7.org/linux/man-pages/man2/memfd_create.2.html). I did not try this out yet, but it should behave as...

Cgroups seem to support getting notifications at arbitrary memory thresholds even before the actual memory limit is reached: https://www.kernel.org/doc/Documentation/cgroups/memory.txt, Section "9. Memory thresholds". This can simplify implementing this feature.

> 2. Set correspondence between witness file and violated property with > status=unsafe. > > For items 2 and 3 it seems that we have a solution. For item 2...

>> Currently, BenchExec itself does not know about witness files, only Dirk's additional scripts for witness validation do. Of course these scripts need to be updated, but I can't say...

>> How do we support cases where other properties not based on reachability of an error function are also present? Or don't we need to support them? > > To...

Best would be if you could create a pull request that contains everything for this feature: code, documentation, etc. Then I would be glad to review it.

I added my comments to the pull request. For question 1, I am not sure. It depends a lot on what is represented in the main status in case of...