[{"date_updated":"2023-03-20T07:29:28Z","citation":{"mla":"Koval, Nikita, et al. “Fast and Scalable Channels in Kotlin Coroutines.” Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Association for Computing Machinery, 2023, pp. 107–18, doi:10.1145/3572848.3577481.","ieee":"N. Koval, D.-A. Alistarh, and R. Elizarov, “Fast and scalable channels in Kotlin Coroutines,” in Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Montreal, QC, Canada, 2023, pp. 107–118.","short":"N. Koval, D.-A. Alistarh, R. Elizarov, in:, Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Association for Computing Machinery, 2023, pp. 107–118.","ama":"Koval N, Alistarh D-A, Elizarov R. Fast and scalable channels in Kotlin Coroutines. In: Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. Association for Computing Machinery; 2023:107-118. doi:10.1145/3572848.3577481","apa":"Koval, N., Alistarh, D.-A., & Elizarov, R. (2023). Fast and scalable channels in Kotlin Coroutines. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (pp. 107–118). Montreal, QC, Canada: Association for Computing Machinery. https://doi.org/10.1145/3572848.3577481","chicago":"Koval, Nikita, Dan-Adrian Alistarh, and Roman Elizarov. “Fast and Scalable Channels in Kotlin Coroutines.” In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 107–18. Association for Computing Machinery, 2023. https://doi.org/10.1145/3572848.3577481.","ista":"Koval N, Alistarh D-A, Elizarov R. 2023. Fast and scalable channels in Kotlin Coroutines. Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. PPoPP: Sympopsium on Principles and Practice of Parallel Programming, 107–118."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"arxiv":["2211.04986"]},"article_processing_charge":"No","author":[{"last_name":"Koval","full_name":"Koval, Nikita","first_name":"Nikita","id":"2F4DB10C-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-3650-940X","full_name":"Alistarh, Dan-Adrian","last_name":"Alistarh","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","first_name":"Dan-Adrian"},{"first_name":"Roman","full_name":"Elizarov, Roman","last_name":"Elizarov"}],"title":"Fast and scalable channels in Kotlin Coroutines","department":[{"_id":"DaAl"}],"_id":"12735","conference":{"name":"PPoPP: Sympopsium on Principles and Practice of Parallel Programming","start_date":"2023-02-25","location":"Montreal, QC, Canada","end_date":"2023-03-01"},"type":"conference","status":"public","year":"2023","publication_status":"published","publication_identifier":{"isbn":["9798400700156"]},"language":[{"iso":"eng"}],"publication":"Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming","day":"25","page":"107-118","date_created":"2023-03-19T23:00:58Z","doi":"10.1145/3572848.3577481","date_published":"2023-02-25T00:00:00Z","abstract":[{"lang":"eng","text":"Asynchronous programming has gained significant popularity over the last decade: support for this programming pattern is available in many popular languages via libraries and native language implementations, typically in the form of coroutines or the async/await construct. Instead of programming via shared memory, this concept assumes implicit synchronization through message passing. The key data structure enabling such communication is the rendezvous channel. Roughly, a rendezvous channel is a blocking queue of size zero, so both send(e) and receive() operations wait for each other, performing a rendezvous when they meet. To optimize the message passing pattern, channels are usually equipped with a fixed-size buffer, so sends do not suspend and put elements into the buffer until its capacity is exceeded. This primitive is known as a buffered channel.\r\n\r\nThis paper presents a fast and scalable algorithm for both rendezvous and buffered channels. Similarly to modern queues, our solution is based on an infinite array with two positional counters for send(e) and receive() operations, leveraging the unconditional Fetch-And-Add instruction to update them. Yet, the algorithm requires non-trivial modifications of this classic pattern, in order to support the full channel semantics, such as buffering and cancellation of waiting requests. We compare the performance of our solution to that of the Kotlin implementation, as well as against other academic proposals, showing up to 9.8× speedup. To showcase its expressiveness and performance, we also integrated the proposed algorithm into the standard Kotlin Coroutines library, replacing the previous channel implementations."}],"oa_version":"Preprint","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2211.04986","open_access":"1"}],"oa":1,"publisher":"Association for Computing Machinery","scopus_import":"1","quality_controlled":"1","month":"02"},{"citation":{"ista":"Aksenov V, Brown TA, Fedorov A, Kokorin I. 2023. Unexpected scaling in path copying trees, Association for Computing Machinery,p.","chicago":"Aksenov, Vitaly, Trevor A Brown, Alexander Fedorov, and Ilya Kokorin. Unexpected Scaling in Path Copying Trees. Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. Association for Computing Machinery, 2023. https://doi.org/10.1145/3572848.3577512.","apa":"Aksenov, V., Brown, T. A., Fedorov, A., & Kokorin, I. (2023). Unexpected scaling in path copying trees. Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (pp. 438–440). Montreal, QB, Canada: Association for Computing Machinery. https://doi.org/10.1145/3572848.3577512","ama":"Aksenov V, Brown TA, Fedorov A, Kokorin I. Unexpected Scaling in Path Copying Trees. Association for Computing Machinery; 2023:438-440. doi:10.1145/3572848.3577512","short":"V. Aksenov, T.A. Brown, A. Fedorov, I. Kokorin, Unexpected Scaling in Path Copying Trees, Association for Computing Machinery, 2023.","ieee":"V. Aksenov, T. A. Brown, A. Fedorov, and I. Kokorin, Unexpected scaling in path copying trees. Association for Computing Machinery, 2023, pp. 438–440.","mla":"Aksenov, Vitaly, et al. “Unexpected Scaling in Path Copying Trees.” Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Association for Computing Machinery, 2023, pp. 438–40, doi:10.1145/3572848.3577512."},"date_updated":"2023-03-20T07:57:27Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","author":[{"first_name":"Vitaly","last_name":"Aksenov","full_name":"Aksenov, Vitaly"},{"full_name":"Brown, Trevor A","last_name":"Brown","id":"3569F0A0-F248-11E8-B48F-1D18A9856A87","first_name":"Trevor A"},{"first_name":"Alexander","id":"2e711909-896a-11ed-bdf8-eb0f5a2984c6","last_name":"Fedorov","full_name":"Fedorov, Alexander"},{"first_name":"Ilya","last_name":"Kokorin","full_name":"Kokorin, Ilya"}],"department":[{"_id":"DaAl"},{"_id":"GradSch"}],"title":"Unexpected scaling in path copying trees","_id":"12736","conference":{"location":"Montreal, QB, Canada","end_date":"2023-03-01","start_date":"2023-02-25","name":"PPoPP: Sympopsium on Principles and Practice of Parallel Programming"},"type":"conference_poster","status":"public","publication_status":"published","year":"2023","publication_identifier":{"isbn":["9798400700156"]},"publication":"Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming","language":[{"iso":"eng"}],"day":"25","page":"438-440","date_created":"2023-03-19T23:00:58Z","doi":"10.1145/3572848.3577512","date_published":"2023-02-25T00:00:00Z","abstract":[{"lang":"eng","text":"Although a wide variety of handcrafted concurrent data structures have been proposed, there is considerable interest in universal approaches (Universal Constructions or UCs) for building concurrent data structures. UCs (semi-)automatically convert a sequential data structure into a concurrent one. The simplest approach uses locks [3, 6] that protect a sequential data structure and allow only one process to access it at a time. However, the resulting data structure is blocking. Most work on UCs instead focuses on obtaining non-blocking progress guarantees such as obstruction-freedom, lock-freedom or wait-freedom. Many non-blocking UCs have appeared. Key examples include the seminal wait-free UC [2] by Herlihy, a NUMA-aware UC [10] by Yi et al., and an efficient UC for large objects [1] by Fatourou et al."}],"acknowledgement":"This work was supported by: the Natural Sciences and Engineering Research Council of Canada (NSERC) Discovery Program grant: RGPIN-2019-04227, and the Canada Foundation for Innovation John R. Evans Leaders Fund (CFI-JELF) with equal support from the Ontario Research Fund CFI Leaders Opportunity Fund: 38512.","oa_version":"Published Version","oa":1,"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1145/3572848.3577512"}],"publisher":"Association for Computing Machinery","quality_controlled":"1","month":"02"},{"language":[{"iso":"eng"}],"file":[{"success":1,"checksum":"22141ab8bc55188e2dfff665e5daecbd","file_id":"12769","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"2023_LIPICS_HenzingerM.pdf","date_created":"2023-03-27T06:37:22Z","creator":"dernst","file_size":872706,"date_updated":"2023-03-27T06:37:22Z"}],"publication_status":"published","publication_identifier":{"isbn":["9783959772662"],"issn":["1868-8969"]},"volume":254,"oa_version":"Published Version","abstract":[{"text":"Dynamic programming (DP) is one of the fundamental paradigms in algorithm design. However,\r\nmany DP algorithms have to fill in large DP tables, represented by two-dimensional arrays, which causes at least quadratic running times and space usages. This has led to the development of improved algorithms for special cases when the DPs satisfy additional properties like, e.g., the Monge property or total monotonicity.\r\nIn this paper, we consider a new condition which assumes (among some other technical assumptions) that the rows of the DP table are monotone. Under this assumption, we introduce\r\na novel data structure for computing (1 + ϵ)-approximate DP solutions in near-linear time and\r\nspace in the static setting, and with polylogarithmic update times when the DP entries change\r\ndynamically. To the best of our knowledge, our new condition is incomparable to previous conditions and is the first which allows to derive dynamic algorithms based on existing DPs. Instead of using two-dimensional arrays to store the DP tables, we store the rows of the DP tables using monotone piecewise constant functions. This allows us to store length-n DP table rows with entries in [0, W] using only polylog(n, W) bits, and to perform operations, such as (min, +)-convolution or rounding, on these functions in polylogarithmic time.\r\nWe further present several applications of our data structure. For bicriteria versions of k-balanced graph partitioning and simultaneous source location, we obtain the first dynamic algorithms with subpolynomial update times, as well as the first static algorithms using only near-linear time and space. Additionally, we obtain the currently fastest algorithm for fully dynamic knapsack.","lang":"eng"}],"intvolume":" 254","month":"03","alternative_title":["LIPIcs"],"scopus_import":"1","ddc":["000"],"date_updated":"2023-03-27T06:46:27Z","file_date_updated":"2023-03-27T06:37:22Z","department":[{"_id":"MoHe"}],"_id":"12760","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"location":"Hamburg, Germany","end_date":"2023-03-09","start_date":"2023-03-07","name":"STACS: Symposium on Theoretical Aspects of Computer Science"},"type":"conference","publication":"40th International Symposium on Theoretical Aspects of Computer Science","day":"01","year":"2023","has_accepted_license":"1","date_created":"2023-03-26T22:01:07Z","date_published":"2023-03-01T00:00:00Z","doi":"10.4230/LIPIcs.STACS.2023.36","acknowledgement":"Monika Henzinger: This project has received funding from the European Research Council\r\n(ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant\r\nagreement No. 101019564 “The Design of Modern Fully Dynamic Data Structures (MoDynStruct)” and from the Austrian Science Fund (FWF) project “Fast Algorithms for a Reactive Network Layer (ReactNet)”, P 33775-N, with additional funding from the netidee SCIENCE Stiftung, 2020–2024.\r\nStefan Neumann: This research is supported by the the ERC Advanced Grant REBOUND (834862) and the EC H2020 RIA project SoBigData++ (871042).\r\nStefan Schmid: Research supported by Austrian Science Fund (FWF) project I 5025-N (DELTA), 2020-2024.","oa":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Henzinger MH, Neumann S, Räcke H, Schmid S. 2023. Dynamic maintenance of monotone dynamic programs and applications. 40th International Symposium on Theoretical Aspects of Computer Science. STACS: Symposium on Theoretical Aspects of Computer Science, LIPIcs, vol. 254, 36.","chicago":"Henzinger, Monika H, Stefan Neumann, Harald Räcke, and Stefan Schmid. “Dynamic Maintenance of Monotone Dynamic Programs and Applications.” In 40th International Symposium on Theoretical Aspects of Computer Science, Vol. 254. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. https://doi.org/10.4230/LIPIcs.STACS.2023.36.","short":"M.H. Henzinger, S. Neumann, H. Räcke, S. Schmid, in:, 40th International Symposium on Theoretical Aspects of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.","ieee":"M. H. Henzinger, S. Neumann, H. Räcke, and S. Schmid, “Dynamic maintenance of monotone dynamic programs and applications,” in 40th International Symposium on Theoretical Aspects of Computer Science, Hamburg, Germany, 2023, vol. 254.","apa":"Henzinger, M. H., Neumann, S., Räcke, H., & Schmid, S. (2023). Dynamic maintenance of monotone dynamic programs and applications. In 40th International Symposium on Theoretical Aspects of Computer Science (Vol. 254). Hamburg, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.STACS.2023.36","ama":"Henzinger MH, Neumann S, Räcke H, Schmid S. Dynamic maintenance of monotone dynamic programs and applications. In: 40th International Symposium on Theoretical Aspects of Computer Science. Vol 254. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.STACS.2023.36","mla":"Henzinger, Monika H., et al. “Dynamic Maintenance of Monotone Dynamic Programs and Applications.” 40th International Symposium on Theoretical Aspects of Computer Science, vol. 254, 36, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:10.4230/LIPIcs.STACS.2023.36."},"title":"Dynamic maintenance of monotone dynamic programs and applications","external_id":{"arxiv":["2301.01744"]},"article_processing_charge":"No","author":[{"orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H"},{"last_name":"Neumann","full_name":"Neumann, Stefan","first_name":"Stefan"},{"full_name":"Räcke, Harald","last_name":"Räcke","first_name":"Harald"},{"first_name":"Stefan","full_name":"Schmid, Stefan","last_name":"Schmid"}],"article_number":"36"},{"project":[{"call_identifier":"H2020","_id":"2634E9D2-B435-11E9-9278-68D0E5697425","name":"Circuits of Visual Attention","grant_number":"756502"}],"citation":{"short":"L. Burnett, To Flee, or Not to Flee? Using Innate Defensive Behaviours to Investigate Rapid Perceptual Decision-Making through Subcortical Circuits in Mouse Models of Autism, Institute of Science and Technology Austria, 2023.","ieee":"L. Burnett, “To flee, or not to flee? Using innate defensive behaviours to investigate rapid perceptual decision-making through subcortical circuits in mouse models of autism,” Institute of Science and Technology Austria, 2023.","apa":"Burnett, L. (2023). To flee, or not to flee? Using innate defensive behaviours to investigate rapid perceptual decision-making through subcortical circuits in mouse models of autism. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:12716","ama":"Burnett L. To flee, or not to flee? Using innate defensive behaviours to investigate rapid perceptual decision-making through subcortical circuits in mouse models of autism. 2023. doi:10.15479/at:ista:12716","mla":"Burnett, Laura. To Flee, or Not to Flee? Using Innate Defensive Behaviours to Investigate Rapid Perceptual Decision-Making through Subcortical Circuits in Mouse Models of Autism. Institute of Science and Technology Austria, 2023, doi:10.15479/at:ista:12716.","ista":"Burnett L. 2023. To flee, or not to flee? Using innate defensive behaviours to investigate rapid perceptual decision-making through subcortical circuits in mouse models of autism. Institute of Science and Technology Austria.","chicago":"Burnett, Laura. “To Flee, or Not to Flee? Using Innate Defensive Behaviours to Investigate Rapid Perceptual Decision-Making through Subcortical Circuits in Mouse Models of Autism.” Institute of Science and Technology Austria, 2023. https://doi.org/10.15479/at:ista:12716."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","article_processing_charge":"No","author":[{"orcid":"0000-0002-8937-410X","full_name":"Burnett, Laura","last_name":"Burnett","id":"3B717F68-F248-11E8-B48F-1D18A9856A87","first_name":"Laura"}],"title":"To flee, or not to flee? Using innate defensive behaviours to investigate rapid perceptual decision-making through subcortical circuits in mouse models of autism","oa":1,"publisher":"Institute of Science and Technology Austria","year":"2023","has_accepted_license":"1","day":"10","page":"178","date_created":"2023-03-08T15:19:45Z","date_published":"2023-03-10T00:00:00Z","doi":"10.15479/at:ista:12716","_id":"12716","type":"dissertation","status":"public","date_updated":"2023-04-05T10:59:04Z","supervisor":[{"first_name":"Maximilian A","id":"2BD278E6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3937-1330","full_name":"Jösch, Maximilian A","last_name":"Jösch"}],"ddc":["599","573"],"file_date_updated":"2023-03-08T15:08:46Z","department":[{"_id":"GradSch"},{"_id":"MaJö"}],"abstract":[{"text":"The process of detecting and evaluating sensory information to guide behaviour is termed perceptual decision-making (PDM), and is critical for the ability of an organism to interact with its external world. Individuals with autism, a neurodevelopmental condition primarily characterised by social and communication difficulties, frequently exhibit altered sensory processing and PDM difficulties are widely reported. Recent technological advancements have pushed forward our understanding of the genetic changes accompanying this condition, however our understanding of how these mutations affect the function of specific neuronal circuits and bring about the corresponding behavioural changes remains limited. Here, we use an innate PDM task, the looming avoidance response (LAR) paradigm, to identify a convergent behavioural abnormality across three molecularly distinct genetic mouse models of autism (Cul3, Setd5 and Ptchd1). Although mutant mice can rapidly detect threatening visual stimuli, their responses are consistently delayed, requiring longer to initiate an appropriate response than their wild-type siblings. Mutant animals show abnormal adaptation in both their stimulus- evoked escape responses and exploratory dynamics following repeated stimulus presentations. Similarly delayed behavioural responses are observed in wild-type animals when faced with more ambiguous threats, suggesting the mutant phenotype could arise from a dysfunction in the flexible control of this PDM process.\r\nOur knowledge of the core neuronal circuitry mediating the LAR facilitated a detailed dissection of the neuronal mechanisms underlying the behavioural impairment. In vivo extracellular recording revealed that visual responses were unaffected within a key brain region for the rapid processing of visual threats, the superior colliculus (SC), indicating that the behavioural delay was unlikely to originate from sensory impairments. Delayed behavioural responses were recapitulated in the Setd5 model following optogenetic stimulation of the excitatory output neurons of the SC, which are known to mediate escape initiation through the activation of cells in the underlying dorsal periaqueductal grey (dPAG). In vitro patch-clamp recordings of dPAG cells uncovered a stark hypoexcitability phenotype in two out of the three genetic models investigated (Setd5 and Ptchd1), that in Setd5, is mediated by the misregulation of voltage-gated potassium channels. Overall, our results show that the ability to use visual information to drive efficient escape responses is impaired in three diverse genetic mouse models of autism and that, in one of the models studied, this behavioural delay likely originates from differences in the intrinsic excitability of a key subcortical node, the dPAG. Furthermore, this work showcases the use of an innate behavioural paradigm to mechanistically dissect PDM processes in autism.","lang":"eng"}],"acknowledged_ssus":[{"_id":"PreCl"},{"_id":"Bio"},{"_id":"LifeSc"},{"_id":"M-Shop"},{"_id":"CampIT"}],"oa_version":"Published Version","alternative_title":["ISTA Thesis"],"month":"03","degree_awarded":"PhD","publication_status":"published","publication_identifier":{"issn":["2663-337X"]},"language":[{"iso":"eng"}],"file":[{"date_created":"2023-03-08T15:08:46Z","file_name":"Burnett_Thesis_2023.docx","creator":"lburnett","date_updated":"2023-03-08T15:08:46Z","file_size":23029260,"checksum":"6c6d9cc2c4cdacb74e6b1047a34d7332","file_id":"12717","access_level":"closed","relation":"source_file","content_type":"application/vnd.openxmlformats-officedocument.wordprocessingml.document"},{"creator":"lburnett","date_updated":"2023-03-08T15:08:46Z","file_size":11959869,"date_created":"2023-03-08T15:08:46Z","file_name":"Burnett_Thesis_2023_pdfA.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"12718","checksum":"cebc77705288bf4382db9b3541483cd0","success":1}],"ec_funded":1},{"page":"535-540","date_created":"2023-04-20T08:22:53Z","date_published":"2023-04-20T00:00:00Z","doi":"10.1007/978-3-031-30820-8_32","year":"2023","has_accepted_license":"1","publication":"Tools and Algorithms for the Construction and Analysis of Systems","day":"20","oa":1,"publisher":"Springer Nature","quality_controlled":"1","acknowledgement":"This work was supported by the ERC-2020-AdG 10102009 grant.","article_processing_charge":"No","author":[{"last_name":"Chalupa","full_name":"Chalupa, Marek","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"}],"title":"Bubaak: Runtime monitoring of program verifiers","citation":{"mla":"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.","short":"M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 535–540.","ieee":"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.","apa":"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","ama":"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","chicago":"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.","ista":"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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"ec_funded":1,"volume":13994,"publication_status":"published","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031308192"],"issn":["0302-9743"],"eisbn":["9783031308208"]},"language":[{"iso":"eng"}],"file":[{"file_size":16096413,"date_updated":"2023-04-25T06:58:36Z","creator":"dernst","file_name":"2023_LNCS_Chalupa.pdf","date_created":"2023-04-25T06:58:36Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","success":1,"file_id":"12864","checksum":"120d2c2a38384058ad0630fdf8288312"}],"alternative_title":["LNCS"],"intvolume":" 13994","month":"04","abstract":[{"text":"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.\r\nAt 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.","lang":"eng"}],"oa_version":"Published Version","file_date_updated":"2023-04-25T06:58:36Z","department":[{"_id":"ToHe"}],"date_updated":"2023-04-25T07:02:43Z","ddc":["000"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22","location":"Paris, France","end_date":"2023-04-27"},"type":"conference","status":"public","_id":"12854"}]