Bubaak: Runtime Monitoring of Program Verifiers: (Competition Contribution)
M Chalupa, TA Henzinger - … Conference on Tools and Algorithms for the …, 2023 - Springer
International Conference on Tools and Algorithms for the Construction and …, 2023•Springer
The main idea behind Bubaak is to run multiple program analyses in parallel and use
runtime monitoring and enforcement to observe and control their progress in real time. The
analyses send information about (un) explored states of the program and discovered
invariants to a monitor. The monitor processes the received data and can force an analysis
to stop the search of certain program parts (which have already been analyzed by other
analyses), or to make it utilize a program invariant found by another analysis. At sv-comp …
runtime monitoring and enforcement to observe and control their progress in real time. The
analyses send information about (un) explored states of the program and discovered
invariants to a monitor. The monitor processes the received data and can force an analysis
to stop the search of certain program parts (which have already been analyzed by other
analyses), or to make it utilize a program invariant found by another analysis. At sv-comp …
Abstract
The main idea behind Bubaak is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis.
At SV-COMP 2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why Bubaak only ran several analyses in parallel, without any coordination. Still, Bubaak won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition.
Springer