[{"date_published":"2014-01-01T00:00:00Z","doi":"10.1007/978-3-642-54013-4_10","date_created":"2018-12-11T11:51:45Z","page":"161 - 181","day":"01","has_accepted_license":"1","year":"2014","publisher":"Springer","quality_controlled":"1","oa":1,"acknowledgement":"Supported by the Vienna Science and Technology Fund (WWTF) through grant PROSEED.","title":"A logic-based framework for verifying consensus algorithms","publist_id":"5817","author":[{"full_name":"Dragoi, Cezara","last_name":"Dragoi","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Veith","full_name":"Veith, Helmut","first_name":"Helmut"},{"first_name":"Josef","last_name":"Widder","full_name":"Widder, Josef"},{"full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","last_name":"Zufferey","first_name":"Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Dragoi, Cezara, Thomas A Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. “A Logic-Based Framework for Verifying Consensus Algorithms,” 8318:161–81. Springer, 2014. https://doi.org/10.1007/978-3-642-54013-4_10.","ista":"Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. 2014. A logic-based framework for verifying consensus algorithms. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 8318, 161–181.","mla":"Dragoi, Cezara, et al. A Logic-Based Framework for Verifying Consensus Algorithms. Vol. 8318, Springer, 2014, pp. 161–81, doi:10.1007/978-3-642-54013-4_10.","ama":"Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. A logic-based framework for verifying consensus algorithms. In: Vol 8318. Springer; 2014:161-181. doi:10.1007/978-3-642-54013-4_10","apa":"Dragoi, C., Henzinger, T. A., Veith, H., Widder, J., & Zufferey, D. (2014). A logic-based framework for verifying consensus algorithms (Vol. 8318, pp. 161–181). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, San Diego, USA: Springer. https://doi.org/10.1007/978-3-642-54013-4_10","ieee":"C. Dragoi, T. A. Henzinger, H. Veith, J. Widder, and D. Zufferey, “A logic-based framework for verifying consensus algorithms,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, San Diego, USA, 2014, vol. 8318, pp. 161–181.","short":"C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer, 2014, pp. 161–181."},"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"}],"volume":8318,"ec_funded":1,"file":[{"file_name":"IST-2014-179-v1+1_vmcai14.pdf","date_created":"2018-12-12T10:11:06Z","creator":"system","file_size":444138,"date_updated":"2020-07-14T12:44:48Z","checksum":"bffa33d39be77df0da39defe97eabf84","file_id":"4859","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"publication_status":"published","month":"01","intvolume":" 8318","alternative_title":["LNCS"],"scopus_import":1,"oa_version":"Submitted Version","abstract":[{"text":"Fault-tolerant distributed algorithms play an important role in ensuring the reliability of many software applications. In this paper we consider distributed algorithms whose computations are organized in rounds. To verify the correctness of such algorithms, we reason about (i) properties (such as invariants) of the state, (ii) the transitions controlled by the algorithm, and (iii) the communication graph. We introduce a logic that addresses these points, and contains set comprehensions with cardinality constraints, function symbols to describe the local states of each process, and a limited form of quantifier alternation to express the verification conditions. We show its use in automating the verification of consensus algorithms. In particular, we give a semi-decision procedure for the unsatisfiability problem of the logic and identify a decidable fragment. We successfully applied our framework to verify the correctness of a variety of consensus algorithms tolerant to both benign faults (message loss, process crashes) and value faults (message corruption).","lang":"eng"}],"department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:44:48Z","ddc":["000","005"],"date_updated":"2021-01-12T06:50:22Z","status":"public","pubrep_id":"179","type":"conference","conference":{"start_date":"2014-01-19","end_date":"2014-01-21","location":"San Diego, USA","name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"_id":"1392"},{"_id":"1393","conference":{"name":"FOSE: Future of Software Engineering","location":"Hyderabad, India","end_date":"2014-06-07","start_date":"2014-05-31"},"type":"conference","status":"public","date_updated":"2021-01-12T06:50:22Z","department":[{"_id":"ToHe"}],"abstract":[{"lang":"eng","text":"Probabilistic programs are usual functional or imperative programs with two added constructs: (1) the ability to draw values at random from distributions, and (2) the ability to condition values of variables in a program via observations. Models from diverse application areas such as computer vision, coding theory, cryptographic protocols, biology and reliability analysis can be written as probabilistic programs. Probabilistic inference is the problem of computing an explicit representation of the probability distribution implicitly specified by a probabilistic program. Depending on the application, the desired output from inference may vary-we may want to estimate the expected value of some function f with respect to the distribution, or the mode of the distribution, or simply a set of samples drawn from the distribution. In this paper, we describe connections this research area called \\Probabilistic Programming" has with programming languages and software engineering, and this includes language design, and the static and dynamic analysis of programs. We survey current state of the art and speculate on promising directions for future research."}],"oa_version":"Published Version","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1145/2593882.2593900"}],"scopus_import":1,"month":"05","publication_status":"published","language":[{"iso":"eng"}],"ec_funded":1,"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"citation":{"ista":"Gordon A, Henzinger TA, Nori A, Rajamani S. 2014. Probabilistic programming. Proceedings of the on Future of Software Engineering. FOSE: Future of Software Engineering, 167–181.","chicago":"Gordon, Andrew, Thomas A Henzinger, Aditya Nori, and Sriram Rajamani. “Probabilistic Programming.” In Proceedings of the on Future of Software Engineering, 167–81. ACM, 2014. https://doi.org/10.1145/2593882.2593900.","ieee":"A. Gordon, T. A. Henzinger, A. Nori, and S. Rajamani, “Probabilistic programming,” in Proceedings of the on Future of Software Engineering, Hyderabad, India, 2014, pp. 167–181.","short":"A. Gordon, T.A. Henzinger, A. Nori, S. Rajamani, in:, Proceedings of the on Future of Software Engineering, ACM, 2014, pp. 167–181.","ama":"Gordon A, Henzinger TA, Nori A, Rajamani S. Probabilistic programming. In: Proceedings of the on Future of Software Engineering. ACM; 2014:167-181. doi:10.1145/2593882.2593900","apa":"Gordon, A., Henzinger, T. A., Nori, A., & Rajamani, S. (2014). Probabilistic programming. In Proceedings of the on Future of Software Engineering (pp. 167–181). Hyderabad, India: ACM. https://doi.org/10.1145/2593882.2593900","mla":"Gordon, Andrew, et al. “Probabilistic Programming.” Proceedings of the on Future of Software Engineering, ACM, 2014, pp. 167–81, doi:10.1145/2593882.2593900."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","author":[{"first_name":"Andrew","last_name":"Gordon","full_name":"Gordon, Andrew"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Nori, Aditya","last_name":"Nori","first_name":"Aditya"},{"first_name":"Sriram","full_name":"Rajamani, Sriram","last_name":"Rajamani"}],"publist_id":"5816","title":"Probabilistic programming","oa":1,"publisher":"ACM","quality_controlled":"1","year":"2014","publication":"Proceedings of the on Future of Software Engineering","day":"31","page":"167 - 181","date_created":"2018-12-11T11:51:45Z","date_published":"2014-05-31T00:00:00Z","doi":"10.1145/2593882.2593900"},{"acknowledgement":"This work was funded by the DFG and the ERC.","oa_version":"None","abstract":[{"lang":"eng","text":"The co-evolution of hosts and pathogens is characterized by continuous adaptations of both parties. Pathogens of social insects need to adapt towards disease defences at two levels: 1) individual immunity of each colony member consisting of behavioural defence strategies as well as humoral and cellular immune responses and 2) social immunity that is collectively performed by all group members comprising behavioural, physiological and organisational defence strategies.\r\n\r\nTo disentangle the selection pressure on pathogens by the collective versus individual level of disease defence in social insects, we performed an evolution experiment using the Argentine Ant, Linepithema humile, as a host and a mixture of the general insect pathogenic fungus Metarhizium spp. (6 strains) as a pathogen. We allowed pathogen evolution over 10 serial host passages to two different evolution host treatments: (1) only individual host immunity in a single host treatment, and (2) simultaneously acting individual and social immunity in a social host treatment, in which an exposed ant was accompanied by two untreated nestmates.\r\n\r\nBefore starting the pathogen evolution experiment, the 6 Metarhizium spp. strains were characterised concerning conidiospore size killing rates in singly and socially reared ants, their competitiveness under coinfecting conditions and their influence on ant behaviour. We analysed how the ancestral atrain mixture changed in conidiospere size, killing rate and strain composition dependent on host treatment (single or social hosts) during 10 passages and found that killing rate and conidiospere size of the pathogen increased under both evolution regimes, but different depending on host treatment.\r\n\r\nTesting the evolved strain mixtures that evolved under either the single or social host treatment under both single and social current rearing conditions in a full factorial design experiment revealed that the additional collective defences in insect societies add new selection pressure for their coevolving pathogens that compromise their ability to adapt to its host at the group level. To our knowledge, this is the first study directly measuring the influence of social immunity on pathogen evolution."}],"month":"04","alternative_title":["IST Austria Thesis"],"publisher":"IST Austria","language":[{"iso":"eng"}],"day":"01","publication_status":"published","year":"2014","date_created":"2018-12-11T11:51:49Z","date_published":"2014-04-01T00:00:00Z","page":"101","_id":"1404","status":"public","type":"dissertation","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:50:30Z","citation":{"ista":"Stock M. 2014. Evolution of a fungal pathogen towards individual versus social immunity in ants. IST Austria.","chicago":"Stock, Miriam. “Evolution of a Fungal Pathogen towards Individual versus Social Immunity in Ants.” IST Austria, 2014.","short":"M. Stock, Evolution of a Fungal Pathogen towards Individual versus Social Immunity in Ants, IST Austria, 2014.","ieee":"M. Stock, “Evolution of a fungal pathogen towards individual versus social immunity in ants,” IST Austria, 2014.","apa":"Stock, M. (2014). Evolution of a fungal pathogen towards individual versus social immunity in ants. IST Austria.","ama":"Stock M. Evolution of a fungal pathogen towards individual versus social immunity in ants. 2014.","mla":"Stock, Miriam. Evolution of a Fungal Pathogen towards Individual versus Social Immunity in Ants. IST Austria, 2014."},"supervisor":[{"last_name":"Cremer","full_name":"Cremer, Sylvia M","orcid":"0000-0002-2193-3868","first_name":"Sylvia M","id":"2F64EC8C-F248-11E8-B48F-1D18A9856A87"}],"title":"Evolution of a fungal pathogen towards individual versus social immunity in ants","department":[{"_id":"SyCr"}],"publist_id":"5803","author":[{"last_name":"Stock","full_name":"Stock, Miriam","first_name":"Miriam","id":"42462816-F248-11E8-B48F-1D18A9856A87"}]},{"publisher":"World Scientific Publishing","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1403.2563"}],"oa":1,"month":"01","abstract":[{"lang":"eng","text":"We present a rigorous derivation of the BCS gap equation for superfluid fermionic gases with point interactions. Our starting point is the BCS energy functional, whose minimizer we investigate in the limit when the range of the interaction potential goes to zero.\r\n"}],"oa_version":"Preprint","page":"127 - 137","doi":"10.1142/9789814618144_0007","date_published":"2014-01-01T00:00:00Z","date_created":"2018-12-11T11:52:28Z","year":"2014","publication_status":"published","day":"01","publication":"Proceedings of the QMath12 Conference","language":[{"iso":"eng"}],"type":"conference","conference":{"start_date":"2013-09-10","location":"Berlin, Germany","end_date":"2013-09-13","name":"QMath: Mathematical Results in Quantum Physics"},"status":"public","_id":"1516","publist_id":"5661","author":[{"first_name":"Gerhard","last_name":"Bräunlich","full_name":"Bräunlich, Gerhard"},{"first_name":"Christian","full_name":"Hainzl, Christian","last_name":"Hainzl"},{"orcid":"0000-0002-6781-0521","full_name":"Seiringer, Robert","last_name":"Seiringer","first_name":"Robert","id":"4AFD0470-F248-11E8-B48F-1D18A9856A87"}],"external_id":{"arxiv":["1403.2563"]},"article_processing_charge":"No","department":[{"_id":"RoSe"}],"title":"On the BCS gap equation for superfluid fermionic gases","citation":{"ista":"Bräunlich G, Hainzl C, Seiringer R. 2014. On the BCS gap equation for superfluid fermionic gases. Proceedings of the QMath12 Conference. QMath: Mathematical Results in Quantum Physics, 127–137.","chicago":"Bräunlich, Gerhard, Christian Hainzl, and Robert Seiringer. “On the BCS Gap Equation for Superfluid Fermionic Gases.” In Proceedings of the QMath12 Conference, 127–37. World Scientific Publishing, 2014. https://doi.org/10.1142/9789814618144_0007.","ama":"Bräunlich G, Hainzl C, Seiringer R. On the BCS gap equation for superfluid fermionic gases. In: Proceedings of the QMath12 Conference. World Scientific Publishing; 2014:127-137. doi:10.1142/9789814618144_0007","apa":"Bräunlich, G., Hainzl, C., & Seiringer, R. (2014). On the BCS gap equation for superfluid fermionic gases. In Proceedings of the QMath12 Conference (pp. 127–137). Berlin, Germany: World Scientific Publishing. https://doi.org/10.1142/9789814618144_0007","short":"G. Bräunlich, C. Hainzl, R. Seiringer, in:, Proceedings of the QMath12 Conference, World Scientific Publishing, 2014, pp. 127–137.","ieee":"G. Bräunlich, C. Hainzl, and R. Seiringer, “On the BCS gap equation for superfluid fermionic gases,” in Proceedings of the QMath12 Conference, Berlin, Germany, 2014, pp. 127–137.","mla":"Bräunlich, Gerhard, et al. “On the BCS Gap Equation for Superfluid Fermionic Gases.” Proceedings of the QMath12 Conference, World Scientific Publishing, 2014, pp. 127–37, doi:10.1142/9789814618144_0007."},"date_updated":"2021-01-12T06:51:19Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"intvolume":" 33","month":"03","abstract":[{"lang":"eng","text":"We propose a method for propagating edit operations in 2D vector graphics, based on geometric relationship functions. These functions quantify the geometric relationship of a point to a polygon, such as the distance to the boundary or the direction to the closest corner vertex. The level sets of the relationship functions describe points with the same relationship to a polygon. For a given query point, we first determine a set of relationships to local features, construct all level sets for these relationships, and accumulate them. The maxima of the resulting distribution are points with similar geometric relationships. We show extensions to handle mirror symmetries, and discuss the use of relationship functions as local coordinate systems. Our method can be applied, for example, to interactive floorplan editing, and it is especially useful for large layouts, where individual edits would be cumbersome. We demonstrate populating 2D layouts with tens to hundreds of objects by propagating relatively few edit operations."}],"oa_version":"Submitted Version","issue":"2","volume":33,"publication_status":"published","language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"4876","checksum":"7f91e588a4e888610313b98271e6418e","date_updated":"2020-07-14T12:45:07Z","file_size":9832561,"creator":"system","date_created":"2018-12-12T10:11:22Z","file_name":"IST-2016-577-v1+1_2014.TOG.Paul.EditingPropagation.final.pdf"}],"type":"journal_article","pubrep_id":"577","status":"public","_id":"1629","file_date_updated":"2020-07-14T12:45:07Z","department":[{"_id":"ChWo"}],"date_updated":"2021-01-12T06:52:06Z","ddc":["000"],"oa":1,"quality_controlled":"1","publisher":"ACM","date_created":"2018-12-11T11:53:08Z","date_published":"2014-03-01T00:00:00Z","doi":"10.1145/2591010","year":"2014","has_accepted_license":"1","publication":"ACM Transactions on Graphics","day":"01","article_number":"15","publist_id":"5526","author":[{"full_name":"Guerrero, Paul","last_name":"Guerrero","first_name":"Paul"},{"full_name":"Jeschke, Stefan","last_name":"Jeschke","id":"44D6411A-F248-11E8-B48F-1D18A9856A87","first_name":"Stefan"},{"first_name":"Michael","full_name":"Wimmer, Michael","last_name":"Wimmer"},{"last_name":"Wonka","full_name":"Wonka, Peter","first_name":"Peter"}],"title":"Edit propagation using geometric relationship functions","citation":{"chicago":"Guerrero, Paul, Stefan Jeschke, Michael Wimmer, and Peter Wonka. “Edit Propagation Using Geometric Relationship Functions.” ACM Transactions on Graphics. ACM, 2014. https://doi.org/10.1145/2591010.","ista":"Guerrero P, Jeschke S, Wimmer M, Wonka P. 2014. Edit propagation using geometric relationship functions. ACM Transactions on Graphics. 33(2), 15.","mla":"Guerrero, Paul, et al. “Edit Propagation Using Geometric Relationship Functions.” ACM Transactions on Graphics, vol. 33, no. 2, 15, ACM, 2014, doi:10.1145/2591010.","ieee":"P. Guerrero, S. Jeschke, M. Wimmer, and P. Wonka, “Edit propagation using geometric relationship functions,” ACM Transactions on Graphics, vol. 33, no. 2. ACM, 2014.","short":"P. Guerrero, S. Jeschke, M. Wimmer, P. Wonka, ACM Transactions on Graphics 33 (2014).","ama":"Guerrero P, Jeschke S, Wimmer M, Wonka P. Edit propagation using geometric relationship functions. ACM Transactions on Graphics. 2014;33(2). doi:10.1145/2591010","apa":"Guerrero, P., Jeschke, S., Wimmer, M., & Wonka, P. (2014). Edit propagation using geometric relationship functions. ACM Transactions on Graphics. ACM. https://doi.org/10.1145/2591010"},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87"}]