[{"ddc":["004"],"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"ec_funded":1,"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under grant 2014/15/D/ST6/04543.","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_number":"24","file_date_updated":"2018-12-12T10:17:31Z","date_published":"2016-08-01T00:00:00Z","day":"01","article_processing_charge":"No","pubrep_id":"795","file":[{"date_created":"2018-12-12T10:17:31Z","file_id":"5286","creator":"system","file_name":"IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf","content_type":"application/pdf","date_updated":"2018-12-12T10:17:31Z","access_level":"open_access","file_size":564560,"relation":"main_file"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","citation":{"ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average automata of bounded width,” presented at the MFCS: Mathematical Foundations of Computer Science, Krakow; Poland, 2016, vol. 58.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata of bounded width. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 58, 24.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted limit-average automata of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Nested weighted limit-average automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations of Computer Science, Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">https://doi.org/10.4230/LIPIcs.MFCS.2016.24</a>","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Limit-Average Automata of Bounded Width</i>. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.24\">10.4230/LIPIcs.MFCS.2016.24</a>."},"intvolume":"        58","doi":"10.4230/LIPIcs.MFCS.2016.24","volume":58,"has_accepted_license":"1","type":"conference","quality_controlled":"1","month":"08","publist_id":"6286","alternative_title":["LIPIcs"],"date_updated":"2025-07-10T11:50:02Z","conference":{"location":"Krakow; Poland","start_date":"2016-08-22","end_date":"2016-08-26","name":"MFCS: Mathematical Foundations of Computer Science"},"scopus_import":"1","oa_version":"Published Version","publication_status":"published","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"year":"2016","abstract":[{"text":" While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.","lang":"eng"}],"date_created":"2018-12-11T11:50:05Z","oa":1,"title":"Nested weighted limit-average automata of bounded width","status":"public","_id":"1090"},{"status":"public","_id":"1093","title":"Linear distances between Markov chains","oa":1,"date_created":"2018-12-11T11:50:06Z","abstract":[{"text":"We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. ","lang":"eng"}],"oa_version":"Published Version","scopus_import":1,"conference":{"location":"Quebec City; Canada","start_date":"2016-08-23","name":"CONCUR: Concurrency Theory","end_date":"2016-08-26"},"date_updated":"2026-04-15T10:02:12Z","year":"2016","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"publication_status":"published","type":"conference","has_accepted_license":"1","volume":59,"doi":"10.4230/LIPIcs.CONCUR.2016.20","alternative_title":["LIPIcs"],"publist_id":"6283","month":"08","quality_controlled":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"},{"_id":"CaGu"}],"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF) under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award), by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced Postdoc. Mobility Fellowship – grant number P300P2_161067.","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1155"}]},"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky"},{"last_name":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87"}],"ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"ddc":["004"],"intvolume":"        59","citation":{"apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Linear distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>","mla":"Daca, Przemyslaw, et al. <i>Linear Distances between Markov Chains</i>. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City; Canada, 2016, vol. 59.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.20\">10.4230/LIPIcs.CONCUR.2016.20</a>"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","pubrep_id":"794","file":[{"access_level":"open_access","file_size":501827,"content_type":"application/pdf","date_updated":"2018-12-12T10:11:39Z","relation":"main_file","date_created":"2018-12-12T10:11:39Z","file_name":"IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf","creator":"system","file_id":"4895"}],"day":"01","date_published":"2016-08-01T00:00:00Z","article_number":"20","file_date_updated":"2018-12-12T10:11:39Z"},{"date_created":"2018-12-11T11:50:06Z","abstract":[{"lang":"eng","text":"Immunogold labeling of freeze-fracture replicas has recently been used for high-resolution visualization of protein localization in electron microscopy. This method has higher labeling efficiency than conventional immunogold methods for membrane molecules allowing precise quantitative measurements. However, one of the limitations of freeze-fracture replica immunolabeling is difficulty in keeping structural orientation and identifying labeled profiles in complex tissues like brain. The difficulty is partly due to fragmentation of freeze-fracture replica preparations during labeling procedures and limited morphological clues on the replica surface. To overcome these issues, we introduce here a grid-glued replica method combined with SEM observation. This method allows histological staining before dissolving the tissue and easy handling of replicas during immunogold labeling, and keeps the whole replica surface intact without fragmentation. The procedure described here is also useful for matched double-replica analysis allowing further identification of labeled profiles in corresponding P-face and E-face."}],"title":"Immunogold protein localization on grid-glued freeze-fracture replicas","_id":"1094","status":"public","page":"203 - 216","publication_status":"published","project":[{"name":"Localization of ion channels and receptors by two and three-dimensional immunoelectron microscopic approaches","grant_number":"604102","_id":"25CD3DD2-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"year":"2016","date_updated":"2025-04-15T07:12:21Z","oa_version":"None","publist_id":"6281","month":"08","quality_controlled":"1","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"]},"alternative_title":["Methods in Molecular Biology"],"volume":1474,"doi":"10.1007/978-1-4939-6352-2_12","type":"book_chapter","article_processing_charge":"No","day":"12","date_published":"2016-08-12T00:00:00Z","citation":{"ieee":"H. Harada and R. Shigemoto, “Immunogold protein localization on grid-glued freeze-fracture replicas,” in <i>High-Resolution Imaging of Cellular Proteins</i>, vol. 1474, Springer, 2016, pp. 203–216.","chicago":"Harada, Harumi, and Ryuichi Shigemoto. “Immunogold Protein Localization on Grid-Glued Freeze-Fracture Replicas.” In <i>High-Resolution Imaging of Cellular Proteins</i>, 1474:203–16. Springer, 2016. <a href=\"https://doi.org/10.1007/978-1-4939-6352-2_12\">https://doi.org/10.1007/978-1-4939-6352-2_12</a>.","ista":"Harada H, Shigemoto R. 2016.Immunogold protein localization on grid-glued freeze-fracture replicas. In: High-Resolution Imaging of Cellular Proteins. Methods in Molecular Biology, vol. 1474, 203–216.","ama":"Harada H, Shigemoto R. Immunogold protein localization on grid-glued freeze-fracture replicas. In: <i>High-Resolution Imaging of Cellular Proteins</i>. Vol 1474. Springer; 2016:203-216. doi:<a href=\"https://doi.org/10.1007/978-1-4939-6352-2_12\">10.1007/978-1-4939-6352-2_12</a>","short":"H. Harada, R. Shigemoto, in:, High-Resolution Imaging of Cellular Proteins, Springer, 2016, pp. 203–216.","apa":"Harada, H., &#38; Shigemoto, R. (2016). Immunogold protein localization on grid-glued freeze-fracture replicas. In <i>High-Resolution Imaging of Cellular Proteins</i> (Vol. 1474, pp. 203–216). Springer. <a href=\"https://doi.org/10.1007/978-1-4939-6352-2_12\">https://doi.org/10.1007/978-1-4939-6352-2_12</a>","mla":"Harada, Harumi, and Ryuichi Shigemoto. “Immunogold Protein Localization on Grid-Glued Freeze-Fracture Replicas.” <i>High-Resolution Imaging of Cellular Proteins</i>, vol. 1474, Springer, 2016, pp. 203–16, doi:<a href=\"https://doi.org/10.1007/978-1-4939-6352-2_12\">10.1007/978-1-4939-6352-2_12</a>."},"publisher":"Springer","intvolume":"      1474","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication":"High-Resolution Imaging of Cellular Proteins","language":[{"iso":"eng"}],"acknowledged_ssus":[{"_id":"EM-Fac"}],"author":[{"full_name":"Harada, Harumi","last_name":"Harada","first_name":"Harumi","id":"2E55CDF2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7429-7896"},{"id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8761-9444","full_name":"Shigemoto, Ryuichi","last_name":"Shigemoto","first_name":"Ryuichi"}],"ec_funded":1,"department":[{"_id":"RySh"}],"acknowledgement":"We thank Prof. Elek Molnár for providing us a pan-AMPAR anti-body used in Fig.2 and Dr. Ludek Lovicar for technical assistance in scanning electron microscope imaging. This work was supported by the European Union (HBP—Project Ref. 604102). "},{"intvolume":"        59","citation":{"mla":"Haas, Andreas, et al. “Local Linearizability for Concurrent Container-Type Data Structures.” <i>Leibniz International Proceedings in Informatics</i>, vol. 59, 6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">10.4230/LIPIcs.CONCUR.2016.6</a>.","apa":"Haas, A., Henzinger, T. A., Holzer, A., Kirsch, C., Lippautz, M., Payer, H., … Veith, H. (2016). Local linearizability for concurrent container-type data structures. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 59). Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.6</a>","short":"A. Haas, T.A. Henzinger, A. Holzer, C. Kirsch, M. Lippautz, H. Payer, A. Sezgin, A. Sokolova, H. Veith, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ama":"Haas A, Henzinger TA, Holzer A, et al. Local linearizability for concurrent container-type data structures. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">10.4230/LIPIcs.CONCUR.2016.6</a>","ista":"Haas A, Henzinger TA, Holzer A, Kirsch C, Lippautz M, Payer H, Sezgin A, Sokolova A, Veith H. 2016. Local linearizability for concurrent container-type data structures. Leibniz International Proceedings in Informatics. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 6.","chicago":"Haas, Andreas, Thomas A Henzinger, Andreas Holzer, Christoph Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. “Local Linearizability for Concurrent Container-Type Data Structures.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.6\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.6</a>.","ieee":"A. Haas <i>et al.</i>, “Local linearizability for concurrent container-type data structures,” in <i>Leibniz International Proceedings in Informatics</i>, Quebec City; Canada, 2016, vol. 59."},"file":[{"date_created":"2018-12-12T10:10:10Z","creator":"system","file_name":"IST-2017-793-v1+1_LIPIcs-CONCUR-2016-6.pdf","file_id":"4795","file_size":589747,"access_level":"open_access","content_type":"application/pdf","date_updated":"2018-12-12T10:10:10Z","relation":"main_file"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","pubrep_id":"793","day":"01","date_published":"2016-08-01T00:00:00Z","article_number":"6","file_date_updated":"2018-12-12T10:10:10Z","department":[{"_id":"ToHe"}],"acknowledgement":"This work has been supported by the National Research Network RiSE on Rigorous Systems Engineering\r\n(Austrian Science Fund (FWF): S11402-N23, S11403-N23, S11404-N23, S11411-N23), a Google\r\nPhD Fellowship, an Erwin Schrödinger Fellowship (Austrian Science Fund (FWF): J3696-N26), EPSRC\r\ngrants EP/H005633/1 and EP/K008528/1, the Vienna Science and Technology Fund (WWTF) trough\r\ngrant PROSEED, the European Research Council (ERC) under grant 267989 (QUAREM) and by the\r\nAustrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","ec_funded":1,"author":[{"full_name":"Haas, Andreas","first_name":"Andreas","last_name":"Haas"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"last_name":"Holzer","first_name":"Andreas","full_name":"Holzer, Andreas"},{"first_name":"Christoph","last_name":"Kirsch","full_name":"Kirsch, Christoph"},{"full_name":"Lippautz, Michael","last_name":"Lippautz","first_name":"Michael"},{"full_name":"Payer, Hannes","first_name":"Hannes","last_name":"Payer"},{"full_name":"Sezgin, Ali","first_name":"Ali","last_name":"Sezgin","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Sokolova, Ana","first_name":"Ana","last_name":"Sokolova"},{"full_name":"Veith, Helmut","first_name":"Helmut","last_name":"Veith"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publication":"Leibniz International Proceedings in Informatics","ddc":["004"],"language":[{"iso":"eng"}],"alternative_title":["LIPIcs"],"publist_id":"6280","month":"08","quality_controlled":"1","type":"conference","has_accepted_license":"1","volume":59,"doi":"10.4230/LIPIcs.CONCUR.2016.6","year":"2016","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"publication_status":"published","scopus_import":1,"oa_version":"Published Version","conference":{"end_date":"2016-08-26","name":"CONCUR: Concurrency Theory","start_date":"2016-08-23","location":"Quebec City; Canada"},"date_updated":"2025-04-15T06:25:58Z","_id":"1095","status":"public","title":"Local linearizability for concurrent container-type data structures","date_created":"2018-12-11T11:50:07Z","oa":1,"abstract":[{"lang":"eng","text":" The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations. "}]},{"year":"2016","page":"493 - 506","publication_status":"published","scopus_import":"1","oa_version":"None","date_updated":"2026-04-08T13:55:28Z","_id":"1096","status":"public","title":"Actin rings of power","date_created":"2018-12-11T11:50:07Z","isi":1,"issue":"6","intvolume":"        37","publisher":"Cell Press","citation":{"ama":"Schwayer C, Sikora MK, Slovakova J, Kardos R, Heisenberg C-PJ. Actin rings of power. <i>Developmental Cell</i>. 2016;37(6):493-506. doi:<a href=\"https://doi.org/10.1016/j.devcel.2016.05.024\">10.1016/j.devcel.2016.05.024</a>","ieee":"C. Schwayer, M. K. Sikora, J. Slovakova, R. Kardos, and C.-P. J. Heisenberg, “Actin rings of power,” <i>Developmental Cell</i>, vol. 37, no. 6. Cell Press, pp. 493–506, 2016.","ista":"Schwayer C, Sikora MK, Slovakova J, Kardos R, Heisenberg C-PJ. 2016. Actin rings of power. Developmental Cell. 37(6), 493–506.","chicago":"Schwayer, Cornelia, Mateusz K Sikora, Jana Slovakova, Roland Kardos, and Carl-Philipp J Heisenberg. “Actin Rings of Power.” <i>Developmental Cell</i>. Cell Press, 2016. <a href=\"https://doi.org/10.1016/j.devcel.2016.05.024\">https://doi.org/10.1016/j.devcel.2016.05.024</a>.","short":"C. Schwayer, M.K. Sikora, J. Slovakova, R. Kardos, C.-P.J. Heisenberg, Developmental Cell 37 (2016) 493–506.","mla":"Schwayer, Cornelia, et al. “Actin Rings of Power.” <i>Developmental Cell</i>, vol. 37, no. 6, Cell Press, 2016, pp. 493–506, doi:<a href=\"https://doi.org/10.1016/j.devcel.2016.05.024\">10.1016/j.devcel.2016.05.024</a>.","apa":"Schwayer, C., Sikora, M. K., Slovakova, J., Kardos, R., &#38; Heisenberg, C.-P. J. (2016). Actin rings of power. <i>Developmental Cell</i>. Cell Press. <a href=\"https://doi.org/10.1016/j.devcel.2016.05.024\">https://doi.org/10.1016/j.devcel.2016.05.024</a>"},"date_published":"2016-06-20T00:00:00Z","day":"20","article_processing_charge":"No","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"7186"}]},"department":[{"_id":"CaHe"}],"author":[{"last_name":"Schwayer","first_name":"Cornelia","full_name":"Schwayer, Cornelia","orcid":"0000-0001-5130-2226","id":"3436488C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Sikora, Mateusz K","first_name":"Mateusz K","last_name":"Sikora","id":"2F74BCDE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Slovakova, Jana","last_name":"Slovakova","first_name":"Jana","id":"30F3F2F0-F248-11E8-B48F-1D18A9856A87"},{"id":"4039350E-F248-11E8-B48F-1D18A9856A87","full_name":"Kardos, Roland","last_name":"Kardos","first_name":"Roland"},{"orcid":"0000-0002-0912-4566","id":"39427864-F248-11E8-B48F-1D18A9856A87","last_name":"Heisenberg","first_name":"Carl-Philipp J","full_name":"Heisenberg, Carl-Philipp J"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication":"Developmental Cell","language":[{"iso":"eng"}],"quality_controlled":"1","publist_id":"6279","month":"06","type":"journal_article","external_id":{"isi":["000378204200005"]},"doi":"10.1016/j.devcel.2016.05.024","volume":37},{"publication_status":"published","year":"2016","project":[{"_id":"25082902-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"645599","name":"Soft-bodied intelligence for Manipulation"}],"conference":{"end_date":"2016-12-08","name":"SIGGRAPH Asia: Conference and Exhibition on Computer Graphics and Interactive Techniques in Asia","start_date":"2016-12-05","location":"Macao, China"},"date_updated":"2025-09-22T14:17:29Z","oa_version":"Submitted Version","scopus_import":"1","abstract":[{"lang":"eng","text":"We present an interactive system for computational design, optimization, and fabrication of multicopters. Our computational approach allows non-experts to design, explore, and evaluate a wide range of different multicopters. We provide users with an intuitive interface for assembling a multicopter from a collection of components (e.g., propellers, motors, and carbon fiber rods). Our algorithm interactively optimizes shape and controller parameters of the current design to ensure its proper operation. In addition, we allow incorporating a variety of other metrics (such as payload, battery usage, size, and cost) into the design process and exploring tradeoffs between them. We show the efficacy of our method and system by designing, optimizing, fabricating, and operating multicopters with complex geometries and propeller configurations. We also demonstrate the ability of our optimization algorithm to improve the multicopter performance under different metrics."}],"oa":1,"date_created":"2018-12-11T11:50:07Z","status":"public","_id":"1097","title":"Computational multicopter design","isi":1,"day":"01","date_published":"2016-11-01T00:00:00Z","article_processing_charge":"No","article_number":"227","file_date_updated":"2018-12-12T10:17:42Z","issue":"6","intvolume":"        35","publisher":"ACM","pubrep_id":"759","file":[{"file_name":"IST-2017-759-v1+1_copter.pdf","creator":"system","file_id":"5298","date_created":"2018-12-12T10:17:42Z","relation":"main_file","file_size":33114420,"access_level":"open_access","content_type":"application/pdf","date_updated":"2018-12-12T10:17:42Z"}],"citation":{"chicago":"Du, Tao, Adriana Schulz, Bo Zhu, Bernd Bickel, and Wojciech Matusik. “Computational Multicopter Design,” Vol. 35. ACM, 2016. <a href=\"https://doi.org/10.1145/2980179.2982427\">https://doi.org/10.1145/2980179.2982427</a>.","ieee":"T. Du, A. Schulz, B. Zhu, B. Bickel, and W. Matusik, “Computational multicopter design,” presented at the SIGGRAPH Asia: Conference and Exhibition on Computer Graphics and Interactive Techniques in Asia, Macao, China, 2016, vol. 35, no. 6.","ista":"Du T, Schulz A, Zhu B, Bickel B, Matusik W. 2016. Computational multicopter design. SIGGRAPH Asia: Conference and Exhibition on Computer Graphics and Interactive Techniques in Asia, ACM Transactions on Graphics, vol. 35, 227.","ama":"Du T, Schulz A, Zhu B, Bickel B, Matusik W. Computational multicopter design. In: Vol 35. ACM; 2016. doi:<a href=\"https://doi.org/10.1145/2980179.2982427\">10.1145/2980179.2982427</a>","short":"T. Du, A. Schulz, B. Zhu, B. Bickel, W. Matusik, in:, ACM, 2016.","apa":"Du, T., Schulz, A., Zhu, B., Bickel, B., &#38; Matusik, W. (2016). Computational multicopter design (Vol. 35). Presented at the SIGGRAPH Asia: Conference and Exhibition on Computer Graphics and Interactive Techniques in Asia, Macao, China: ACM. <a href=\"https://doi.org/10.1145/2980179.2982427\">https://doi.org/10.1145/2980179.2982427</a>","mla":"Du, Tao, et al. <i>Computational Multicopter Design</i>. Vol. 35, no. 6, 227, ACM, 2016, doi:<a href=\"https://doi.org/10.1145/2980179.2982427\">10.1145/2980179.2982427</a>."},"language":[{"iso":"eng"}],"ddc":["006"],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","acknowledgement":"We thank Nobuyuki Umetani for his insightful suggestions in our discussions. We thank Alan Schultz and his colleagues at NRL for building the hexacopter and for the valuable discussions. We thank Randall Davis, Boris Katz, and Howard Shrobe at MIT for their advice. We are grateful to Nick Bandiera for preprocessing mechanical parts and providing 3D printing technical support; Charles Blouin from RCBenchmark for dynamometer hardware support; Brian Saavedra for the composition UI; Yingzhe Yuan for data acquisition and video recording in the experiments; Michael Foshey and David Kim for their comments on the draft of the paper. \r\n\r\n\r\nThis work was partially supported by Air Force Research Laboratory’s sponsorship of Julia: A Fresh Approach to Technical Computing and Data Processing (Sponsor Award ID FA8750-15-2- 0272, MIT Award ID 024831-00003), and NSF Expedition project (Sponsor Award ID CCF-1138967, MIT Award ID 020610-00002). The views expressed herein are not endorsed by the sponsors. This project has also received funding from the European Union’s Horizon 2020 research and innovation program under grant agreement No 645599. ","department":[{"_id":"BeBi"}],"ec_funded":1,"author":[{"full_name":"Du, Tao","last_name":"Du","first_name":"Tao"},{"last_name":"Schulz","first_name":"Adriana","full_name":"Schulz, Adriana"},{"full_name":"Zhu, Bo","last_name":"Zhu","first_name":"Bo"},{"orcid":"0000-0001-6511-9385","id":"49876194-F248-11E8-B48F-1D18A9856A87","last_name":"Bickel","first_name":"Bernd","full_name":"Bickel, Bernd"},{"full_name":"Matusik, Wojciech","first_name":"Wojciech","last_name":"Matusik"}],"quality_controlled":"1","publist_id":"6278","month":"11","alternative_title":["ACM Transactions on Graphics"],"doi":"10.1145/2980179.2982427","volume":35,"has_accepted_license":"1","type":"conference","external_id":{"isi":["000388446200069"]}},{"publist_id":"6277","month":"12","quality_controlled":"1","alternative_title":["Advances in Neural Information Processing Systems"],"has_accepted_license":"1","volume":29,"type":"conference","file_date_updated":"2018-12-12T10:12:43Z","article_processing_charge":"No","date_published":"2016-12-01T00:00:00Z","day":"01","citation":{"short":"A. Pentina, R. Urner, in:, Neural Information Processing Systems Foundation, 2016, pp. 3619–3627.","ama":"Pentina A, Urner R. Lifelong learning with weighted majority votes. In: Vol 29. Neural Information Processing Systems Foundation; 2016:3619-3627.","ista":"Pentina A, Urner R. 2016. Lifelong learning with weighted majority votes. NIPS: Neural Information Processing Systems, Advances in Neural Information Processing Systems, vol. 29, 3619–3627.","ieee":"A. Pentina and R. Urner, “Lifelong learning with weighted majority votes,” presented at the NIPS: Neural Information Processing Systems, Barcelona, Spain, 2016, vol. 29, pp. 3619–3627.","chicago":"Pentina, Anastasia, and Ruth Urner. “Lifelong Learning with Weighted Majority Votes,” 29:3619–27. Neural Information Processing Systems Foundation, 2016.","mla":"Pentina, Anastasia, and Ruth Urner. <i>Lifelong Learning with Weighted Majority Votes</i>. Vol. 29, Neural Information Processing Systems Foundation, 2016, pp. 3619–27.","apa":"Pentina, A., &#38; Urner, R. (2016). Lifelong learning with weighted majority votes (Vol. 29, pp. 3619–3627). Presented at the NIPS: Neural Information Processing Systems, Barcelona, Spain: Neural Information Processing Systems Foundation."},"publisher":"Neural Information Processing Systems Foundation","file":[{"relation":"main_file","date_updated":"2018-12-12T10:12:42Z","content_type":"application/pdf","access_level":"open_access","file_size":237111,"file_name":"IST-2017-775-v1+1_main.pdf","creator":"system","file_id":"4961","date_created":"2018-12-12T10:12:42Z"},{"date_created":"2018-12-12T10:12:43Z","file_id":"4962","creator":"system","file_name":"IST-2017-775-v1+2_supplementary.pdf","file_size":185818,"access_level":"open_access","date_updated":"2018-12-12T10:12:43Z","content_type":"application/pdf","relation":"main_file"}],"pubrep_id":"775","intvolume":"        29","language":[{"iso":"eng"}],"ddc":["006"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"42E87FC6-F248-11E8-B48F-1D18A9856A87","first_name":"Anastasia","last_name":"Pentina","full_name":"Pentina, Anastasia"},{"first_name":"Ruth","last_name":"Urner","full_name":"Urner, Ruth"}],"ec_funded":1,"department":[{"_id":"ChLa"}],"acknowledgement":"This work was in parts funded by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2013)/ERC grant agreement no 308036.\r\n\r\n","oa":1,"date_created":"2018-12-11T11:50:08Z","abstract":[{"lang":"eng","text":"Better understanding of the potential benefits of information transfer and representation learning is an important step towards the goal of building intelligent systems that are able to persist in the world and learn over time. In this work, we consider a setting where the learner encounters a stream of tasks but is able to retain only limited information from each encountered task, such as a learned predictor. In contrast to most previous works analyzing this scenario, we do not make any distributional assumptions on the task generating process. Instead, we formulate a complexity measure that captures the diversity of the observed tasks. We provide a lifelong learning algorithm with error guarantees for every observed task (rather than on average). We show sample complexity reductions in comparison to solving every task in isolation in terms of our task complexity measure. Further, our algorithmic framework can naturally be viewed as learning a representation from encountered tasks with a neural network."}],"title":"Lifelong learning with weighted majority votes","status":"public","_id":"1098","page":"3619-3627","publication_status":"published","project":[{"name":"Lifelong Learning of Visual Scene Understanding","grant_number":"308036","call_identifier":"FP7","_id":"2532554C-B435-11E9-9278-68D0E5697425"}],"year":"2016","date_updated":"2025-06-03T11:35:58Z","conference":{"name":"NIPS: Neural Information Processing Systems","end_date":"2016-12-10","location":"Barcelona, Spain","start_date":"2016-12-05"},"oa_version":"Published Version","scopus_import":"1"},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ddc":["000","005"],"language":[{"iso":"eng"}],"department":[{"_id":"BeBi"}],"acknowledgement":"The armadillo, bunny and dragon models are courtesy of the Stanford  3D  Scanning  Repository.   The  bimba,  fertility  and  elephant models are courtesy of the AIM@SHAPE Shape Repository.  \r\nThis project has received funding from the European Union’s Horizon 2020  research  and  innovation  programme  under  grant  agreement\r\nNo. 645599.","author":[{"first_name":"Luigi","last_name":"Malomo","full_name":"Malomo, Luigi"},{"full_name":"Pietroni, Nico","last_name":"Pietroni","first_name":"Nico"},{"id":"49876194-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-6511-9385","full_name":"Bickel, Bernd","first_name":"Bernd","last_name":"Bickel"},{"last_name":"Cignoni","first_name":"Paolo","full_name":"Cignoni, Paolo"}],"ec_funded":1,"article_processing_charge":"No","date_published":"2016-11-01T00:00:00Z","day":"01","article_number":"223","file_date_updated":"2018-12-12T10:12:01Z","intvolume":"        35","issue":"6","citation":{"short":"L. Malomo, N. Pietroni, B. Bickel, P. Cignoni, in:, ACM, 2016.","ama":"Malomo L, Pietroni N, Bickel B, Cignoni P. FlexMolds: Automatic design of flexible shells for molding. In: Vol 35. ACM; 2016. doi:<a href=\"https://doi.org/10.1145/2980179.2982397\">10.1145/2980179.2982397</a>","chicago":"Malomo, Luigi, Nico Pietroni, Bernd Bickel, and Paolo Cignoni. “FlexMolds: Automatic Design of Flexible Shells for Molding,” Vol. 35. ACM, 2016. <a href=\"https://doi.org/10.1145/2980179.2982397\">https://doi.org/10.1145/2980179.2982397</a>.","ista":"Malomo L, Pietroni N, Bickel B, Cignoni P. 2016. FlexMolds: Automatic design of flexible shells for molding. SIGGRAPH Asia: Conference and Exhibition on Computer Graphics and Interactive Techniques in Asia, ACM Transactions on Graphics, vol. 35, 223.","ieee":"L. Malomo, N. Pietroni, B. Bickel, and P. Cignoni, “FlexMolds: Automatic design of flexible shells for molding,” presented at the SIGGRAPH Asia: Conference and Exhibition on Computer Graphics and Interactive Techniques in Asia, Macao, China, 2016, vol. 35, no. 6.","mla":"Malomo, Luigi, et al. <i>FlexMolds: Automatic Design of Flexible Shells for Molding</i>. Vol. 35, no. 6, 223, ACM, 2016, doi:<a href=\"https://doi.org/10.1145/2980179.2982397\">10.1145/2980179.2982397</a>.","apa":"Malomo, L., Pietroni, N., Bickel, B., &#38; Cignoni, P. (2016). FlexMolds: Automatic design of flexible shells for molding (Vol. 35). Presented at the SIGGRAPH Asia: Conference and Exhibition on Computer Graphics and Interactive Techniques in Asia, Macao, China: ACM. <a href=\"https://doi.org/10.1145/2980179.2982397\">https://doi.org/10.1145/2980179.2982397</a>"},"file":[{"relation":"main_file","access_level":"open_access","file_size":11122029,"date_updated":"2018-12-12T10:12:01Z","content_type":"application/pdf","file_name":"IST-2017-760-v1+1_flexmolds.pdf","creator":"system","file_id":"4918","date_created":"2018-12-12T10:12:01Z"}],"pubrep_id":"760","publisher":"ACM","has_accepted_license":"1","volume":35,"doi":"10.1145/2980179.2982397","external_id":{"isi":["000388446200065"]},"type":"conference","publist_id":"6276","month":"11","quality_controlled":"1","alternative_title":["ACM Transactions on Graphics"],"conference":{"name":"SIGGRAPH Asia: Conference and Exhibition on Computer Graphics and Interactive Techniques in Asia","end_date":"2016-12-08","start_date":"2016-12-05","location":"Macao, China"},"date_updated":"2025-09-22T14:16:02Z","oa_version":"Submitted Version","scopus_import":"1","publication_status":"published","year":"2016","project":[{"call_identifier":"H2020","_id":"25082902-B435-11E9-9278-68D0E5697425","name":"Soft-bodied intelligence for Manipulation","grant_number":"645599"}],"isi":1,"date_created":"2018-12-11T11:50:08Z","oa":1,"abstract":[{"text":"We present FlexMolds, a novel computational approach to automatically design flexible, reusable molds that, once 3D printed, allow us to physically fabricate, by means of liquid casting, multiple copies of complex shapes with rich surface details and complex topology. The approach to design such flexible molds is based on a greedy bottom-up search of possible cuts over an object, evaluating for each possible cut the feasibility of the resulting mold. We use a dynamic simulation approach to evaluate candidate molds, providing a heuristic to generate forces that are able to open, detach, and remove a complex mold from the object it surrounds. We have tested the approach with a number of objects with nontrivial shapes and topologies.","lang":"eng"}],"_id":"1099","status":"public","title":"FlexMolds: Automatic design of flexible shells for molding"},{"month":"11","publist_id":"6274","quality_controlled":"1","external_id":{"isi":["000388914800003"]},"type":"journal_article","volume":1,"doi":"10.1021/acssensors.6b00576","intvolume":"         1","issue":"11","citation":{"mla":"Mitchell, Joshua, et al. “Rangefinder: A Semisynthetic FRET Sensor Design Algorithm.” <i>ACS SENSORS</i>, vol. 1, no. 11, American Chemical Society, 2016, pp. 1286–90, doi:<a href=\"https://doi.org/10.1021/acssensors.6b00576\">10.1021/acssensors.6b00576</a>.","apa":"Mitchell, J., Whitfield, J., Zhang, W., Henneberger, C., Janovjak, H. L., O’Mara, M., &#38; Jackson, C. (2016). Rangefinder: A semisynthetic FRET sensor design algorithm. <i>ACS SENSORS</i>. American Chemical Society. <a href=\"https://doi.org/10.1021/acssensors.6b00576\">https://doi.org/10.1021/acssensors.6b00576</a>","short":"J. Mitchell, J. Whitfield, W. Zhang, C. Henneberger, H.L. Janovjak, M. O’Mara, C. Jackson, ACS SENSORS 1 (2016) 1286–1290.","ama":"Mitchell J, Whitfield J, Zhang W, et al. Rangefinder: A semisynthetic FRET sensor design algorithm. <i>ACS SENSORS</i>. 2016;1(11):1286-1290. doi:<a href=\"https://doi.org/10.1021/acssensors.6b00576\">10.1021/acssensors.6b00576</a>","ista":"Mitchell J, Whitfield J, Zhang W, Henneberger C, Janovjak HL, O’Mara M, Jackson C. 2016. Rangefinder: A semisynthetic FRET sensor design algorithm. ACS SENSORS. 1(11), 1286–1290.","ieee":"J. Mitchell <i>et al.</i>, “Rangefinder: A semisynthetic FRET sensor design algorithm,” <i>ACS SENSORS</i>, vol. 1, no. 11. American Chemical Society, pp. 1286–1290, 2016.","chicago":"Mitchell, Joshua, Jason Whitfield, William Zhang, Christian Henneberger, Harald L Janovjak, Megan O’Mara, and Colin Jackson. “Rangefinder: A Semisynthetic FRET Sensor Design Algorithm.” <i>ACS SENSORS</i>. American Chemical Society, 2016. <a href=\"https://doi.org/10.1021/acssensors.6b00576\">https://doi.org/10.1021/acssensors.6b00576</a>."},"publisher":"American Chemical Society","article_processing_charge":"No","day":"10","date_published":"2016-11-10T00:00:00Z","department":[{"_id":"HaJa"}],"acknowledgement":"J.A.M., J.H.W., and W.H.Z. were supported by Australian\r\nPostgraduate Awards (APA), AS Sargeson Supplementary\r\nscholarships, and RSC supplementary scholarships. C.J.J.\r\nacknowledges support from a Human Frontiers in Science\r\nYoung Investigator Award and a Discovery Project and Future\r\nFellowship from the Australian Research Council. M.L.O. is\r\nsupported by an Australian Research Council Discovery Project\r\n(DP130102153) and the Merit Allocation Scheme of the\r\nNational Computational Infrastructure.","author":[{"last_name":"Mitchell","first_name":"Joshua","full_name":"Mitchell, Joshua"},{"last_name":"Whitfield","first_name":"Jason","full_name":"Whitfield, Jason"},{"full_name":"Zhang, William","last_name":"Zhang","first_name":"William"},{"full_name":"Henneberger, Christian","last_name":"Henneberger","first_name":"Christian"},{"first_name":"Harald L","last_name":"Janovjak","full_name":"Janovjak, Harald L","orcid":"0000-0002-8023-9315","id":"33BA6C30-F248-11E8-B48F-1D18A9856A87"},{"last_name":"O'Mara","first_name":"Megan","full_name":"O'Mara, Megan"},{"first_name":"Colin","last_name":"Jackson","full_name":"Jackson, Colin"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"publication":"ACS SENSORS","status":"public","_id":"1101","title":"Rangefinder: A semisynthetic FRET sensor design algorithm","date_created":"2018-12-11T11:50:09Z","abstract":[{"text":"Optical sensors based on the phenomenon of Förster resonance energy transfer (FRET) are powerful tools that have advanced the study of small molecules in biological systems. However, sensor construction is not trivial and often requires multiple rounds of engineering or an ability to screen large numbers of variants. A method that would allow the accurate rational design of FRET sensors would expedite the production of biologically useful sensors. Here, we present Rangefinder, a computational algorithm that allows rapid in silico screening of dye attachment sites in a ligand-binding protein for the conjugation of a dye molecule to act as a Förster acceptor for a fused fluorescent protein. We present three ratiometric fluorescent sensors designed with Rangefinder, including a maltose sensor with a dynamic range of &gt;300% and the first sensors for the most abundant sialic acid in human cells, N-acetylneuraminic acid. Provided a ligand-binding protein exists, it is our expectation that this model will facilitate the design of an optical sensor for any small molecule of interest.","lang":"eng"}],"isi":1,"year":"2016","page":"1286 - 1290","publication_status":"published","scopus_import":"1","oa_version":"None","date_updated":"2025-09-22T14:14:58Z"},{"date_created":"2018-12-11T11:50:09Z","oa":1,"abstract":[{"text":"Weakly-supervised object localization methods tend to fail for object classes that consistently co-occur with the same background elements, e.g. trains on tracks. We propose a method to overcome these failures by adding a very small amount of model-specific additional annotation. The main idea is to cluster a deep network\\'s mid-level representations and assign object or distractor labels to each cluster. Experiments show substantially improved localization results on the challenging ILSVC2014 dataset for bounding box detection and the PASCAL VOC2012 dataset for semantic segmentation.","lang":"eng"}],"_id":"1102","status":"public","title":"Improving weakly-supervised object localization by micro-annotation","page":"92.1-92.12","publication_status":"published","year":"2016","project":[{"_id":"2532554C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"308036","name":"Lifelong Learning of Visual Scene Understanding"}],"conference":{"name":"BMVC: British Machine Vision Conference","end_date":"2016-09-22","location":"York, United Kingdom","start_date":"2016-09-19"},"date_updated":"2026-06-18T10:46:30Z","oa_version":"Published Version","scopus_import":"1","month":"09","publist_id":"6273","quality_controlled":"1","volume":"2016-September","doi":"10.5244/C.30.92","type":"conference","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"http://www.bmva.org/bmvc/2016/papers/paper092/paper092.pdf"}],"day":"01","date_published":"2016-09-01T00:00:00Z","citation":{"mla":"Kolesnikov, Alexander, and Christoph Lampert. “Improving Weakly-Supervised Object Localization by Micro-Annotation.” <i>Proceedings of the British Machine Vision Conference 2016</i>, vol. 2016–September, BMVA Press, 2016, p. 92.1-92.12, doi:<a href=\"https://doi.org/10.5244/C.30.92\">10.5244/C.30.92</a>.","apa":"Kolesnikov, A., &#38; Lampert, C. (2016). Improving weakly-supervised object localization by micro-annotation. In <i>Proceedings of the British Machine Vision Conference 2016</i> (Vol. 2016–September, p. 92.1-92.12). York, United Kingdom: BMVA Press. <a href=\"https://doi.org/10.5244/C.30.92\">https://doi.org/10.5244/C.30.92</a>","ama":"Kolesnikov A, Lampert C. Improving weakly-supervised object localization by micro-annotation. In: <i>Proceedings of the British Machine Vision Conference 2016</i>. Vol 2016-September. BMVA Press; 2016:92.1-92.12. doi:<a href=\"https://doi.org/10.5244/C.30.92\">10.5244/C.30.92</a>","ista":"Kolesnikov A, Lampert C. 2016. Improving weakly-supervised object localization by micro-annotation. Proceedings of the British Machine Vision Conference 2016. BMVC: British Machine Vision Conference vol. 2016–September, 92.1-92.12.","chicago":"Kolesnikov, Alexander, and Christoph Lampert. “Improving Weakly-Supervised Object Localization by Micro-Annotation.” In <i>Proceedings of the British Machine Vision Conference 2016</i>, 2016–September:92.1-92.12. BMVA Press, 2016. <a href=\"https://doi.org/10.5244/C.30.92\">https://doi.org/10.5244/C.30.92</a>.","ieee":"A. Kolesnikov and C. Lampert, “Improving weakly-supervised object localization by micro-annotation,” in <i>Proceedings of the British Machine Vision Conference 2016</i>, York, United Kingdom, 2016, vol. 2016–September, p. 92.1-92.12.","short":"A. Kolesnikov, C. Lampert, in:, Proceedings of the British Machine Vision Conference 2016, BMVA Press, 2016, p. 92.1-92.12."},"publisher":"BMVA Press","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"Proceedings of the British Machine Vision Conference 2016","ddc":["000"],"department":[{"_id":"ChLa"}],"acknowledgement":"This work was funded in parts by the European Research Council\r\nunder the European Union’s Seventh Framework Programme (FP7/2007-2013)/ERC grant\r\nagreement no 308036. We gratefully acknowledge the support of NVIDIA Corporation with\r\nthe donation of the GPUs used for this research.","author":[{"id":"2D157DB6-F248-11E8-B48F-1D18A9856A87","first_name":"Alexander","last_name":"Kolesnikov","full_name":"Kolesnikov, Alexander"},{"full_name":"Lampert, Christoph","last_name":"Lampert","first_name":"Christoph","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8622-7887"}],"ec_funded":1},{"status":"public","_id":"1103","title":"Parallel reachability analysis for hybrid systems","abstract":[{"lang":"eng","text":"We propose two parallel state-space-exploration algorithms for hybrid automaton (HA), with the goal of enhancing performance on multi-core shared-memory systems. The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN model checker, when traversing the discrete modes of the HA, and enhances it with a parallel exploration of the continuous states within each mode. We show that this simple-minded extension of PBFS does not provide the desired load balancing in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS), which uses a cheap precomputation of the cost associated with the post operations (both continuous and discrete) in order to improve load balancing. We illustrate the TP-BFS and the cost precomputation of the post operators on a support-function-based algorithm for state-space exploration. The performance comparison of the two algorithms shows that, in general, TP-BFS provides a better utilization/load-balancing of the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect to SpaceEx LGG scenario. In order to make the comparison fair, we employed an equal number of post operations in both tools. To the best of our knowledge, this paper represents the first attempt to provide parallel, reachability-analysis algorithms for HA."}],"date_created":"2018-12-11T11:50:09Z","oa":1,"year":"2016","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"publication_status":"published","oa_version":"Preprint","scopus_import":"1","conference":{"end_date":"2016-11-20","name":"MEMOCODE: Conference on Formal Methods and Models for System Design","start_date":"2016-11-18","location":"Kanpur, India "},"date_updated":"2025-06-04T11:52:29Z","quality_controlled":"1","publist_id":"6272","month":"12","type":"conference","external_id":{"arxiv":["1606.05473"]},"doi":"10.1109/MEMCOD.2016.7797741","publisher":"IEEE","citation":{"short":"A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, R. Ray, in:, IEEE, 2016.","ieee":"A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, and R. Ray, “Parallel reachability analysis for hybrid systems,” presented at the MEMOCODE: Conference on Formal Methods and Models for System Design, Kanpur, India , 2016.","chicago":"Gurung, Amit, Arup Deka, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, and Rajarshi Ray. “Parallel Reachability Analysis for Hybrid Systems.” IEEE, 2016. <a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">https://doi.org/10.1109/MEMCOD.2016.7797741</a>.","ista":"Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. 2016. Parallel reachability analysis for hybrid systems. MEMOCODE: Conference on Formal Methods and Models for System Design, 7797741.","ama":"Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. Parallel reachability analysis for hybrid systems. In: IEEE; 2016. doi:<a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">10.1109/MEMCOD.2016.7797741</a>","apa":"Gurung, A., Deka, A., Bartocci, E., Bogomolov, S., Grosu, R., &#38; Ray, R. (2016). Parallel reachability analysis for hybrid systems. Presented at the MEMOCODE: Conference on Formal Methods and Models for System Design, Kanpur, India : IEEE. <a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">https://doi.org/10.1109/MEMCOD.2016.7797741</a>","mla":"Gurung, Amit, et al. <i>Parallel Reachability Analysis for Hybrid Systems</i>. 7797741, IEEE, 2016, doi:<a href=\"https://doi.org/10.1109/MEMCOD.2016.7797741\">10.1109/MEMCOD.2016.7797741</a>."},"date_published":"2016-12-27T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1606.05473","open_access":"1"}],"day":"27","article_processing_charge":"No","article_number":"7797741","acknowledgement":"This work was supported in part by DST-SERB, GoI under Project No. YSS/2014/000623 and by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","department":[{"_id":"ToHe"}],"ec_funded":1,"author":[{"full_name":"Gurung, Amit","last_name":"Gurung","first_name":"Amit"},{"full_name":"Deka, Arup","first_name":"Arup","last_name":"Deka"},{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Grosu, Radu","last_name":"Grosu","first_name":"Radu"},{"first_name":"Rajarshi","last_name":"Ray","full_name":"Ray, Rajarshi"}],"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1},{"oa_version":"None","scopus_import":"1","conference":{"name":"NIPS: Neural Information Processing Systems","end_date":"2016-12-10","location":"Barcelona; Spain","start_date":"2016-12-05"},"date_updated":"2025-06-03T11:36:49Z","year":"2016","project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"publication_status":"published","page":"3610-3618","corr_author":"1","_id":"1105","status":"public","title":"Estimating nonlinear neural response functions using GP priors and Kronecker methods","oa":1,"date_created":"2018-12-11T11:50:10Z","abstract":[{"lang":"eng","text":"Jointly characterizing neural responses in terms of several external variables promises novel insights into circuit function, but remains computationally prohibitive in practice. Here we use gaussian process (GP) priors and exploit recent advances in fast GP inference and learning based on Kronecker methods, to efficiently estimate multidimensional nonlinear tuning functions. Our estimator require considerably less data than traditional methods and further provides principled uncertainty estimates. We apply these tools to hippocampal recordings during open field exploration and use them to characterize the joint dependence of CA1 responses on the position of the animal and several other variables, including the animal\\'s speed, direction of motion, and network oscillations.Our results provide an unprecedentedly detailed quantification of the tuning of hippocampal neurons. The model\\'s generality suggests that our approach can be used to estimate neural response properties in other brain regions."}],"department":[{"_id":"GaTk"}],"acknowledgement":"We  thank  Jozsef  Csicsvari  for  kindly  sharing  the  CA1  data.\r\nThis work was supported by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme(FP7/2007-2013) under REA grant agreement no. 291734.","author":[{"id":"3933349E-F248-11E8-B48F-1D18A9856A87","full_name":"Savin, Cristina","first_name":"Cristina","last_name":"Savin"},{"orcid":"0000-0002-6699-1455","id":"3D494DCA-F248-11E8-B48F-1D18A9856A87","last_name":"Tkacik","first_name":"Gasper","full_name":"Tkacik, Gasper"}],"ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"intvolume":"        29","citation":{"ama":"Savin C, Tkačik G. Estimating nonlinear neural response functions using GP priors and Kronecker methods. In: Vol 29. Neural Information Processing Systems Foundation; 2016:3610-3618.","ieee":"C. Savin and G. Tkačik, “Estimating nonlinear neural response functions using GP priors and Kronecker methods,” presented at the NIPS: Neural Information Processing Systems, Barcelona; Spain, 2016, vol. 29, pp. 3610–3618.","ista":"Savin C, Tkačik G. 2016. Estimating nonlinear neural response functions using GP priors and Kronecker methods. NIPS: Neural Information Processing Systems, Advances in Neural Information Processing Systems, vol. 29, 3610–3618.","chicago":"Savin, Cristina, and Gašper Tkačik. “Estimating Nonlinear Neural Response Functions Using GP Priors and Kronecker Methods,” 29:3610–18. Neural Information Processing Systems Foundation, 2016.","short":"C. Savin, G. Tkačik, in:, Neural Information Processing Systems Foundation, 2016, pp. 3610–3618.","mla":"Savin, Cristina, and Gašper Tkačik. <i>Estimating Nonlinear Neural Response Functions Using GP Priors and Kronecker Methods</i>. Vol. 29, Neural Information Processing Systems Foundation, 2016, pp. 3610–18.","apa":"Savin, C., &#38; Tkačik, G. (2016). Estimating nonlinear neural response functions using GP priors and Kronecker methods (Vol. 29, pp. 3610–3618). Presented at the NIPS: Neural Information Processing Systems, Barcelona; Spain: Neural Information Processing Systems Foundation."},"publisher":"Neural Information Processing Systems Foundation","article_processing_charge":"No","date_published":"2016-12-01T00:00:00Z","main_file_link":[{"open_access":"1","url":"http://papers.nips.cc/paper/6153-estimating-nonlinear-neural-response-functions-using-gp-priors-and-kronecker-methods"}],"day":"01","type":"conference","volume":29,"alternative_title":["Advances in Neural Information Processing Systems"],"month":"12","publist_id":"6265","quality_controlled":"1"},{"month":"12","publist_id":"6251","quality_controlled":"1","external_id":{"arxiv":["1601.07261"]},"type":"conference","doi":"10.1364/CLEO_SI.2016.SF2G.3","citation":{"apa":"Rueda, A., Sedlmeir, F., Collodo, M., Vogl, U., Stiller, B., Schunk, G., … Schwefel, H. (2016). Efficient single sideband microwave to optical conversion using a LiNbO₃ WGM-resonator. Presented at the CLEO: Conference on Lasers and Electro Optics, San Jose, CA, USA: IEEE. <a href=\"https://doi.org/10.1364/CLEO_SI.2016.SF2G.3\">https://doi.org/10.1364/CLEO_SI.2016.SF2G.3</a>","mla":"Rueda, Alfredo, et al. <i>Efficient Single Sideband Microwave to Optical Conversion Using a LiNbO₃ WGM-Resonator</i>. 7788479, IEEE, 2016, doi:<a href=\"https://doi.org/10.1364/CLEO_SI.2016.SF2G.3\">10.1364/CLEO_SI.2016.SF2G.3</a>.","short":"A. Rueda, F. Sedlmeir, M. Collodo, U. Vogl, B. Stiller, G. Schunk, D. Strekalov, C. Marquardt, J.M. Fink, O. Painter, G. Leuchs, H. Schwefel, in:, IEEE, 2016.","ieee":"A. Rueda <i>et al.</i>, “Efficient single sideband microwave to optical conversion using a LiNbO₃ WGM-resonator,” presented at the CLEO: Conference on Lasers and Electro Optics, San Jose, CA, USA, 2016.","chicago":"Rueda, Alfredo, Florian Sedlmeir, Michele Collodo, Ulrich Vogl, Birgit Stiller, Georg Schunk, Dimitry Strekalov, et al. “Efficient Single Sideband Microwave to Optical Conversion Using a LiNbO₃ WGM-Resonator.” IEEE, 2016. <a href=\"https://doi.org/10.1364/CLEO_SI.2016.SF2G.3\">https://doi.org/10.1364/CLEO_SI.2016.SF2G.3</a>.","ista":"Rueda A, Sedlmeir F, Collodo M, Vogl U, Stiller B, Schunk G, Strekalov D, Marquardt C, Fink JM, Painter O, Leuchs G, Schwefel H. 2016. Efficient single sideband microwave to optical conversion using a LiNbO₃ WGM-resonator. CLEO: Conference on Lasers and Electro Optics, 7788479.","ama":"Rueda A, Sedlmeir F, Collodo M, et al. Efficient single sideband microwave to optical conversion using a LiNbO₃ WGM-resonator. In: IEEE; 2016. doi:<a href=\"https://doi.org/10.1364/CLEO_SI.2016.SF2G.3\">10.1364/CLEO_SI.2016.SF2G.3</a>"},"publisher":"IEEE","article_number":"7788479","article_processing_charge":"No","day":"16","date_published":"2016-12-16T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1601.07261","open_access":"1"}],"author":[{"full_name":"Rueda, Alfredo","last_name":"Rueda","first_name":"Alfredo"},{"full_name":"Sedlmeir, Florian","first_name":"Florian","last_name":"Sedlmeir"},{"full_name":"Collodo, Michele","last_name":"Collodo","first_name":"Michele"},{"last_name":"Vogl","first_name":"Ulrich","full_name":"Vogl, Ulrich"},{"full_name":"Stiller, Birgit","first_name":"Birgit","last_name":"Stiller"},{"full_name":"Schunk, Georg","last_name":"Schunk","first_name":"Georg"},{"first_name":"Dimitry","last_name":"Strekalov","full_name":"Strekalov, Dimitry"},{"full_name":"Marquardt, Christoph","first_name":"Christoph","last_name":"Marquardt"},{"orcid":"0000-0001-8112-028X","id":"4B591CBA-F248-11E8-B48F-1D18A9856A87","last_name":"Fink","first_name":"Johannes M","full_name":"Fink, Johannes M"},{"full_name":"Painter, Oskar","last_name":"Painter","first_name":"Oskar"},{"last_name":"Leuchs","first_name":"Gerd","full_name":"Leuchs, Gerd"},{"full_name":"Schwefel, Harald","first_name":"Harald","last_name":"Schwefel"}],"department":[{"_id":"JoFi"}],"related_material":{"link":[{"url":"http://ieeexplore.ieee.org/document/7788479/","relation":"other"}]},"arxiv":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"title":"Efficient single sideband microwave to optical conversion using a LiNbO₃ WGM-resonator","_id":"1115","status":"public","oa":1,"date_created":"2018-12-11T11:50:14Z","abstract":[{"lang":"eng","text":"We present a coherent microwave to telecom signal converter based on the electro-optical effect using a crystalline WGM-resonator coupled to a 3D microwave cavity, achieving high photon conversion efficiency of 0.1% with MHz bandwidth."}],"year":"2016","publication_status":"published","oa_version":"Preprint","scopus_import":"1","date_updated":"2025-04-22T13:41:54Z","conference":{"location":"San Jose, CA, USA","start_date":"2016-06-05","name":"CLEO: Conference on Lasers and Electro Optics","end_date":"2016-06-10"}},{"day":"07","main_file_link":[{"open_access":"1","url":"http://thorstent.github.io/theses/phd_thorsten_tarrach.pdf"}],"date_published":"2016-07-07T00:00:00Z","article_processing_charge":"No","file_date_updated":"2021-11-17T13:46:55Z","file":[{"content_type":"application/pdf","date_updated":"2021-02-22T11:39:32Z","success":1,"file_size":1523935,"access_level":"open_access","relation":"main_file","checksum":"319a506831650327e85376db41fc1094","date_created":"2021-02-22T11:39:32Z","file_id":"9179","creator":"dernst","file_name":"2016_Tarrach_Thesis.pdf"},{"date_created":"2021-11-16T14:14:38Z","creator":"cchlebak","file_name":"2016_Tarrach_Thesispdfa.pdf","file_id":"10296","file_size":1306068,"access_level":"closed","date_updated":"2021-11-17T13:46:55Z","content_type":"application/pdf","checksum":"39efcd789f0ad859ff15652cb7afc412","relation":"main_file"}],"publisher":"Institute of Science and Technology Austria","citation":{"mla":"Tarrach, Thorsten. <i>Automatic Synthesis of Synchronisation Primitives for Concurrent Programs</i>. Institute of Science and Technology Austria, 2016, doi:<a href=\"https://doi.org/10.15479/at:ista:1130\">10.15479/at:ista:1130</a>.","apa":"Tarrach, T. (2016). <i>Automatic synthesis of synchronisation primitives for concurrent programs</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:1130\">https://doi.org/10.15479/at:ista:1130</a>","short":"T. Tarrach, Automatic Synthesis of Synchronisation Primitives for Concurrent Programs, Institute of Science and Technology Austria, 2016.","ama":"Tarrach T. Automatic synthesis of synchronisation primitives for concurrent programs. 2016. doi:<a href=\"https://doi.org/10.15479/at:ista:1130\">10.15479/at:ista:1130</a>","ista":"Tarrach T. 2016. Automatic synthesis of synchronisation primitives for concurrent programs. Institute of Science and Technology Austria.","ieee":"T. Tarrach, “Automatic synthesis of synchronisation primitives for concurrent programs,” Institute of Science and Technology Austria, 2016.","chicago":"Tarrach, Thorsten. “Automatic Synthesis of Synchronisation Primitives for Concurrent Programs.” Institute of Science and Technology Austria, 2016. <a href=\"https://doi.org/10.15479/at:ista:1130\">https://doi.org/10.15479/at:ista:1130</a>."},"ddc":["000"],"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"2218"},{"id":"2445","status":"public","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"1729"}]},"department":[{"_id":"ToHe"},{"_id":"GradSch"}],"author":[{"id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4409-8487","full_name":"Tarrach, Thorsten","last_name":"Tarrach","first_name":"Thorsten"}],"ec_funded":1,"OA_place":"publisher","publist_id":"6230","month":"07","alternative_title":["ISTA Thesis"],"publication_identifier":{"issn":["2663-337X"]},"doi":"10.15479/at:ista:1130","has_accepted_license":"1","type":"dissertation","publication_status":"published","page":"151","year":"2016","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"date_updated":"2026-04-09T10:54:01Z","oa_version":"Published Version","abstract":[{"lang":"eng","text":"In this thesis we present a computer-aided programming approach to concurrency. Our approach helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t. a specification. We consider both user-provided explicit specifications in the form of assertion\r\nstatements in the code as well as an implicit specification. The implicit specification is inferred from the non-preemptive behaviour. Let us consider sequences of calls that the program makes to an external interface. The implicit specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We consider several semantics-preserving fixes that go beyond atomic sections typically explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers and wait-signal statements and last, but not least reorder independent statements. The latter may be useful if a thread is released to early, e.g., before some initialisation is completed. We guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective function. We dub our solution trace-based synchronisation synthesis and it is loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger the specification violation. Synchronisation may be placed immediately (greedy approach) or delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach we construct a set of global constraints over synchronisation placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronisation placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronisation solution. We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver\r\nbenchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs. For the experiments with an explicit specification we added assertions that would detect the bugs in the experiments. Device drivers lend themselves to implicit specification, where the device and the operating system are the external interfaces. Our experiments demonstrate that our synthesis method is precise and efficient. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronisation placements are produced for our experiments, favouring e.g. a minimal number of synchronisation operations or maximum concurrency."}],"oa":1,"date_created":"2018-12-11T11:50:19Z","_id":"1130","status":"public","title":"Automatic synthesis of synchronisation primitives for concurrent programs","corr_author":"1","supervisor":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"degree_awarded":"PhD"},{"type":"conference","doi":"10.1109/CCA.2016.7587948","status":"public","_id":"1134","title":"Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP","abstract":[{"text":"Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification. © 2016 IEEE.","lang":"eng"}],"quality_controlled":"1","publist_id":"6224","date_created":"2018-12-11T11:50:20Z","month":"10","department":[{"_id":"ToHe"}],"author":[{"first_name":"Parasara","last_name":"Duggirala","full_name":"Duggirala, Parasara"},{"first_name":"Chuchu","last_name":"Fan","full_name":"Fan, Chuchu"},{"full_name":"Potok, Matthew","last_name":"Potok","first_name":"Matthew"},{"first_name":"Bolun","last_name":"Qi","full_name":"Qi, Bolun"},{"first_name":"Sayan","last_name":"Mitra","full_name":"Mitra, Sayan"},{"last_name":"Viswanathan","first_name":"Mahesh","full_name":"Viswanathan, Mahesh"},{"last_name":"Bak","first_name":"Stanley","full_name":"Bak, Stanley"},{"orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"full_name":"Johnson, Taylor","first_name":"Taylor","last_name":"Johnson"},{"first_name":"Luan","last_name":"Nguyen","full_name":"Nguyen, Luan"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling"},{"full_name":"Sogokon, Andrew","last_name":"Sogokon","first_name":"Andrew"},{"full_name":"Tran, Hoang","last_name":"Tran","first_name":"Hoang"},{"first_name":"Weiming","last_name":"Xiang","full_name":"Xiang, Weiming"}],"oa_version":"None","scopus_import":1,"conference":{"name":"CCA: Control Applications ","end_date":"2016-09-22","start_date":"2016-09-19","location":"Buenos Aires, Argentina "},"language":[{"iso":"eng"}],"publication":"2016 IEEE Conference on Control Applications","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:48:32Z","year":"2016","publisher":"IEEE","citation":{"apa":"Duggirala, P., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., … Xiang, W. (2016). Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In <i>2016 IEEE Conference on Control Applications</i>. Buenos Aires, Argentina : IEEE. <a href=\"https://doi.org/10.1109/CCA.2016.7587948\">https://doi.org/10.1109/CCA.2016.7587948</a>","mla":"Duggirala, Parasara, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” <i>2016 IEEE Conference on Control Applications</i>, 7587948, IEEE, 2016, doi:<a href=\"https://doi.org/10.1109/CCA.2016.7587948\">10.1109/CCA.2016.7587948</a>.","ieee":"P. Duggirala <i>et al.</i>, “Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP,” in <i>2016 IEEE Conference on Control Applications</i>, Buenos Aires, Argentina , 2016.","chicago":"Duggirala, Parasara, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” In <i>2016 IEEE Conference on Control Applications</i>. IEEE, 2016. <a href=\"https://doi.org/10.1109/CCA.2016.7587948\">https://doi.org/10.1109/CCA.2016.7587948</a>.","ista":"Duggirala P, Fan C, Potok M, Qi B, Mitra S, Viswanathan M, Bak S, Bogomolov S, Johnson T, Nguyen L, Schilling C, Sogokon A, Tran H, Xiang W. 2016. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. 2016 IEEE Conference on Control Applications. CCA: Control Applications , 7587948.","ama":"Duggirala P, Fan C, Potok M, et al. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In: <i>2016 IEEE Conference on Control Applications</i>. IEEE; 2016. doi:<a href=\"https://doi.org/10.1109/CCA.2016.7587948\">10.1109/CCA.2016.7587948</a>","short":"P. Duggirala, C. Fan, M. Potok, B. Qi, S. Mitra, M. Viswanathan, S. Bak, S. Bogomolov, T. Johnson, L. Nguyen, C. Schilling, A. Sogokon, H. Tran, W. Xiang, in:, 2016 IEEE Conference on Control Applications, IEEE, 2016."},"day":"10","date_published":"2016-10-10T00:00:00Z","article_number":"7587948","publication_status":"published"},{"has_accepted_license":"1","doi":"10.1145/2968478.2968499","external_id":{"isi":["000414220100026"]},"type":"conference","publist_id":"6223","month":"10","quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ddc":["000"],"language":[{"iso":"eng"}],"publication":"Proceedings of the 13th International Conference on Embedded Software ","department":[{"_id":"ToHe"}],"author":[{"full_name":"Avni, Guy","last_name":"Avni","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"first_name":"Shibashis","last_name":"Guha","full_name":"Guha, Shibashis"},{"last_name":"Rodríguez Navas","first_name":"Guillermo","full_name":"Rodríguez Navas, Guillermo"}],"ec_funded":1,"article_processing_charge":"No","day":"01","date_published":"2016-10-01T00:00:00Z","file_date_updated":"2018-12-12T10:09:31Z","article_number":"26","citation":{"apa":"Avni, G., Guha, S., &#38; Rodríguez Navas, G. (2016). Synthesizing time triggered schedules for switched networks with faulty links. In <i>Proceedings of the 13th International Conference on Embedded Software </i>. Pittsburgh, PA, USA: ACM. <a href=\"https://doi.org/10.1145/2968478.2968499\">https://doi.org/10.1145/2968478.2968499</a>","mla":"Avni, Guy, et al. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” <i>Proceedings of the 13th International Conference on Embedded Software </i>, 26, ACM, 2016, doi:<a href=\"https://doi.org/10.1145/2968478.2968499\">10.1145/2968478.2968499</a>.","short":"G. Avni, S. Guha, G. Rodríguez Navas, in:, Proceedings of the 13th International Conference on Embedded Software , ACM, 2016.","chicago":"Avni, Guy, Shibashis Guha, and Guillermo Rodríguez Navas. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” In <i>Proceedings of the 13th International Conference on Embedded Software </i>. ACM, 2016. <a href=\"https://doi.org/10.1145/2968478.2968499\">https://doi.org/10.1145/2968478.2968499</a>.","ieee":"G. Avni, S. Guha, and G. Rodríguez Navas, “Synthesizing time triggered schedules for switched networks with faulty links,” in <i>Proceedings of the 13th International Conference on Embedded Software </i>, Pittsburgh, PA, USA, 2016.","ista":"Avni G, Guha S, Rodríguez Navas G. 2016. Synthesizing time triggered schedules for switched networks with faulty links. Proceedings of the 13th International Conference on Embedded Software . EMSOFT: Embedded Software , 26.","ama":"Avni G, Guha S, Rodríguez Navas G. Synthesizing time triggered schedules for switched networks with faulty links. In: <i>Proceedings of the 13th International Conference on Embedded Software </i>. ACM; 2016. doi:<a href=\"https://doi.org/10.1145/2968478.2968499\">10.1145/2968478.2968499</a>"},"publisher":"ACM","file":[{"relation":"main_file","content_type":"application/pdf","date_updated":"2018-12-12T10:09:31Z","file_size":279240,"access_level":"open_access","file_id":"4755","creator":"system","file_name":"IST-2016-644-v1+1_emsoft-no-format.pdf","date_created":"2018-12-12T10:09:31Z"}],"pubrep_id":"644","isi":1,"oa":1,"date_created":"2018-12-11T11:50:20Z","abstract":[{"text":"Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a pk; qresistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least no matter what sequence of at most k links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not pk; q-resistant. We illustrate the applicability of our approach using an SMT-based implementation. © 2016 ACM.","lang":"eng"}],"status":"public","_id":"1135","title":"Synthesizing time triggered schedules for switched networks with faulty links","conference":{"start_date":"2016-10-01","location":"Pittsburgh, PA, USA","end_date":"2016-10-07","name":"EMSOFT: Embedded Software "},"date_updated":"2025-09-22T14:14:05Z","oa_version":"Submitted Version","scopus_import":"1","publication_status":"published","year":"2016","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}]},{"project":[{"grant_number":"638176","name":"Big Splash: Efficient Simulation of Natural Phenomena at Extremely Large Scales","_id":"2533E772-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"year":"2016","publication_status":"published","scopus_import":"1","oa_version":"Submitted Version","date_updated":"2024-10-22T09:58:18Z","conference":{"start_date":"2016-10-10","location":"San Francisco, CA, USA","name":"MIG: Motion in Games","end_date":"2016-10-12"},"title":"Space-time sculpting of liquid animation","status":"public","_id":"1136","date_created":"2018-12-11T11:50:20Z","oa":1,"abstract":[{"text":"We propose an interactive sculpting system for seamlessly editing pre-computed animations of liquid, without the need for any resimulation. The input is a sequence of meshes without correspondences representing the liquid surface over time. Our method enables the efficient selection of consistent space-time parts of this animation, such as moving waves or droplets, which we call space-time features. Once selected, a feature can be copied, edited, or duplicated and then pasted back anywhere in space and time in the same or in another liquid animation sequence. Our method circumvents tedious user interactions by automatically computing the spatial and temporal ranges of the selected feature. We also provide space-time shape editing tools for non-uniform scaling, rotation, trajectory changes, and temporal editing to locally speed up or slow down motion. Using our tools, the user can edit and progressively refine any input simulation result, possibly using a library of precomputed space-time features extracted from other animations. In contrast to the trial-and-error loop usually required to edit animation results through the tuning of indirect simulation parameters, our method gives the user full control over the edited space-time behaviors. © 2016 Copyright held by the owner/author(s).","lang":"eng"}],"citation":{"apa":"Manteaux, P., Vimont, U., Wojtan, C., Rohmer, D., &#38; Cani, M. (2016). Space-time sculpting of liquid animation. In <i>Proceedings of the 9th International Conference on Motion in Games </i>. San Francisco, CA, USA: ACM. <a href=\"https://doi.org/10.1145/2994258.2994261\">https://doi.org/10.1145/2994258.2994261</a>","mla":"Manteaux, Pierre, et al. “Space-Time Sculpting of Liquid Animation.” <i>Proceedings of the 9th International Conference on Motion in Games </i>, 2994261, ACM, 2016, doi:<a href=\"https://doi.org/10.1145/2994258.2994261\">10.1145/2994258.2994261</a>.","short":"P. Manteaux, U. Vimont, C. Wojtan, D. Rohmer, M. Cani, in:, Proceedings of the 9th International Conference on Motion in Games , ACM, 2016.","ieee":"P. Manteaux, U. Vimont, C. Wojtan, D. Rohmer, and M. Cani, “Space-time sculpting of liquid animation,” in <i>Proceedings of the 9th International Conference on Motion in Games </i>, San Francisco, CA, USA, 2016.","ista":"Manteaux P, Vimont U, Wojtan C, Rohmer D, Cani M. 2016. Space-time sculpting of liquid animation. Proceedings of the 9th International Conference on Motion in Games . MIG: Motion in Games, 2994261.","chicago":"Manteaux, Pierre, Ulysse Vimont, Chris Wojtan, Damien Rohmer, and Marie Cani. “Space-Time Sculpting of Liquid Animation.” In <i>Proceedings of the 9th International Conference on Motion in Games </i>. ACM, 2016. <a href=\"https://doi.org/10.1145/2994258.2994261\">https://doi.org/10.1145/2994258.2994261</a>.","ama":"Manteaux P, Vimont U, Wojtan C, Rohmer D, Cani M. Space-time sculpting of liquid animation. In: <i>Proceedings of the 9th International Conference on Motion in Games </i>. ACM; 2016. doi:<a href=\"https://doi.org/10.1145/2994258.2994261\">10.1145/2994258.2994261</a>"},"publisher":"ACM","article_number":"2994261","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://hal.inria.fr/hal-01367181"}],"date_published":"2016-10-10T00:00:00Z","day":"10","author":[{"full_name":"Manteaux, Pierre","first_name":"Pierre","last_name":"Manteaux"},{"first_name":"Ulysse","last_name":"Vimont","full_name":"Vimont, Ulysse"},{"orcid":"0000-0001-6646-5546","id":"3C61F1D2-F248-11E8-B48F-1D18A9856A87","first_name":"Christopher J","last_name":"Wojtan","full_name":"Wojtan, Christopher J"},{"last_name":"Rohmer","first_name":"Damien","full_name":"Rohmer, Damien"},{"last_name":"Cani","first_name":"Marie","full_name":"Cani, Marie"}],"ec_funded":1,"department":[{"_id":"ChWo"}],"acknowledgement":"This work was partly supported by the starting grant BigSplash, as well as the advanced grant EXPRESSIVE from the European Research Council (ERC-2014-StG 638176 , and ERC-2011-ADG 20110209).","publication":"Proceedings of the 9th International Conference on Motion in Games ","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["004"],"month":"10","publist_id":"6222","quality_controlled":"1","type":"conference","has_accepted_license":"1","doi":"10.1145/2994258.2994261"},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"publication":"Nature Immunology","department":[{"_id":"MiSi"}],"author":[{"first_name":"Elisabeth","last_name":"Salzer","full_name":"Salzer, Elisabeth"},{"last_name":"Çaǧdaş","first_name":"Deniz","full_name":"Çaǧdaş, Deniz"},{"id":"4167FE56-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6625-3348","full_name":"Hons, Miroslav","first_name":"Miroslav","last_name":"Hons"},{"first_name":"Emily","last_name":"Mace","full_name":"Mace, Emily"},{"full_name":"Garncarz, Wojciech","last_name":"Garncarz","first_name":"Wojciech"},{"full_name":"Petronczki, Oezlem","last_name":"Petronczki","first_name":"Oezlem"},{"first_name":"René","last_name":"Platzer","full_name":"Platzer, René"},{"full_name":"Pfajfer, Laurène","first_name":"Laurène","last_name":"Pfajfer"},{"full_name":"Bilic, Ivan","last_name":"Bilic","first_name":"Ivan"},{"last_name":"Ban","first_name":"Sol","full_name":"Ban, Sol"},{"full_name":"Willmann, Katharina","first_name":"Katharina","last_name":"Willmann"},{"first_name":"Malini","last_name":"Mukherjee","full_name":"Mukherjee, Malini"},{"full_name":"Supper, Verena","first_name":"Verena","last_name":"Supper"},{"full_name":"Hsu, Hsiangting","first_name":"Hsiangting","last_name":"Hsu"},{"full_name":"Banerjee, Pinaki","last_name":"Banerjee","first_name":"Pinaki"},{"full_name":"Sinha, Papiya","first_name":"Papiya","last_name":"Sinha"},{"last_name":"Mcclanahan","first_name":"Fabienne","full_name":"Mcclanahan, Fabienne"},{"full_name":"Zlabinger, Gerhard","last_name":"Zlabinger","first_name":"Gerhard"},{"last_name":"Pickl","first_name":"Winfried","full_name":"Pickl, Winfried"},{"full_name":"Gribben, John","last_name":"Gribben","first_name":"John"},{"last_name":"Stockinger","first_name":"Hannes","full_name":"Stockinger, Hannes"},{"full_name":"Bennett, Keiryn","last_name":"Bennett","first_name":"Keiryn"},{"full_name":"Huppa, Johannes","first_name":"Johannes","last_name":"Huppa"},{"last_name":"Dupré","first_name":"Loï̈C","full_name":"Dupré, Loï̈C"},{"first_name":"Özden","last_name":"Sanal","full_name":"Sanal, Özden"},{"first_name":"Ulrich","last_name":"Jäger","full_name":"Jäger, Ulrich"},{"orcid":"0000-0002-6620-9179","id":"41E9FBEA-F248-11E8-B48F-1D18A9856A87","first_name":"Michael K","last_name":"Sixt","full_name":"Sixt, Michael K"},{"full_name":"Tezcan, Ilhan","first_name":"Ilhan","last_name":"Tezcan"},{"last_name":"Orange","first_name":"Jordan","full_name":"Orange, Jordan"},{"full_name":"Boztug, Kaan","last_name":"Boztug","first_name":"Kaan"}],"main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6400263"}],"date_published":"2016-12-01T00:00:00Z","day":"01","article_processing_charge":"No","issue":"12","intvolume":"        17","publisher":"Nature Publishing Group","citation":{"short":"E. Salzer, D. Çaǧdaş, M. Hons, E. Mace, W. Garncarz, O. Petronczki, R. Platzer, L. Pfajfer, I. Bilic, S. Ban, K. Willmann, M. Mukherjee, V. Supper, H. Hsu, P. Banerjee, P. Sinha, F. Mcclanahan, G. Zlabinger, W. Pickl, J. Gribben, H. Stockinger, K. Bennett, J. Huppa, L. Dupré, Ö. Sanal, U. Jäger, M.K. Sixt, I. Tezcan, J. Orange, K. Boztug, Nature Immunology 17 (2016) 1352–1360.","ieee":"E. Salzer <i>et al.</i>, “RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics,” <i>Nature Immunology</i>, vol. 17, no. 12. Nature Publishing Group, pp. 1352–1360, 2016.","chicago":"Salzer, Elisabeth, Deniz Çaǧdaş, Miroslav Hons, Emily Mace, Wojciech Garncarz, Oezlem Petronczki, René Platzer, et al. “RASGRP1 Deficiency Causes Immunodeficiency with Impaired Cytoskeletal Dynamics.” <i>Nature Immunology</i>. Nature Publishing Group, 2016. <a href=\"https://doi.org/10.1038/ni.3575\">https://doi.org/10.1038/ni.3575</a>.","ista":"Salzer E, Çaǧdaş D, Hons M, Mace E, Garncarz W, Petronczki O, Platzer R, Pfajfer L, Bilic I, Ban S, Willmann K, Mukherjee M, Supper V, Hsu H, Banerjee P, Sinha P, Mcclanahan F, Zlabinger G, Pickl W, Gribben J, Stockinger H, Bennett K, Huppa J, Dupré L, Sanal Ö, Jäger U, Sixt MK, Tezcan I, Orange J, Boztug K. 2016. RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics. Nature Immunology. 17(12), 1352–1360.","ama":"Salzer E, Çaǧdaş D, Hons M, et al. RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics. <i>Nature Immunology</i>. 2016;17(12):1352-1360. doi:<a href=\"https://doi.org/10.1038/ni.3575\">10.1038/ni.3575</a>","apa":"Salzer, E., Çaǧdaş, D., Hons, M., Mace, E., Garncarz, W., Petronczki, O., … Boztug, K. (2016). RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics. <i>Nature Immunology</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/ni.3575\">https://doi.org/10.1038/ni.3575</a>","mla":"Salzer, Elisabeth, et al. “RASGRP1 Deficiency Causes Immunodeficiency with Impaired Cytoskeletal Dynamics.” <i>Nature Immunology</i>, vol. 17, no. 12, Nature Publishing Group, 2016, pp. 1352–60, doi:<a href=\"https://doi.org/10.1038/ni.3575\">10.1038/ni.3575</a>."},"doi":"10.1038/ni.3575","volume":17,"type":"journal_article","external_id":{"isi":["000388056400005"],"pmid":["27776107"]},"article_type":"original","quality_controlled":"1","month":"12","publist_id":"6221","date_updated":"2025-09-22T14:13:22Z","scopus_import":"1","oa_version":"Submitted Version","page":"1352 - 1360","publication_status":"published","year":"2016","pmid":1,"isi":1,"abstract":[{"text":"RASGRP1 is an important guanine nucleotide exchange factor and activator of the RAS-MAPK pathway following T cell antigen receptor (TCR) signaling. The consequences of RASGRP1 mutations in humans are unknown. In a patient with recurrent bacterial and viral infections, born to healthy consanguineous parents, we used homozygosity mapping and exome sequencing to identify a biallelic stop-gain variant in RASGRP1. This variant segregated perfectly with the disease and has not been reported in genetic databases. RASGRP1 deficiency was associated in T cells and B cells with decreased phosphorylation of the extracellular-signal-regulated serine kinase ERK, which was restored following expression of wild-type RASGRP1. RASGRP1 deficiency also resulted in defective proliferation, activation and motility of T cells and B cells. RASGRP1-deficient natural killer (NK) cells exhibited impaired cytotoxicity with defective granule convergence and actin accumulation. Interaction proteomics identified the dynein light chain DYNLL1 as interacting with RASGRP1, which links RASGRP1 to cytoskeletal dynamics. RASGRP1-deficient cells showed decreased activation of the GTPase RhoA. Treatment with lenalidomide increased RhoA activity and reversed the migration and activation defects of RASGRP1-deficient lymphocytes.","lang":"eng"}],"date_created":"2018-12-11T11:50:21Z","oa":1,"_id":"1137","status":"public","title":"RASGRP1 deficiency causes immunodeficiency with impaired cytoskeletal dynamics"},{"publisher":"IEEE","citation":{"apa":"Chatterjee, K., Dvoák, W., Henzinger, M., &#38; Loitzenbauer, V. (2016). Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. In <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 197–206). New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2935304\">https://doi.org/10.1145/2933575.2935304</a>","mla":"Chatterjee, Krishnendu, et al. “Model and Objective Separation with Conditional Lower Bounds: Disjunction Is Harder than Conjunction.” <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2016, pp. 197–206, doi:<a href=\"https://doi.org/10.1145/2933575.2935304\">10.1145/2933575.2935304</a>.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvoák, Monika Henzinger, and Veronika Loitzenbauer. “Model and Objective Separation with Conditional Lower Bounds: Disjunction Is Harder than Conjunction.” In <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 197–206. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2935304\">https://doi.org/10.1145/2933575.2935304</a>.","ieee":"K. Chatterjee, W. Dvoák, M. Henzinger, and V. Loitzenbauer, “Model and objective separation with conditional lower bounds: disjunction is harder than conjunction,” in <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>, New York, NY, USA, 2016, pp. 197–206.","ista":"Chatterjee K, Dvoák W, Henzinger M, Loitzenbauer V. 2016. Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, Proceedings Symposium on Logic in Computer Science, , 197–206.","ama":"Chatterjee K, Dvoák W, Henzinger M, Loitzenbauer V. Model and objective separation with conditional lower bounds: disjunction is harder than conjunction. In: <i>Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2016:197-206. doi:<a href=\"https://doi.org/10.1145/2933575.2935304\">10.1145/2933575.2935304</a>","short":"K. Chatterjee, W. Dvoák, M. Henzinger, V. Loitzenbauer, in:, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2016, pp. 197–206."},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1602.02670"}],"day":"05","date_published":"2016-07-05T00:00:00Z","article_processing_charge":"No","acknowledgement":"K.  C.,  M.  H.,  and  W.  D.  are  partially  supported  by  the  Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003.\r\nK. C. is partially supported by the Austrian Science Fund (FWF)\r\nNFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC Start grant\r\n(279307: Graph Games). For W. D., M. H., and V. L. the research\r\nleading to these results has received funding from the European\r\nResearch Council under the European Union’s Seventh Framework\r\nProgramme (FP/2007-2013) / ERC Grant Agreement no. 340506.","department":[{"_id":"KrCh"}],"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Wolfgang","last_name":"Dvoák","full_name":"Dvoák, Wolfgang"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H","last_name":"Henzinger"},{"last_name":"Loitzenbauer","first_name":"Veronika","full_name":"Loitzenbauer, Veronika"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"publication":"Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science","arxiv":1,"alternative_title":["Proceedings Symposium on Logic in Computer Science"],"quality_controlled":"1","month":"07","publist_id":"6219","type":"conference","external_id":{"isi":["000387609200020"],"arxiv":["1602.02670"]},"doi":"10.1145/2933575.2935304","year":"2016","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"}],"publication_status":"published","page":"197 - 206","oa_version":"Preprint","scopus_import":"1","conference":{"end_date":"2016-07-08","name":"LICS: Logic in Computer Science","location":"New York, NY, USA","start_date":"2016-07-05"},"date_updated":"2025-09-22T14:12:05Z","_id":"1140","status":"public","title":"Model and objective separation with conditional lower bounds: disjunction is harder than conjunction","abstract":[{"text":"Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental -regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical -regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives. © 2016 ACM.","lang":"eng"}],"date_created":"2018-12-11T11:50:22Z","oa":1,"isi":1},{"publist_id":"6217","month":"11","quality_controlled":"1","external_id":{"isi":["000390625600021"]},"type":"journal_article","volume":17,"doi":"10.1016/j.jocs.2016.03.004","intvolume":"        17","issue":"1","citation":{"short":"R. Łazarz, M. Idzik, K. Gądek, E.P. Gajda-Zagorska, Journal of Computational Science 17 (2016) 249–260.","ama":"Łazarz R, Idzik M, Gądek K, Gajda-Zagorska EP. Hierarchic genetic strategy with maturing as a generic tool for multiobjective optimization. <i>Journal of Computational Science</i>. 2016;17(1):249-260. doi:<a href=\"https://doi.org/10.1016/j.jocs.2016.03.004\">10.1016/j.jocs.2016.03.004</a>","ista":"Łazarz R, Idzik M, Gądek K, Gajda-Zagorska EP. 2016. Hierarchic genetic strategy with maturing as a generic tool for multiobjective optimization. Journal of Computational Science. 17(1), 249–260.","chicago":"Łazarz, Radosław, Michał Idzik, Konrad Gądek, and Ewa P Gajda-Zagorska. “Hierarchic Genetic Strategy with Maturing as a Generic Tool for Multiobjective Optimization.” <i>Journal of Computational Science</i>. Elsevier, 2016. <a href=\"https://doi.org/10.1016/j.jocs.2016.03.004\">https://doi.org/10.1016/j.jocs.2016.03.004</a>.","ieee":"R. Łazarz, M. Idzik, K. Gądek, and E. P. Gajda-Zagorska, “Hierarchic genetic strategy with maturing as a generic tool for multiobjective optimization,” <i>Journal of Computational Science</i>, vol. 17, no. 1. Elsevier, pp. 249–260, 2016.","mla":"Łazarz, Radosław, et al. “Hierarchic Genetic Strategy with Maturing as a Generic Tool for Multiobjective Optimization.” <i>Journal of Computational Science</i>, vol. 17, no. 1, Elsevier, 2016, pp. 249–60, doi:<a href=\"https://doi.org/10.1016/j.jocs.2016.03.004\">10.1016/j.jocs.2016.03.004</a>.","apa":"Łazarz, R., Idzik, M., Gądek, K., &#38; Gajda-Zagorska, E. P. (2016). Hierarchic genetic strategy with maturing as a generic tool for multiobjective optimization. <i>Journal of Computational Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jocs.2016.03.004\">https://doi.org/10.1016/j.jocs.2016.03.004</a>"},"publisher":"Elsevier","article_processing_charge":"No","day":"01","date_published":"2016-11-01T00:00:00Z","department":[{"_id":"ChWo"}],"acknowledgement":"The work presented in this paper was partially supported by Polish National Science Centre grant nos. DEC-2012/05/N/ST6/03433 and DEC-2011/03/B/ST6/01393. Radosław Łazarz was supported by Polish National Science Centre grant no. DEC-2013/10/M/ST6/00531.","author":[{"first_name":"Radosław","last_name":"Łazarz","full_name":"Łazarz, Radosław"},{"last_name":"Idzik","first_name":"Michał","full_name":"Idzik, Michał"},{"last_name":"Gądek","first_name":"Konrad","full_name":"Gądek, Konrad"},{"first_name":"Ewa P","last_name":"Gajda-Zagorska","full_name":"Gajda-Zagorska, Ewa P","id":"47794CF0-F248-11E8-B48F-1D18A9856A87"}],"publication":"Journal of Computational Science","language":[{"iso":"eng"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","_id":"1141","status":"public","title":"Hierarchic genetic strategy with maturing as a generic tool for multiobjective optimization","date_created":"2018-12-11T11:50:22Z","abstract":[{"lang":"eng","text":"In this paper we introduce the Multiobjective Optimization Hierarchic Genetic Strategy with maturing (MO-mHGS), a meta-algorithm that performs evolutionary optimization in a hierarchy of populations. The maturing mechanism improves growth and reduces redundancy. The performance of MO-mHGS with selected state-of-the-art multiobjective evolutionary algorithms as internal algorithms is analysed on benchmark problems and their modifications for which single fitness evaluation time depends on the solution accuracy. We compare the proposed algorithm with the Island Model Genetic Algorithm as well as with single-deme methods, and discuss the impact of internal algorithms on the MO-mHGS meta-algorithm. © 2016 Elsevier B.V."}],"isi":1,"year":"2016","publication_status":"published","page":"249 - 260","scopus_import":"1","oa_version":"None","date_updated":"2025-09-22T14:11:23Z"}]