Bubaak: Runtime monitoring of program verifiers

Chalupa, Marek; Henzinger, Thomas A

Bubaak: Runtime monitoring of program verifiers

Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 535–540.

Download

2023_LNCS_Chalupa.pdf 16.10 MB [Published Version]

DOI

10.1007/978-3-031-30820-8_32

Conference Paper | Published | English

Author

Chalupa, Marek^ISTA; Henzinger, Thomas A^ISTA

Department

Henzinger_Thomas Group

Grant

Vigilant Algorithmic Monitoring of Software

Series Title

LNCS

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.

Publishing Year

2023

Date Published

2023-04-20

Proceedings Title

Tools and Algorithms for the Construction and Analysis of Systems

Publisher

Springer Nature

Acknowledgement

This work was supported by the ERC-2020-AdG 10102009 grant.

Volume

13994

Page

535-540

Conference

TACAS: Tools and Algorithms for the Construction and Analysis of Systems

Conference Location

Paris, France

Conference Date

2023-04-22 – 2023-04-27

ISBN

9783031308192

ISSN

0302-9743

eISSN

1611-3349

IST-REx-ID

12854

Cite this

Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers. In: Tools and Algorithms for the Construction and Analysis of Systems. Vol 13994. Springer Nature; 2023:535-540. doi:10.1007/978-3-031-30820-8_32

Chalupa, M., & Henzinger, T. A. (2023). Bubaak: Runtime monitoring of program verifiers. In Tools and Algorithms for the Construction and Analysis of Systems (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. https://doi.org/10.1007/978-3-031-30820-8_32

Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” In Tools and Algorithms for the Construction and Analysis of Systems, 13994:535–40. Springer Nature, 2023. https://doi.org/10.1007/978-3-031-30820-8_32.

M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,” in Tools and Algorithms for the Construction and Analysis of Systems, Paris, France, 2023, vol. 13994, pp. 535–540.

Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” Tools and Algorithms for the Construction and Analysis of Systems, vol. 13994, Springer Nature, 2023, pp. 535–40, doi:10.1007/978-3-031-30820-8_32.

All files available under the following license(s):

Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):