[{"language":[{"iso":"eng"}],"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2012-03-24","location":"Tallinn, Estonia","end_date":"2012-04-01"},"publication":"Tools and Algorithms for the Construction and Analysis of Systems","oa_version":"Published Version","month":"04","place":"Berlin, Heidelberg","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-642-28756-5_46"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_published":"2012-04-01T00:00:00Z","type":"conference","publication_identifier":{"eisbn":["9783642287565"],"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783642287558"]},"oa":1,"page":"549-551","quality_controlled":"1","series_title":"LNCS","publisher":"Springer","editor":[{"first_name":"Cormac","last_name":"Flanagan","full_name":"Flanagan, Cormac"},{"full_name":"König, Barbara","first_name":"Barbara","last_name":"König"}],"_id":"10906","scopus_import":"1","author":[{"full_name":"Grebenshchikov, Sergey","first_name":"Sergey","last_name":"Grebenshchikov"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh"},{"first_name":"Nuno P.","last_name":"Lopes","full_name":"Lopes, Nuno P."},{"last_name":"Popeea","first_name":"Corneliu","full_name":"Popeea, Corneliu"},{"last_name":"Rybalchenko","first_name":"Andrey","full_name":"Rybalchenko, Andrey"}],"publication_status":"published","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2022-03-21T08:03:30Z","title":"HSF(C): A software verifier based on Horn clauses","alternative_title":["LNCS"],"intvolume":"      7214","volume":7214,"date_updated":"2023-09-05T14:09:54Z","year":"2012","citation":{"ista":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C): A software verifier based on Horn clauses. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.","mla":"Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn Clauses.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">10.1007/978-3-642-28756-5_46</a>.","short":"S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:, C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.","ieee":"S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Tallinn, Estonia, 2012, vol. 7214, pp. 549–551.","chicago":"Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">https://doi.org/10.1007/978-3-642-28756-5_46</a>.","ama":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software verifier based on Horn clauses. In: Flanagan C, König B, eds. <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">10.1007/978-3-642-28756-5_46</a>","apa":"Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., &#38; Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &#38; B. König (Eds.), <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">https://doi.org/10.1007/978-3-642-28756-5_46</a>"},"doi":"10.1007/978-3-642-28756-5_46","day":"01","abstract":[{"text":"HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool.","lang":"eng"}]},{"author":[{"first_name":"Riccardo","last_name":"Colini-Baldeschi","full_name":"Colini-Baldeschi, Riccardo"},{"first_name":"Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"full_name":"Leonardi, Stefano","first_name":"Stefano","last_name":"Leonardi"},{"last_name":"Starnberger","first_name":"Martin","full_name":"Starnberger, Martin"}],"scopus_import":"1","_id":"11795","intvolume":"      7392","alternative_title":["LNCS"],"title":"On multiple keyword sponsored search auctions with budgets","article_processing_charge":"No","date_created":"2022-08-11T11:46:51Z","publication_status":"published","quality_controlled":"1","page":"1–12","publisher":"Springer Nature","year":"2012","citation":{"ieee":"R. Colini-Baldeschi, M. H. Henzinger, S. Leonardi, and M. Starnberger, “On multiple keyword sponsored search auctions with budgets,” in <i>39th International Colloquium on Automata, Languages, and Programming</i>, Warwick, United Kingdom, 2012, vol. 7392, pp. 1–12.","chicago":"Colini-Baldeschi, Riccardo, Monika H Henzinger, Stefano Leonardi, and Martin Starnberger. “On Multiple Keyword Sponsored Search Auctions with Budgets.” In <i>39th International Colloquium on Automata, Languages, and Programming</i>, 7392:1–12. Springer Nature, 2012. <a href=\"https://doi.org/10.1007/978-3-642-31585-5_1\">https://doi.org/10.1007/978-3-642-31585-5_1</a>.","ama":"Colini-Baldeschi R, Henzinger MH, Leonardi S, Starnberger M. On multiple keyword sponsored search auctions with budgets. In: <i>39th International Colloquium on Automata, Languages, and Programming</i>. Vol 7392. Springer Nature; 2012:1–12. doi:<a href=\"https://doi.org/10.1007/978-3-642-31585-5_1\">10.1007/978-3-642-31585-5_1</a>","apa":"Colini-Baldeschi, R., Henzinger, M. H., Leonardi, S., &#38; Starnberger, M. (2012). On multiple keyword sponsored search auctions with budgets. In <i>39th International Colloquium on Automata, Languages, and Programming</i> (Vol. 7392, pp. 1–12). Warwick, United Kingdom: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-31585-5_1\">https://doi.org/10.1007/978-3-642-31585-5_1</a>","ista":"Colini-Baldeschi R, Henzinger MH, Leonardi S, Starnberger M. 2012. On multiple keyword sponsored search auctions with budgets. 39th International Colloquium on Automata, Languages, and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LNCS, vol. 7392, 1–12.","mla":"Colini-Baldeschi, Riccardo, et al. “On Multiple Keyword Sponsored Search Auctions with Budgets.” <i>39th International Colloquium on Automata, Languages, and Programming</i>, vol. 7392, Springer Nature, 2012, pp. 1–12, doi:<a href=\"https://doi.org/10.1007/978-3-642-31585-5_1\">10.1007/978-3-642-31585-5_1</a>.","short":"R. Colini-Baldeschi, M.H. Henzinger, S. Leonardi, M. Starnberger, in:, 39th International Colloquium on Automata, Languages, and Programming, Springer Nature, 2012, pp. 1–12."},"date_updated":"2023-02-21T16:28:31Z","abstract":[{"text":"We study multiple keyword sponsored search auctions with budgets. Each keyword has multiple ad slots with a click-through rate. The bidders have additive valuations, which are linear in the click-through rates, and budgets, which are restricting their overall payments. Additionally, the number of slots per keyword assigned to a bidder is bounded.\r\n\r\nWe show the following results: (1) We give the first mechanism for multiple keywords, where click-through rates differ among slots. Our mechanism is incentive compatible in expectation, individually rational in expectation, and Pareto optimal. (2) We study the combinatorial setting, where each bidder is only interested in a subset of the keywords. We give an incentive compatible, individually rational, Pareto optimal, and deterministic mechanism for identical click-through rates. (3) We give an impossibility result for incentive compatible, individually rational, Pareto optimal, and deterministic mechanisms for bidders with diminishing marginal valuations.","lang":"eng"}],"day":"01","doi":"10.1007/978-3-642-31585-5_1","extern":"1","volume":7392,"publication":"39th International Colloquium on Automata, Languages, and Programming","month":"07","oa_version":"None","language":[{"iso":"eng"}],"conference":{"end_date":"2012-07-13","location":"Warwick, United Kingdom","name":"ICALP: International Colloquium on Automata, Languages, and Programming","start_date":"2012-07-09"},"type":"conference","date_published":"2012-07-01T00:00:00Z","publication_identifier":{"issn":["0302-9743"],"isbn":["9783642315848"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","related_material":{"record":[{"id":"11795","relation":"later_version","status":"public"}]}},{"file":[{"content_type":"application/pdf","file_name":"2012_ATVA_Gupta.pdf","date_updated":"2020-07-14T12:47:10Z","checksum":"68415837a315de3cc4d120f6019d752c","file_size":465502,"date_created":"2018-12-18T13:07:35Z","creator":"dernst","file_id":"5746","access_level":"open_access","relation":"main_file"}],"place":"Berlin, Heidelberg","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783642333859","9783642333866"]},"oa":1,"type":"book_chapter","date_published":"2012-01-01T00:00:00Z","conference":{"location":"Thiruvananthapuram, Kerala, India","end_date":"2012-10-06","start_date":"2012-10-03","name":"ATVA 2012"},"language":[{"iso":"eng"}],"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"oa_version":"None","has_accepted_license":"1","publication":"Automated Technology for Verification and Analysis","volume":7561,"ddc":["005"],"doi":"10.1007/978-3-642-33386-6_10","year":"2012","citation":{"ieee":"A. Gupta, “Improved Single Pass Algorithms for Resolution Proof Reduction,” in <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 107–121.","chicago":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” In <i>Automated Technology for Verification and Analysis</i>, 7561:107–21. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>.","apa":"Gupta, A. (2012). Improved Single Pass Algorithms for Resolution Proof Reduction. In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 107–121). Berlin, Heidelberg: Springer Berlin Heidelberg. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>","ama":"Gupta A. Improved Single Pass Algorithms for Resolution Proof Reduction. In: <i>Automated Technology for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg; 2012:107-121. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>","ista":"Gupta A. 2012.Improved Single Pass Algorithms for Resolution Proof Reduction. In: Automated Technology for Verification and Analysis. vol. 7561, 107–121.","mla":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Springer Berlin Heidelberg, 2012, pp. 107–21, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>.","short":"A. Gupta, in:, Automated Technology for Verification and Analysis, Springer Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 107–121."},"date_updated":"2023-09-05T14:15:29Z","publisher":"Springer Berlin Heidelberg","ec_funded":1,"series_title":"LNCS","quality_controlled":"1","page":"107-121","file_date_updated":"2020-07-14T12:47:10Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"date_created":"2018-12-18T13:01:46Z","publication_status":"published","intvolume":"      7561","title":"Improved Single Pass Algorithms for Resolution Proof Reduction","pubrep_id":"180","_id":"5745","author":[{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh"}]},{"series_title":"LNIP","quality_controlled":"1","page":"215-224","editor":[{"full_name":"Jiang, Xiaoyi","last_name":"Jiang","first_name":"Xiaoyi"},{"last_name":"Ferrer","first_name":"Miquel","full_name":"Ferrer, Miquel"},{"full_name":"Torsello, Andrea","last_name":"Torsello","first_name":"Andrea"}],"publisher":"Springer","author":[{"full_name":"Artner, Nicole M.","last_name":"Artner","first_name":"Nicole M."},{"last_name":"Ion","first_name":"Adrian","full_name":"Ion, Adrian","id":"29F89302-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kropatsch","first_name":"Walter G.","full_name":"Kropatsch, Walter G."}],"scopus_import":"1","_id":"10907","intvolume":"      6658","alternative_title":["LNCS"],"title":"Spatio-temporal extraction of articulated models in a graph pyramid","department":[{"_id":"HeEd"}],"article_processing_charge":"No","date_created":"2022-03-21T08:08:35Z","publication_status":"published","volume":6658,"acknowledgement":"This work has been partially supported by the Austrian Science Fund under grants S9103-N13 and P18716-N13.","year":"2011","citation":{"ista":"Artner NM, Ion A, Kropatsch WG. 2011. Spatio-temporal extraction of articulated models in a graph pyramid. Graph-Based Representations in Pattern Recognition. GbRPR: Graph-based Representations in Pattern RecognitionLNIP, LNCS, vol. 6658, 215–224.","short":"N.M. Artner, A. Ion, W.G. Kropatsch, in:, X. Jiang, M. Ferrer, A. Torsello (Eds.), Graph-Based Representations in Pattern Recognition, Springer, Berlin, Heidelberg, 2011, pp. 215–224.","mla":"Artner, Nicole M., et al. “Spatio-Temporal Extraction of Articulated Models in a Graph Pyramid.” <i>Graph-Based Representations in Pattern Recognition</i>, edited by Xiaoyi Jiang et al., vol. 6658, Springer, 2011, pp. 215–24, doi:<a href=\"https://doi.org/10.1007/978-3-642-20844-7_22\">10.1007/978-3-642-20844-7_22</a>.","chicago":"Artner, Nicole M., Adrian Ion, and Walter G. Kropatsch. “Spatio-Temporal Extraction of Articulated Models in a Graph Pyramid.” In <i>Graph-Based Representations in Pattern Recognition</i>, edited by Xiaoyi Jiang, Miquel Ferrer, and Andrea Torsello, 6658:215–24. LNIP. Berlin, Heidelberg: Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-20844-7_22\">https://doi.org/10.1007/978-3-642-20844-7_22</a>.","ieee":"N. M. Artner, A. Ion, and W. G. Kropatsch, “Spatio-temporal extraction of articulated models in a graph pyramid,” in <i>Graph-Based Representations in Pattern Recognition</i>, Münster, Germany, 2011, vol. 6658, pp. 215–224.","apa":"Artner, N. M., Ion, A., &#38; Kropatsch, W. G. (2011). Spatio-temporal extraction of articulated models in a graph pyramid. In X. Jiang, M. Ferrer, &#38; A. Torsello (Eds.), <i>Graph-Based Representations in Pattern Recognition</i> (Vol. 6658, pp. 215–224). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-20844-7_22\">https://doi.org/10.1007/978-3-642-20844-7_22</a>","ama":"Artner NM, Ion A, Kropatsch WG. Spatio-temporal extraction of articulated models in a graph pyramid. In: Jiang X, Ferrer M, Torsello A, eds. <i>Graph-Based Representations in Pattern Recognition</i>. Vol 6658. LNIP. Berlin, Heidelberg: Springer; 2011:215-224. doi:<a href=\"https://doi.org/10.1007/978-3-642-20844-7_22\">10.1007/978-3-642-20844-7_22</a>"},"date_updated":"2023-09-05T14:10:15Z","abstract":[{"text":"This paper presents a method to create a model of an articulated object using the planar motion in an initialization video. The model consists of rigid parts connected by points of articulation. The rigid parts are described by the positions of salient feature-points tracked throughout the video. Following a filtering step that identifies points that belong to different objects, rigid parts are found by a grouping process in a graph pyramid. Valid articulation points are selected by verifying multiple hypotheses for each pair of parts.","lang":"eng"}],"day":"01","doi":"10.1007/978-3-642-20844-7_22","language":[{"iso":"eng"}],"conference":{"name":"GbRPR: Graph-based Representations in Pattern Recognition","start_date":"2011-05-18","end_date":"2011-05-20","location":"Münster, Germany"},"publication":"Graph-Based Representations in Pattern Recognition","month":"06","oa_version":"None","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","place":"Berlin, Heidelberg","type":"conference","date_published":"2011-06-01T00:00:00Z","publication_identifier":{"eisbn":["9783642208447"],"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783642208430"]}},{"publication":"Logic for Programming, Artificial Intelligence, and Reasoning","month":"05","oa_version":"Submitted Version","language":[{"iso":"eng"}],"conference":{"name":"LPAR: Conference on Logic for Programming, Artificial Intelligence and Reasoning","start_date":"2010-04-25","location":"Dakar, Senegal","end_date":"2010-05-01"},"date_published":"2010-05-01T00:00:00Z","type":"conference","oa":1,"publication_identifier":{"eisbn":["9783642175114"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783642175107"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","main_file_link":[{"open_access":"1","url":"https://infoscience.epfl.ch/record/186096"}],"place":"Berlin, Heidelberg","author":[{"first_name":"Régis","last_name":"Blanc","full_name":"Blanc, Régis"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"},{"full_name":"Hottelier, Thibaud","last_name":"Hottelier","first_name":"Thibaud"},{"last_name":"Kovács","first_name":"Laura","full_name":"Kovács, Laura"}],"_id":"10908","scopus_import":"1","title":"ABC: Algebraic Bound Computation for loops","intvolume":"      6355","publication_status":"published","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2022-03-21T08:14:35Z","page":"103-118","quality_controlled":"1","series_title":"LNCS","publisher":"Springer Nature","editor":[{"full_name":"Clarke, Edmund M","first_name":"Edmund M","last_name":"Clarke"},{"full_name":"Voronkov, Andrei","first_name":"Andrei","last_name":"Voronkov"}],"date_updated":"2022-06-13T07:44:21Z","citation":{"mla":"Blanc, Régis, et al. “ABC: Algebraic Bound Computation for Loops.” <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, edited by Edmund M Clarke and Andrei Voronkov, vol. 6355, Springer Nature, 2010, pp. 103–18, doi:<a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">10.1007/978-3-642-17511-4_7</a>.","short":"R. Blanc, T.A. Henzinger, T. Hottelier, L. Kovács, in:, E.M. Clarke, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, Springer Nature, Berlin, Heidelberg, 2010, pp. 103–118.","ista":"Blanc R, Henzinger TA, Hottelier T, Kovács L. 2010. ABC: Algebraic Bound Computation for loops. Logic for Programming, Artificial Intelligence, and Reasoning. LPAR: Conference on Logic for Programming, Artificial Intelligence and ReasoningLNCS vol. 6355, 103–118.","ama":"Blanc R, Henzinger TA, Hottelier T, Kovács L. ABC: Algebraic Bound Computation for loops. In: Clarke EM, Voronkov A, eds. <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>. Vol 6355. LNCS. Berlin, Heidelberg: Springer Nature; 2010:103-118. doi:<a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">10.1007/978-3-642-17511-4_7</a>","apa":"Blanc, R., Henzinger, T. A., Hottelier, T., &#38; Kovács, L. (2010). ABC: Algebraic Bound Computation for loops. In E. M. Clarke &#38; A. Voronkov (Eds.), <i>Logic for Programming, Artificial Intelligence, and Reasoning</i> (Vol. 6355, pp. 103–118). Berlin, Heidelberg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">https://doi.org/10.1007/978-3-642-17511-4_7</a>","ieee":"R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács, “ABC: Algebraic Bound Computation for loops,” in <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, Dakar, Senegal, 2010, vol. 6355, pp. 103–118.","chicago":"Blanc, Régis, Thomas A Henzinger, Thibaud Hottelier, and Laura Kovács. “ABC: Algebraic Bound Computation for Loops.” In <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, edited by Edmund M Clarke and Andrei Voronkov, 6355:103–18. LNCS. Berlin, Heidelberg: Springer Nature, 2010. <a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">https://doi.org/10.1007/978-3-642-17511-4_7</a>."},"year":"2010","abstract":[{"lang":"eng","text":"We present ABC, a software tool for automatically computing symbolic upper bounds on the number of iterations of nested program loops. The system combines static analysis of programs with symbolic summation techniques to derive loop invariant relations between program variables. Iteration bounds are obtained from the inferred invariants, by replacing variables with bounds on their greatest values. We have successfully applied ABC to a large number of examples. The derived symbolic bounds express non-trivial polynomial relations over loop variables. We also report on results to automatically infer symbolic expressions over harmonic numbers as upper bounds on loop iteration counts."}],"doi":"10.1007/978-3-642-17511-4_7","day":"01","volume":6355,"acknowledgement":"This work was supported in part by the Swiss NSF. The fourth author is supported by an FWF Hertha Firnberg Research grant (T425-N23)."},{"date_updated":"2022-04-01T13:45:24Z","year":"2010","citation":{"mla":"Juhás, Gabriel, et al. “Instance Deadlock: A Mystery behind Frozen Programs.” <i>Applications and Theory of Petri Nets</i>, Springer Berlin Heidelberg, 2010, pp. 1–17, doi:<a href=\"https://doi.org/10.1007/978-3-642-13675-7_1\">10.1007/978-3-642-13675-7_1</a>.","short":"G. Juhás, I. Kazlov, A. Juhásová, in:, Applications and Theory of Petri Nets, Springer Berlin Heidelberg, Berlin, Heidelberg, 2010, pp. 1–17.","ista":"Juhás G, Kazlov I, Juhásová A. 2010.Instance Deadlock: A Mystery behind Frozen Programs. In: Applications and Theory of Petri Nets. , 1–17.","ama":"Juhás G, Kazlov I, Juhásová A. Instance Deadlock: A Mystery behind Frozen Programs. In: <i>Applications and Theory of Petri Nets</i>. Berlin, Heidelberg: Springer Berlin Heidelberg; 2010:1-17. doi:<a href=\"https://doi.org/10.1007/978-3-642-13675-7_1\">10.1007/978-3-642-13675-7_1</a>","apa":"Juhás, G., Kazlov, I., &#38; Juhásová, A. (2010). Instance Deadlock: A Mystery behind Frozen Programs. In <i>Applications and Theory of Petri Nets</i> (pp. 1–17). Berlin, Heidelberg: Springer Berlin Heidelberg. <a href=\"https://doi.org/10.1007/978-3-642-13675-7_1\">https://doi.org/10.1007/978-3-642-13675-7_1</a>","chicago":"Juhás, Gabriel, Igor Kazlov, and Ana Juhásová. “Instance Deadlock: A Mystery behind Frozen Programs.” In <i>Applications and Theory of Petri Nets</i>, 1–17. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010. <a href=\"https://doi.org/10.1007/978-3-642-13675-7_1\">https://doi.org/10.1007/978-3-642-13675-7_1</a>.","ieee":"G. Juhás, I. Kazlov, and A. Juhásová, “Instance Deadlock: A Mystery behind Frozen Programs,” in <i>Applications and Theory of Petri Nets</i>, Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 1–17."},"date_published":"2010-01-01T00:00:00Z","type":"book_chapter","doi":"10.1007/978-3-642-13675-7_1","publication_identifier":{"isbn":["9783642136740","9783642136757"],"issn":["0302-9743","1611-3349"]},"place":"Berlin, Heidelberg","extern":"1","status":"public","user_id":"4A997E50-F248-11E8-B48F-1D18A9856A87","publication":"Applications and Theory of Petri Nets","_id":"5940","author":[{"full_name":"Juhás, Gabriel","first_name":"Gabriel","last_name":"Juhás"},{"id":"4A997E50-F248-11E8-B48F-1D18A9856A87","last_name":"Kazlov","first_name":"Igor","full_name":"Kazlov, Igor"},{"full_name":"Juhásová, Ana","last_name":"Juhásová","first_name":"Ana"}],"publication_status":"published","oa_version":"None","article_processing_charge":"No","date_created":"2019-02-08T09:33:41Z","title":"Instance Deadlock: A Mystery behind Frozen Programs","page":"1-17","language":[{"iso":"eng"}],"publisher":"Springer Berlin Heidelberg"},{"author":[{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H","last_name":"Henzinger"}],"scopus_import":"1","_id":"11800","publication":"31st International Colloquium on Automata, Languages and Programming","intvolume":"      3142","alternative_title":["LNCS"],"month":"07","title":"The past, present, and future of web search engines","article_processing_charge":"No","date_created":"2022-08-11T12:38:58Z","publication_status":"published","oa_version":"None","language":[{"iso":"eng"}],"quality_controlled":"1","page":"3","conference":{"end_date":"2004-07-16","location":"Turku, Finland","name":"ICALP: International Colloquium on Automata, Languages, and Programming","start_date":"2004-07-12"},"publisher":"Springer Nature","type":"conference","date_published":"2004-07-01T00:00:00Z","citation":{"ama":"Henzinger MH. The past, present, and future of web search engines. In: <i>31st International Colloquium on Automata, Languages and Programming</i>. Vol 3142. Springer Nature; 2004:3. doi:<a href=\"https://doi.org/10.1007/978-3-540-27836-8_2\">10.1007/978-3-540-27836-8_2</a>","apa":"Henzinger, M. H. (2004). The past, present, and future of web search engines. In <i>31st International Colloquium on Automata, Languages and Programming</i> (Vol. 3142, p. 3). Turku, Finland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-540-27836-8_2\">https://doi.org/10.1007/978-3-540-27836-8_2</a>","chicago":"Henzinger, Monika H. “The Past, Present, and Future of Web Search Engines.” In <i>31st International Colloquium on Automata, Languages and Programming</i>, 3142:3. Springer Nature, 2004. <a href=\"https://doi.org/10.1007/978-3-540-27836-8_2\">https://doi.org/10.1007/978-3-540-27836-8_2</a>.","ieee":"M. H. Henzinger, “The past, present, and future of web search engines,” in <i>31st International Colloquium on Automata, Languages and Programming</i>, Turku, Finland, 2004, vol. 3142, p. 3.","mla":"Henzinger, Monika H. “The Past, Present, and Future of Web Search Engines.” <i>31st International Colloquium on Automata, Languages and Programming</i>, vol. 3142, Springer Nature, 2004, p. 3, doi:<a href=\"https://doi.org/10.1007/978-3-540-27836-8_2\">10.1007/978-3-540-27836-8_2</a>.","short":"M.H. Henzinger, in:, 31st International Colloquium on Automata, Languages and Programming, Springer Nature, 2004, p. 3.","ista":"Henzinger MH. 2004. The past, present, and future of web search engines. 31st International Colloquium on Automata, Languages and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LNCS, vol. 3142, 3."},"year":"2004","date_updated":"2023-02-13T11:45:25Z","abstract":[{"text":"Web search engines have emerged as one of the central applications on the Internet. In fact, search has become one of the most important activities that people engage in on the the Internet. Even beyond becoming the number one source of information, a growing number of businesses are depending on web search engines for customer acquisition.\r\n\r\nThe first generation of web search engines used text-only retrieval techniques. Google revolutionized the field by deploying the PageRank technology – an eigenvector-based analysis of the hyperlink structure – to analyze the web in order to produce relevant results. Moving forward, our goal is to achieve a better understanding of a page with a view towards producing even more relevant results.","lang":"eng"}],"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"]},"day":"01","doi":"10.1007/978-3-540-27836-8_2","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","extern":"1","volume":3142},{"author":[{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H"}],"publication":"2th Annual European Symposium on Algorithms","_id":"11801","scopus_import":"1","title":"Algorithmic aspects of web search engines","alternative_title":["LNCS"],"month":"09","intvolume":"      3221","publication_status":"published","oa_version":"None","article_processing_charge":"No","date_created":"2022-08-11T13:18:05Z","language":[{"iso":"eng"}],"page":"3","quality_controlled":"1","conference":{"start_date":"2004-09-14","name":"ESA: European Symposium on Algorithms","location":"Bergen, Norway","end_date":"2004-09-17"},"publisher":"Springer Nature","date_published":"2004-09-01T00:00:00Z","type":"conference","date_updated":"2023-02-13T11:47:26Z","year":"2004","citation":{"mla":"Henzinger, Monika H. “Algorithmic Aspects of Web Search Engines.” <i>2th Annual European Symposium on Algorithms</i>, vol. 3221, Springer Nature, 2004, p. 3, doi:<a href=\"https://doi.org/10.1007/978-3-540-30140-0_2\">10.1007/978-3-540-30140-0_2</a>.","short":"M.H. Henzinger, in:, 2th Annual European Symposium on Algorithms, Springer Nature, 2004, p. 3.","ista":"Henzinger MH. 2004. Algorithmic aspects of web search engines. 2th Annual European Symposium on Algorithms. ESA: European Symposium on Algorithms, LNCS, vol. 3221, 3.","ama":"Henzinger MH. Algorithmic aspects of web search engines. In: <i>2th Annual European Symposium on Algorithms</i>. Vol 3221. Springer Nature; 2004:3. doi:<a href=\"https://doi.org/10.1007/978-3-540-30140-0_2\">10.1007/978-3-540-30140-0_2</a>","apa":"Henzinger, M. H. (2004). Algorithmic aspects of web search engines. In <i>2th Annual European Symposium on Algorithms</i> (Vol. 3221, p. 3). Bergen, Norway: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-540-30140-0_2\">https://doi.org/10.1007/978-3-540-30140-0_2</a>","ieee":"M. H. Henzinger, “Algorithmic aspects of web search engines,” in <i>2th Annual European Symposium on Algorithms</i>, Bergen, Norway, 2004, vol. 3221, p. 3.","chicago":"Henzinger, Monika H. “Algorithmic Aspects of Web Search Engines.” In <i>2th Annual European Symposium on Algorithms</i>, 3221:3. Springer Nature, 2004. <a href=\"https://doi.org/10.1007/978-3-540-30140-0_2\">https://doi.org/10.1007/978-3-540-30140-0_2</a>."},"abstract":[{"lang":"eng","text":"Web search engines have emerged as one of the central applications on the internet. In fact, search has become one of the most important activities that people engage in on the Internet. Even beyond becoming the number one source of information, a growing number of businesses are depending on web search engines for customer acquisition. In this talk I will brief review the history of web search engines: The first generation of web search engines used text-only retrieval techniques. Google revolutionized the field by deploying the PageRank technology – an eigenvector-based analysis of the hyperlink structure- to analyze the web in order to produce relevant results. Moving forward, our goal is to achieve a better understanding of a page with a view towards producing even more relevant results.\r\n\r\nGoogle is powered by a large number of PCs. Using this infrastructure and striving to be as efficient as possible poses challenging systems problems but also various algorithmic challenges. I will discuss some of them in my talk."}],"doi":"10.1007/978-3-540-30140-0_2","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":[" 3540230254"]},"day":"01","extern":"1","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":3221},{"publisher":"Springer Nature","conference":{"end_date":"2000-09-08","location":"Saarbrücken, Germany","name":"ESA: European Symposium on Algorithms","start_date":"2000-09-05"},"page":"1–8","quality_controlled":"1","language":[{"iso":"eng"}],"oa_version":"None","publication_status":"published","article_processing_charge":"No","date_created":"2022-08-11T13:25:07Z","month":"09","title":"Web information retrieval - an algorithmic perspective","alternative_title":["LNCS"],"intvolume":"      1879","_id":"11802","publication":"8th Annual European Symposium on Algorithms","scopus_import":"1","author":[{"last_name":"Henzinger","first_name":"Monika H","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"}],"volume":1879,"extern":"1","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/3-540-45253-2_1","day":"01","publication_identifier":{"eisbn":["9783540452539"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783540410041"]},"abstract":[{"text":"In this paper we survey algorithmic aspects of Web information retrieval. As an example, we discuss ranking of search engine results using connectivity analysis.","lang":"eng"}],"date_updated":"2023-02-13T12:08:21Z","citation":{"apa":"Henzinger, M. H. (2000). Web information retrieval - an algorithmic perspective. In <i>8th Annual European Symposium on Algorithms</i> (Vol. 1879, pp. 1–8). Saarbrücken, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/3-540-45253-2_1\">https://doi.org/10.1007/3-540-45253-2_1</a>","ama":"Henzinger MH. Web information retrieval - an algorithmic perspective. In: <i>8th Annual European Symposium on Algorithms</i>. Vol 1879. Springer Nature; 2000:1–8. doi:<a href=\"https://doi.org/10.1007/3-540-45253-2_1\">10.1007/3-540-45253-2_1</a>","ieee":"M. H. Henzinger, “Web information retrieval - an algorithmic perspective,” in <i>8th Annual European Symposium on Algorithms</i>, Saarbrücken, Germany, 2000, vol. 1879, pp. 1–8.","chicago":"Henzinger, Monika H. “Web Information Retrieval - an Algorithmic Perspective.” In <i>8th Annual European Symposium on Algorithms</i>, 1879:1–8. Springer Nature, 2000. <a href=\"https://doi.org/10.1007/3-540-45253-2_1\">https://doi.org/10.1007/3-540-45253-2_1</a>.","mla":"Henzinger, Monika H. “Web Information Retrieval - an Algorithmic Perspective.” <i>8th Annual European Symposium on Algorithms</i>, vol. 1879, Springer Nature, 2000, pp. 1–8, doi:<a href=\"https://doi.org/10.1007/3-540-45253-2_1\">10.1007/3-540-45253-2_1</a>.","short":"M.H. Henzinger, in:, 8th Annual European Symposium on Algorithms, Springer Nature, 2000, pp. 1–8.","ista":"Henzinger MH. 2000. Web information retrieval - an algorithmic perspective. 8th Annual European Symposium on Algorithms. ESA: European Symposium on Algorithms, LNCS, vol. 1879, 1–8."},"year":"2000","date_published":"2000-09-01T00:00:00Z","type":"conference"},{"volume":1256,"extern":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","date_updated":"2023-02-14T07:49:03Z","citation":{"apa":"Henzinger, M. H., &#38; King, V. (1997). Maintaining minimum spanning trees in dynamic graphs. In <i>24th International Colloquium on Automata, Languages and Programming</i> (Vol. 1256, pp. 594–604). Bologna, Italy: Springer Nature. <a href=\"https://doi.org/10.1007/3-540-63165-8_214\">https://doi.org/10.1007/3-540-63165-8_214</a>","ama":"Henzinger MH, King V. Maintaining minimum spanning trees in dynamic graphs. In: <i>24th International Colloquium on Automata, Languages and Programming</i>. Vol 1256. Springer Nature; 1997:594–604. doi:<a href=\"https://doi.org/10.1007/3-540-63165-8_214\">10.1007/3-540-63165-8_214</a>","chicago":"Henzinger, Monika H, and Valerie King. “Maintaining Minimum Spanning Trees in Dynamic Graphs.” In <i>24th International Colloquium on Automata, Languages and Programming</i>, 1256:594–604. Springer Nature, 1997. <a href=\"https://doi.org/10.1007/3-540-63165-8_214\">https://doi.org/10.1007/3-540-63165-8_214</a>.","ieee":"M. H. Henzinger and V. King, “Maintaining minimum spanning trees in dynamic graphs,” in <i>24th International Colloquium on Automata, Languages and Programming</i>, Bologna, Italy, 1997, vol. 1256, pp. 594–604.","mla":"Henzinger, Monika H., and Valerie King. “Maintaining Minimum Spanning Trees in Dynamic Graphs.” <i>24th International Colloquium on Automata, Languages and Programming</i>, vol. 1256, Springer Nature, 1997, pp. 594–604, doi:<a href=\"https://doi.org/10.1007/3-540-63165-8_214\">10.1007/3-540-63165-8_214</a>.","short":"M.H. Henzinger, V. King, in:, 24th International Colloquium on Automata, Languages and Programming, Springer Nature, 1997, pp. 594–604.","ista":"Henzinger MH, King V. 1997. Maintaining minimum spanning trees in dynamic graphs. 24th International Colloquium on Automata, Languages and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LNCS, vol. 1256, 594–604."},"year":"1997","date_published":"1997-07-01T00:00:00Z","type":"conference","doi":"10.1007/3-540-63165-8_214","publication_identifier":{"eisbn":["9783540691945"],"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783540631651"]},"day":"01","abstract":[{"text":"We present the first fully dynamic algorithm for maintaining a minimum spanning tree in time o(√n) per operation. To be precise, the algorithm uses O(n 1/3 log n) amortized time per update operation. The algorithm is fairly simple and deterministic. An immediate consequence is the first fully dynamic deterministic algorithm for maintaining connectivity and, bipartiteness in amortized time O(n 1/3 log n) per update, with O(1) worst case time per query.","lang":"eng"}],"page":"594–604","quality_controlled":"1","language":[{"iso":"eng"}],"publisher":"Springer Nature","conference":{"end_date":"1997-07-11","location":"Bologna, Italy","name":"ICALP: International Colloquium on Automata, Languages, and Programming","start_date":"1997-07-07"},"_id":"11803","publication":"24th International Colloquium on Automata, Languages and Programming","scopus_import":"1","author":[{"full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"last_name":"King","first_name":"Valerie","full_name":"King, Valerie"}],"oa_version":"None","publication_status":"published","article_processing_charge":"No","date_created":"2022-08-11T13:35:06Z","alternative_title":["LNCS"],"month":"07","title":"Maintaining minimum spanning trees in dynamic graphs","intvolume":"      1256"},{"publisher":"Springer","editor":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Eduardo D","last_name":"Sontag","full_name":"Sontag, Eduardo D"}],"page":"IX, 619","quality_controlled":"1","series_title":"Lecture Notes in Computer Science","language":[{"iso":"eng"}],"oa_version":"None","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:45Z","alternative_title":["LNCS"],"title":"Hybrid Systems III: Verification and Control","month":"01","intvolume":"      1066","_id":"4612","volume":1066,"place":"Berlin ; Heidelberg","extern":"1","status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","doi":"10.1007/BFb0020931","publication_identifier":{"isbn":["978-3-540-61155-4"],"issn":["0302-9743"]},"day":"01","publist_id":"97","date_updated":"2021-12-22T13:57:33Z","year":"1996","citation":{"ista":"Alur R, Henzinger TA, Sontag ED eds. 1996. Hybrid Systems III: Verification and Control, Berlin ; Heidelberg: Springer, IX, 619p.","short":"R. Alur, T.A. Henzinger, E.D. Sontag, eds., Hybrid Systems III: Verification and Control, Springer, Berlin ; Heidelberg, 1996.","mla":"Alur, Rajeev, et al., editors. <i>Hybrid Systems III: Verification and Control</i>. Vol. 1066, Springer, 1996, doi:<a href=\"https://doi.org/10.1007/BFb0020931\">10.1007/BFb0020931</a>.","chicago":"Alur, Rajeev, Thomas A Henzinger, and Eduardo D Sontag, eds. <i>Hybrid Systems III: Verification and Control</i>. Vol. 1066. Lecture Notes in Computer Science. Berlin ; Heidelberg: Springer, 1996. <a href=\"https://doi.org/10.1007/BFb0020931\">https://doi.org/10.1007/BFb0020931</a>.","ieee":"R. Alur, T. A. Henzinger, and E. D. Sontag, Eds., <i>Hybrid Systems III: Verification and Control</i>, vol. 1066. Berlin ; Heidelberg: Springer, 1996.","apa":"Alur, R., Henzinger, T. A., &#38; Sontag, E. D. (Eds.). (1996). <i>Hybrid Systems III: Verification and Control</i> (Vol. 1066). Berlin ; Heidelberg: Springer. <a href=\"https://doi.org/10.1007/BFb0020931\">https://doi.org/10.1007/BFb0020931</a>","ama":"Alur R, Henzinger TA, Sontag ED, eds. <i>Hybrid Systems III: Verification and Control</i>. Vol 1066. Berlin ; Heidelberg: Springer; 1996. doi:<a href=\"https://doi.org/10.1007/BFb0020931\">10.1007/BFb0020931</a>"},"date_published":"1996-01-01T00:00:00Z","type":"book_editor"},{"type":"conference","date_published":"1996-07-01T00:00:00Z","citation":{"short":"M.H. Henzinger, J.A. Telle, in:, 5th Scandinavian Workshop on Algorithm Theory, Springer Nature, 1996, pp. 16–27.","mla":"Henzinger, Monika H., and Jan Arne Telle. “Faster Algorithms for the Nonemptiness of Streett Automata and for Communication Protocol Pruning.” <i>5th Scandinavian Workshop on Algorithm Theory</i>, vol. 1097, Springer Nature, 1996, pp. 16–27, doi:<a href=\"https://doi.org/10.1007/3-540-61422-2_117\">10.1007/3-540-61422-2_117</a>.","ista":"Henzinger MH, Telle JA. 1996. Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning. 5th Scandinavian Workshop on Algorithm Theory. SWAT: Scandinavian Workshop on Algorithm Theory, LNCS, vol. 1097, 16–27.","apa":"Henzinger, M. H., &#38; Telle, J. A. (1996). Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning. In <i>5th Scandinavian Workshop on Algorithm Theory</i> (Vol. 1097, pp. 16–27). Reykjavik, Iceland: Springer Nature. <a href=\"https://doi.org/10.1007/3-540-61422-2_117\">https://doi.org/10.1007/3-540-61422-2_117</a>","ama":"Henzinger MH, Telle JA. Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning. In: <i>5th Scandinavian Workshop on Algorithm Theory</i>. Vol 1097. Springer Nature; 1996:16–27. doi:<a href=\"https://doi.org/10.1007/3-540-61422-2_117\">10.1007/3-540-61422-2_117</a>","chicago":"Henzinger, Monika H, and Jan Arne Telle. “Faster Algorithms for the Nonemptiness of Streett Automata and for Communication Protocol Pruning.” In <i>5th Scandinavian Workshop on Algorithm Theory</i>, 1097:16–27. Springer Nature, 1996. <a href=\"https://doi.org/10.1007/3-540-61422-2_117\">https://doi.org/10.1007/3-540-61422-2_117</a>.","ieee":"M. H. Henzinger and J. A. Telle, “Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning,” in <i>5th Scandinavian Workshop on Algorithm Theory</i>, Reykjavik, Iceland, 1996, vol. 1097, pp. 16–27."},"year":"1996","date_updated":"2023-02-14T07:52:17Z","abstract":[{"lang":"eng","text":"This paper shows how a general technique, called lock-step search, used in dynamic graph algorithms, can be used to improve the running time of two problems arising in program verification and communication protocol design.\r\n(1)We consider the nonemptiness problem for Streett automata: We are given a directed graph G = (V, E) with n = ¦V¦ and m = ¦E¦, and a collection of pairs of subsets of vertices, called Streett pairs,〈L i , U i 〉, i = 1.k. The question is whether G has a cycle (not necessarily simple) which, for each 1 ≤ i ≤ k, if it contains a vertex from L i then it also contains a vertex of U i . Let b=Σ i=1..k |L i |+|U i |. The previously best algorithm takes time O((m + b) min{n, k}). We present an algorithm that takes time 𝑂(𝑚min{𝑚𝑙𝑜𝑔𝑛,‾‾‾‾‾‾√𝑘,𝑛}+𝑏𝑚𝑖𝑛{𝑙𝑜𝑔𝑛,𝑘}).\r\n(2)In communication protocol pruning we are given a directed graph G = (V, E) with l special vertices. The problem is to efficiently maintain the strongly-connected components of the special vertices on a restricted set of edge deletions. Let m i be the number of edges in the strongly connected component of the ith special vertex. The previously best algorithm repeatedly recomputes the strongly-connected components which leads to a running time of O(Σ i m 2i). We present an algorithm with time 𝑂(𝑙√∑𝑖𝑚1.5𝑖)."}],"publication_identifier":{"isbn":["9783540614227"],"eisbn":["9783540685296"],"issn":["0302-9743"],"eissn":["1611-3349"]},"day":"01","doi":"10.1007/3-540-61422-2_117","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","extern":"1","volume":1097,"author":[{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H","last_name":"Henzinger"},{"full_name":"Telle, Jan Arne","first_name":"Jan Arne","last_name":"Telle"}],"scopus_import":"1","publication":"5th Scandinavian Workshop on Algorithm Theory","_id":"11804","intvolume":"      1097","alternative_title":["LNCS"],"month":"07","title":"Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning","article_processing_charge":"No","date_created":"2022-08-11T13:42:42Z","oa_version":"None","publication_status":"published","language":[{"iso":"eng"}],"quality_controlled":"1","page":"16–27","conference":{"location":"Reykjavik, Iceland","end_date":"1996-07-05","name":"SWAT: Scandinavian Workshop on Algorithm Theory","start_date":"1996-07-03"},"publisher":"Springer Nature"},{"conference":{"location":"Paderborn, Germany","end_date":"1996-07-12","start_date":"1996-07-08","name":"ICALP: International Colloquium on Automata, Languages, and Programming"},"publisher":"Springer Nature","language":[{"iso":"eng"}],"quality_controlled":"1","page":"290-299","intvolume":"      1099","alternative_title":["LNCS"],"month":"07","title":"Improved sampling with applications to dynamic graph algorithms","article_processing_charge":"No","date_created":"2022-08-18T06:42:24Z","oa_version":"None","publication_status":"published","author":[{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","first_name":"Monika H"},{"first_name":"Mikkel","last_name":"Thorup","full_name":"Thorup, Mikkel"}],"scopus_import":"1","_id":"11910","publication":"23rd International Colloquium on Automata, Languages, and Programming","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","extern":"1","volume":1099,"abstract":[{"lang":"eng","text":"We state a new sampling lemma and use it to improve the running time of dynamic graph algorithms.\r\n\r\nFor the dynamic connectivity problem the previously best randomized algorithm takes expected time O(log3 n) per update, amortized over Ω(m) updates. Using the new sampling lemma, we improve its running time to O(log2 n). There exists a lower bound in the cell probe model for the time per operation of Ω(log n/ log log n) for this problem.\r\n\r\nSimilarly improved running times are achieved for 2-edge connectivity, k-weight minimum spanning tree, and bipartiteness."}],"day":"01","publication_identifier":{"eisbn":["9783540685807"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783540614401"]},"doi":"10.1007/3-540-61440-0_136","type":"conference","date_published":"1996-07-01T00:00:00Z","year":"1996","citation":{"chicago":"Henzinger, Monika H, and Mikkel Thorup. “Improved Sampling with Applications to Dynamic Graph Algorithms.” In <i>23rd International Colloquium on Automata, Languages, and Programming</i>, 1099:290–99. Springer Nature, 1996. <a href=\"https://doi.org/10.1007/3-540-61440-0_136\">https://doi.org/10.1007/3-540-61440-0_136</a>.","ieee":"M. H. Henzinger and M. Thorup, “Improved sampling with applications to dynamic graph algorithms,” in <i>23rd International Colloquium on Automata, Languages, and Programming</i>, Paderborn, Germany, 1996, vol. 1099, pp. 290–299.","ama":"Henzinger MH, Thorup M. Improved sampling with applications to dynamic graph algorithms. In: <i>23rd International Colloquium on Automata, Languages, and Programming</i>. Vol 1099. Springer Nature; 1996:290-299. doi:<a href=\"https://doi.org/10.1007/3-540-61440-0_136\">10.1007/3-540-61440-0_136</a>","apa":"Henzinger, M. H., &#38; Thorup, M. (1996). Improved sampling with applications to dynamic graph algorithms. In <i>23rd International Colloquium on Automata, Languages, and Programming</i> (Vol. 1099, pp. 290–299). Paderborn, Germany: Springer Nature. <a href=\"https://doi.org/10.1007/3-540-61440-0_136\">https://doi.org/10.1007/3-540-61440-0_136</a>","ista":"Henzinger MH, Thorup M. 1996. Improved sampling with applications to dynamic graph algorithms. 23rd International Colloquium on Automata, Languages, and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LNCS, vol. 1099, 290–299.","mla":"Henzinger, Monika H., and Mikkel Thorup. “Improved Sampling with Applications to Dynamic Graph Algorithms.” <i>23rd International Colloquium on Automata, Languages, and Programming</i>, vol. 1099, Springer Nature, 1996, pp. 290–99, doi:<a href=\"https://doi.org/10.1007/3-540-61440-0_136\">10.1007/3-540-61440-0_136</a>.","short":"M.H. Henzinger, M. Thorup, in:, 23rd International Colloquium on Automata, Languages, and Programming, Springer Nature, 1996, pp. 290–299."},"date_updated":"2023-02-14T07:57:14Z"},{"volume":979,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","extern":"1","year":"1995","citation":{"chicago":"Henzinger, Monika H, and Han Poutré. “Certificates and Fast Algorithms for Biconnectivity in Fully-Dynamic Graphs.” In <i>3rd Annual European Symposium on Algorithms</i>, 979:171–184. Springer Nature, 1995. <a href=\"https://doi.org/10.1007/3-540-60313-1_142\">https://doi.org/10.1007/3-540-60313-1_142</a>.","ieee":"M. H. Henzinger and H. Poutré, “Certificates and fast algorithms for biconnectivity in fully-dynamic graphs,” in <i>3rd Annual European Symposium on Algorithms</i>, Corfu, Greece, 1995, vol. 979, pp. 171–184.","apa":"Henzinger, M. H., &#38; Poutré, H. (1995). Certificates and fast algorithms for biconnectivity in fully-dynamic graphs. In <i>3rd Annual European Symposium on Algorithms</i> (Vol. 979, pp. 171–184). Corfu, Greece: Springer Nature. <a href=\"https://doi.org/10.1007/3-540-60313-1_142\">https://doi.org/10.1007/3-540-60313-1_142</a>","ama":"Henzinger MH, Poutré H. Certificates and fast algorithms for biconnectivity in fully-dynamic graphs. In: <i>3rd Annual European Symposium on Algorithms</i>. Vol 979. Springer Nature; 1995:171–184. doi:<a href=\"https://doi.org/10.1007/3-540-60313-1_142\">10.1007/3-540-60313-1_142</a>","ista":"Henzinger MH, Poutré H. 1995. Certificates and fast algorithms for biconnectivity in fully-dynamic graphs. 3rd Annual European Symposium on Algorithms. ESA: European Symposium on Algorithms, LNCS, vol. 979, 171–184.","short":"M.H. Henzinger, H. Poutré, in:, 3rd Annual European Symposium on Algorithms, Springer Nature, 1995, pp. 171–184.","mla":"Henzinger, Monika H., and Han Poutré. “Certificates and Fast Algorithms for Biconnectivity in Fully-Dynamic Graphs.” <i>3rd Annual European Symposium on Algorithms</i>, vol. 979, Springer Nature, 1995, pp. 171–184, doi:<a href=\"https://doi.org/10.1007/3-540-60313-1_142\">10.1007/3-540-60313-1_142</a>."},"date_updated":"2023-02-14T08:02:03Z","type":"conference","date_published":"1995-09-01T00:00:00Z","day":"01","publication_identifier":{"eisbn":["9783540449133"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783540603139"]},"doi":"10.1007/3-540-60313-1_142","abstract":[{"text":"In this paper, we present sparse certificates for biconnectivity together with algorithms for updating these certificates. We thus obtain fully-dynamic algorithms for biconnectivity in graphs that run in O(√n log n log⌈m/n⌉) amortized time per operation, where m is the number of edges and n is the number of nodes in the graph. This improves upon the results in [11], in which algorithms were presented running in O(√m) amortized time, and solves the open problem to find certificates to speed up biconnectivity, as stated in [2].","lang":"eng"}],"quality_controlled":"1","page":"171–184","language":[{"iso":"eng"}],"publisher":"Springer Nature","conference":{"location":"Corfu, Greece","end_date":"1995-09-27","name":"ESA: European Symposium on Algorithms","start_date":"1995-09-25"},"scopus_import":"1","publication":"3rd Annual European Symposium on Algorithms","_id":"11805","author":[{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H","last_name":"Henzinger"},{"full_name":"Poutré, Han","last_name":"Poutré","first_name":"Han"}],"date_created":"2022-08-11T14:09:52Z","article_processing_charge":"No","oa_version":"None","publication_status":"published","intvolume":"       979","alternative_title":["LNCS"],"title":"Certificates and fast algorithms for biconnectivity in fully-dynamic graphs","month":"09"},{"date_published":"1995-07-01T00:00:00Z","type":"conference","date_updated":"2023-02-14T08:09:08Z","year":"1995","citation":{"mla":"Henzinger, Monika H. “Approximating Minimum Cuts under Insertions.” <i>22nd International Colloquium on Automata, Languages and Programming</i>, vol. 944, Springer Nature, 1995, pp. 280–291, doi:<a href=\"https://doi.org/10.1007/3-540-60084-1_81\">10.1007/3-540-60084-1_81</a>.","short":"M.H. Henzinger, in:, 22nd International Colloquium on Automata, Languages and Programming, Springer Nature, 1995, pp. 280–291.","ista":"Henzinger MH. 1995. Approximating minimum cuts under insertions. 22nd International Colloquium on Automata, Languages and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LNCS, vol. 944, 280–291.","ama":"Henzinger MH. Approximating minimum cuts under insertions. In: <i>22nd International Colloquium on Automata, Languages and Programming</i>. Vol 944. Springer Nature; 1995:280–291. doi:<a href=\"https://doi.org/10.1007/3-540-60084-1_81\">10.1007/3-540-60084-1_81</a>","apa":"Henzinger, M. H. (1995). Approximating minimum cuts under insertions. In <i>22nd International Colloquium on Automata, Languages and Programming</i> (Vol. 944, pp. 280–291). Szeged, Hungary: Springer Nature. <a href=\"https://doi.org/10.1007/3-540-60084-1_81\">https://doi.org/10.1007/3-540-60084-1_81</a>","chicago":"Henzinger, Monika H. “Approximating Minimum Cuts under Insertions.” In <i>22nd International Colloquium on Automata, Languages and Programming</i>, 944:280–291. Springer Nature, 1995. <a href=\"https://doi.org/10.1007/3-540-60084-1_81\">https://doi.org/10.1007/3-540-60084-1_81</a>.","ieee":"M. H. Henzinger, “Approximating minimum cuts under insertions,” in <i>22nd International Colloquium on Automata, Languages and Programming</i>, Szeged, Hungary, 1995, vol. 944, pp. 280–291."},"abstract":[{"lang":"eng","text":"This paper presents insertions-only algorithms for maintaining the exact and approximate size of the minimum edge cut and the minimum vertex cut of a graph. The algorithms output the approximate or exact size k in time O(1) or O(log n) and a cut of size k in time linear in its size. The amortized time per insertion is O(1/ε 2) for a (2+ε)-approximation, O((log λ)((log n)/ε)2) for a (1+ε)-approximation, and O(λ log n) for the exact size of the minimum edge cut, where n is the number of nodes in the graph, λ is the size of the minimum cut and ε>0. The (2+ε)-approximation algorithm and the exact algorithm are deterministic, the (1+ε)-approximation algorithm is randomized. The algorithms are optimal in the sense that the time needed for m insertions matches the time needed by the best static algorithm on a m-edge graph. We also present a static 2-approximation algorithm for the size κ of the minimum vertex cut in a graph, which takes time O(n 2 min(√n,κ)). This is a factor of κ faster than the best algorithm for computing the exact size, which takes time O(κ 2 n 2 +κ 3 n 1.5). We give an insertionsonly algorithm for maintaining a (2+ε)-approximation of the minimum vertex cut with amortized insertion time O(n(logκk)/ε)."}],"doi":"10.1007/3-540-60084-1_81","day":"01","publication_identifier":{"isbn":["9783540494256"],"eisbn":["9783540600848"],"eissn":["1611-3349"],"issn":["0302-9743"]},"extern":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","volume":944,"author":[{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","first_name":"Monika H"}],"_id":"11806","publication":"22nd International Colloquium on Automata, Languages and Programming","scopus_import":"1","title":"Approximating minimum cuts under insertions","month":"07","alternative_title":["LNCS"],"intvolume":"       944","oa_version":"None","publication_status":"published","article_processing_charge":"No","date_created":"2022-08-11T14:17:33Z","language":[{"iso":"eng"}],"page":"280–291","quality_controlled":"1","conference":{"name":"ICALP: International Colloquium on Automata, Languages, and Programming","start_date":"1995-07-10","location":"Szeged, Hungary","end_date":"1995-07-14"},"publisher":"Springer Nature"}]