You are here

Home › Research › Publications ›

Optimizing Trans-Compilers in Runtime Verification Makes Sense – Sometimes

TitleOptimizing Trans-Compilers in Runtime Verification Makes Sense – Sometimes
Publication TypeConference Proceedings
Year of Publication2022
AuthorsKallwies, H, Leucker, M, Prilop, M, Schmitz, M
Conference NameInternational Symposium on Theoretical Aspects of Software Engineering (TASE)
Date Published07/2022
PublisherSpringer International Publishing
Conference LocationCluj-Napoca, Romania
Keywordscompiler optimization, Monitor generation, Runtime verification
AbstractThis paper considers two kinds of optimizations for a specification language compiler for stream-based runtime verification: (i) the manual addition of core functions with dedicated translation schemas and (ii) an improved initialization that simplifies subsequent constant propagation. We employ both optimizations within the open source runtime verification framework TeSSLa, which comes with a trans-compiler as synthesis tool which translates TeSSLa specifications to Scala code eventually running on the JVM. Our evaluation shows that the first optimization improves the efficiency of the resulting monitor significantly while the second gets lost within the variety of optimizations present for the back end systems.
URLhttps://link.springer.com/chapter/10.1007/978-3-031-10363-6_14
DOI10.1007/978-3-031-10363-6_14
Bibtex: 
@proceedings {1412,
	title = {Optimizing Trans-Compilers in Runtime Verification Makes Sense {\textendash} Sometimes},
	year = {2022},
	month = {07/2022},
	publisher = {Springer International Publishing},
	address = {Cluj-Napoca, Romania},
	abstract = {This paper considers two kinds of optimizations for a specification language compiler for stream-based runtime verification: (i) the manual addition of core functions with dedicated translation schemas and (ii) an improved initialization that simplifies subsequent constant propagation. We employ both optimizations within the open source runtime verification framework TeSSLa, which comes with a trans-compiler as synthesis tool which translates TeSSLa specifications to Scala code eventually running on the JVM. Our evaluation shows that the first optimization improves the efficiency of the resulting monitor significantly while the second gets lost within the variety of optimizations present for the back end systems.
},
	keywords = {compiler optimization, Monitor generation, Runtime verification},
	doi = {10.1007/978-3-031-10363-6_14},
	url = {https://link.springer.com/chapter/10.1007/978-3-031-10363-6_14},
	author = {Hannes Kallwies and Martin Leucker and Meiko Prilop and Malte Schmitz}
}