{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T03:01:15Z","timestamp":1791342075288,"version":"4.3.1"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986819","type":"print"},{"value":"9783031986826","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Stream-based runtime monitors are safety assurance tools that check at runtime whether the system\u2019s behavior satisfies a formal specification. Specifications consist of stream equations, which relate input streams, containing sensor readings and other incoming information, to output streams, representing filtered and aggregated data. This paper presents a framework for the stream-based specification language RTLola. We introduce a new intermediate representation for stream-based languages, the StreamIR, which, like the specification language, operates on streams of unbounded length; while the stream equations are replaced by imperative programs. We present a set of optimizations based on static analysis of the specification and have implemented an interpreter and a compiler for several target languages. In our evaluation, we measure the performance of several real-world case studies. The results show that the new StreamIR framework reduces the runtime significantly compared to the existing RTLola interpreter. We evaluate the effect of the optimizations and show that significant performance gains are possible beyond the optimizations of the target language\u2019s compiler. While our current implementation is limited to RTLola, the StreamIR is designed to accommodate other stream-based languages, enabling their interpretation and compilation into all available target languages.<\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_20","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:14:51Z","timestamp":1753154091000},"page":"393-407","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["An Intermediate Program Representation for\u00a0Optimizing Stream-Based Languages"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8891-7483","authenticated-orcid":false,"given":"Jan","family":"Baumeister","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2307-2296","authenticated-orcid":false,"given":"Arthur","family":"Correnson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-8115-0359","authenticated-orcid":false,"given":"Frederik","family":"Scheerer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"20_CR1","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-981-13-9942-8_32","volume-title":"Advances in Computing and Data Sciences","author":"M Abraham","year":"2019","unstructured":"Abraham, M., Jevitha, K.P.: Runtime verification and vulnerability testing of smart contracts. In: Singh, M., Gupta, P.K., Tyagi, V., Flusser, J., \u00d6ren, T., Kashyap, R. (eds.) ICACDS 2019. CCIS, vol. 1046, pp. 333\u2013342. Springer, Singapore (2019). https:\/\/doi.org\/10.1007\/978-981-13-9942-8_32"},{"key":"20_CR2","unstructured":"Angwin, J., Larson, J., Mattu, S., Kirchner, L.: Machine bias. there\u2019s software used across the country to predict future criminals. and it\u2019s biased against blacks. ProPublica (2016). https:\/\/www.propublica.org\/article\/machine-bias-risk-assessments-in-criminal-sentencing"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-030-03769-7_8","volume-title":"Runtime Verification","author":"S Azzopardi","year":"2018","unstructured":"Azzopardi, S., Ellul, J., Pace, G.J.: Monitoring smart contracts: ContractLarva and open challenges beyond. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 113\u2013137. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_8"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Baumeister, J., Correnson, A., Finkbeiner, B., Scheerer, F.: An intermediate program representation for optimizing stream-based languages (2025). https:\/\/arxiv.org\/abs\/2504.21458","DOI":"10.1007\/978-3-031-98682-6_20"},{"key":"20_CR5","doi-asserted-by":"publisher","unstructured":"Baumeister, J., et al.: Monitoring unmanned aircraft: specification, integration, and lessons-learned. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, 24\u201327 July 2024, Proceedings, Part II. Lecture Notes in Computer Science, vol. 14682, pp. 207\u2013218. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_10","DOI":"10.1007\/978-3-031-65630-9_10"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Baumeister, J., Finkbeiner, B., Kohn, F., Scheerer, F.: A tutorial on stream-based monitoring. In: International Symposium on Formal Methods, pp. 624\u2013648. Springer (2024)","DOI":"10.1007\/978-3-031-71177-0_33"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-030-60508-7_25","volume-title":"Runtime Verification","author":"J Baumeister","year":"2020","unstructured":"Baumeister, J., Finkbeiner, B., Kruse, M., Schwenger, M.: Automatic optimizations for stream-based monitoring languages. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 451\u2013461. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_25"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Baumeister, J., Finkbeiner, B., Scheerer, F., Siber, J., Wagenpfeil, T.: Stream-based monitoring of algorithmic fairness. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 60\u201381. Springer, Cham (2025)","DOI":"10.1007\/978-3-031-90643-5_4"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-030-53291-8_3","volume-title":"Computer Aided Verification","author":"J Baumeister","year":"2020","unstructured":"Baumeister, J., Finkbeiner, B., Schirmer, S., Schwenger, M., Torens, C.: RTLola cleared for take-off: monitoring autonomous aircraft. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 28\u201339. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_3"},{"issue":"5s","key":"20_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358220","volume":"18","author":"J Baumeister","year":"2019","unstructured":"Baumeister, J., Finkbeiner, B., Schwenger, M., Torfah, H.: FPGA stream-monitoring of real-time properties. ACM Trans. Embed. Comput. Syst. (TECS) 18(5s), 1\u201324 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-030-72013-1_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Biewer","year":"2021","unstructured":"Biewer, S., Finkbeiner, B., Hermanns, H., K\u00f6hl, M.A., Schnitzer, Y., Schwenger, M.: RTLola on board: testing real driving emissions on your phone. In: Groote, J.F., Larsen, K.G. (eds.) TACAS 2021. LNCS, vol. 12652, pp. 365\u2013372. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_20"},{"issue":"9","key":"20_CR12","doi-asserted-by":"publisher","first-page":"1293","DOI":"10.1109\/5.97299","volume":"79","author":"F Boussinot","year":"1991","unstructured":"Boussinot, F., De Simone, R.: The esterel language. Proc. IEEE 79(9), 1293\u20131304 (1991)","journal-title":"Proc. IEEE"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-030-03044-5_10","volume-title":"Formal Methods: Foundations and Applications","author":"L Convent","year":"2018","unstructured":"Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: TeSSLa: temporal stream-based specification language. In: Massoni, T., Mousavi, M.R. (eds.) SBMF 2018. LNCS, vol. 11254, pp. 144\u2013162. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03044-5_10"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"d\u2019Angelo, B., et al.: Lola: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166\u2013174. IEEE (2005)","DOI":"10.1109\/TIME.2005.26"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-319-46982-9_10","volume-title":"Runtime Verification","author":"P Faymonville","year":"2016","unstructured":"Faymonville, P., Finkbeiner, B., Schirmer, S., Torfah, H.: A stream-based specification language for network monitoring. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 152\u2013168. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_10"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-030-25540-4_24","volume-title":"Computer Aided Verification","author":"P Faymonville","year":"2019","unstructured":"Faymonville, P., et al.: StreamLAB: stream-based monitoring of cyber-physical systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 421\u2013431. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_24"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Hofmann, J., Kohn, F., Passing, N.: Reactive synthesis of smart contract control flows. In: International Symposium on Automated Technology for Verification and Analysis, pp. 248\u2013269. Springer (2023)","DOI":"10.1007\/978-3-031-45329-8_12"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-030-60508-7_24","volume-title":"Runtime Verification","author":"B Finkbeiner","year":"2020","unstructured":"Finkbeiner, B., Oswald, S., Passing, N., Schwenger, M.: Verified rust monitors for lola specifications. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 431\u2013450. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_24"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Gautier, T., Le\u00a0Guernic, P., Besnard, L.: Signal: A Declarative Language for Synchronous Programming of Real-Time Systems. Springer (1987)","DOI":"10.1007\/3-540-18317-5_15"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-030-03769-7_16","volume-title":"Runtime Verification","author":"F Gorostiaga","year":"2018","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: Striver: stream runtime verification for real-time event-streams. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 282\u2013298. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_16"},{"issue":"9","key":"20_CR21","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language lustre. Proc. IEEE 79(9), 1305\u20131320 (1991)","journal-title":"Proc. IEEE"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Karimi, M., Kueffner, K., Mallik, K.: Monitoring algorithmic fairness. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 358\u2013382. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-37703-7_17"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/978-3-030-81688-9_26","volume-title":"Computer Aided Verification","author":"S Junges","year":"2021","unstructured":"Junges, S., Torfah, H., Seshia, S.A.: Runtime monitors for Markov decision processes. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12760, pp. 553\u2013576. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_26"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Kallwies, H., Leucker, M., Prilop, M., Schmitz, M.: Optimizing trans-compilers in runtime verification makes sense\u2013sometimes. In: International Symposium on Theoretical Aspects of Software Engineering, pp. 197\u2013204. Springer (2022)","DOI":"10.1007\/978-3-031-10363-6_14"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Kallwies, H., Leucker, M., Schmitz, M., Schulz, A., Thoma, D., Weiss, A.: Tessla\u2013an ecosystem for runtime verification. In: International Conference on Runtime Verification, pp. 314\u2013324. Springer (2022)","DOI":"10.1007\/978-3-031-17196-3_20"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-662-58387-6_28","volume-title":"Financial Cryptography and Data Security","author":"A Mavridou","year":"2018","unstructured":"Mavridou, A., Laszka, A.: Designing secure ethereum smart contracts: a finite state machine based approach. In: Meiklejohn, S., Sako, K. (eds.) FC 2018. LNCS, vol. 10957, pp. 523\u2013540. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-58387-6_28"},{"key":"20_CR27","unstructured":"Northpoint Inc. d\/b\/a equivant: Practitioner\u2019s guide to compas core (2015). https:\/\/archive.epic.org\/algorithmic-transparency\/crim-justice\/EPIC-16-06-23-WI-FOIA-201600805-COMPASPractionerGuide.pdf. Accessed 30 Jan 2025"},{"key":"20_CR28","unstructured":"Perez, I., Dedden, F., Goodloe, A.: Copilot 3. Technical report (2020). https:\/\/ntrs.nasa.gov\/citations\/20200003164"},{"key":"20_CR29","doi-asserted-by":"publisher","unstructured":"Perez, I., Goodloe, A.E., Dedden, F.: Runtime verification in real-time with the copilot language: a tutorial. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, 9\u201313 September 2024, Proceedings, Part II. Lecture Notes in Computer Science, vol. 14934, pp. 469\u2013491. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_27","DOI":"10.1007\/978-3-031-71177-0_27"},{"key":"20_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-16612-9_26","volume-title":"Runtime Verification","author":"L Pike","year":"2010","unstructured":"Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 345\u2013359. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_26"},{"key":"20_CR31","unstructured":"Program the Blockchain: Coin funding reference contract (2022). https:\/\/programtheblockchain.com\/posts\/2018\/01\/19\/writing-a-crowdfunding-contract-a-la-kickstarter\/. Accessed 30 Jan 2025"},{"key":"20_CR32","unstructured":"Scheerer, F.: Monitoring smart contracts with rtlola. Bachelor\u2019s thesis, Saarland University (2021)"},{"key":"20_CR33","unstructured":"Sudi, A.: Voting reference contract (2021). https:\/\/github.com\/andresudi\/Voting-Smart-Contract\/blob\/master\/Voting.sol. Accessed 30 Jan 2025"},{"key":"20_CR34","unstructured":"The Solidity Authors: Simple auction reference contract. https:\/\/docs.soliditylang.org\/en\/latest\/solidity-by-example.html#simple-open-auction. Accessed 30 Jan 2025"},{"key":"20_CR35","unstructured":"Vogelsteller, F., Buterin, V.: ERC-20: Token standard (2015). https:\/\/eips.ethereum.org\/EIPS\/eip-20. Accessed 30 Jan 2025"},{"key":"20_CR36","series-title":"Blockchain Technologies","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-981-15-1137-0_4","volume-title":"Blockchain Technology for Industry 4.0","author":"N Zupan","year":"2020","unstructured":"Zupan, N., Kasinathan, P., Cuellar, J., Sauer, M.: Secure smart contract generation based on petri nets. In: Rosa Righi, R., Alberti, A.M., Singh, M. (eds.) Blockchain Technology for Industry 4.0. BT, pp. 73\u201398. Springer, Singapore (2020). https:\/\/doi.org\/10.1007\/978-981-15-1137-0_4"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98682-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T10:31:03Z","timestamp":1783506663000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}