[{"language":[{"iso":"eng"}],"conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation","location":"San Diego, USA","start_date":"2014-01-19","end_date":"2014-01-21"},"doi":"10.1007/978-3-642-54013-4_10","quality_controlled":"1","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"}],"oa":1,"month":"01","date_updated":"2021-01-12T06:50:22Z","date_created":"2018-12-11T11:51:45Z","volume":8318,"author":[{"full_name":"Dragoi, Cezara","last_name":"Dragoi","first_name":"Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Veith, Helmut","first_name":"Helmut","last_name":"Veith"},{"last_name":"Widder","first_name":"Josef","full_name":"Widder, Josef"},{"full_name":"Zufferey, Damien","first_name":"Damien","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736"}],"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","acknowledgement":"Supported by the Vienna Science and Technology Fund (WWTF) through grant PROSEED.","year":"2014","file_date_updated":"2020-07-14T12:44:48Z","ec_funded":1,"publist_id":"5817","date_published":"2014-01-01T00:00:00Z","page":"161 - 181","citation":{"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.","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.","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","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","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.","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.","short":"C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer, 2014, pp. 161–181."},"day":"01","has_accepted_license":"1","scopus_import":1,"oa_version":"Submitted Version","file":[{"creator":"system","content_type":"application/pdf","file_size":444138,"file_name":"IST-2014-179-v1+1_vmcai14.pdf","access_level":"open_access","date_created":"2018-12-12T10:11:06Z","date_updated":"2020-07-14T12:44:48Z","checksum":"bffa33d39be77df0da39defe97eabf84","file_id":"4859","relation":"main_file"}],"pubrep_id":"179","status":"public","ddc":["000","005"],"title":"A logic-based framework for verifying consensus algorithms","intvolume":" 8318","_id":"1392","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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"}],"alternative_title":["LNCS"],"type":"conference"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1393","title":"Probabilistic programming","status":"public","oa_version":"Published Version","type":"conference","abstract":[{"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.","lang":"eng"}],"citation":{"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","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.","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.","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","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.","short":"A. Gordon, T.A. Henzinger, A. Nori, S. Rajamani, in:, Proceedings of the on Future of Software Engineering, ACM, 2014, pp. 167–181.","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."},"publication":"Proceedings of the on Future of Software Engineering","page":"167 - 181","date_published":"2014-05-31T00:00:00Z","scopus_import":1,"article_processing_charge":"No","day":"31","year":"2014","department":[{"_id":"ToHe"}],"publisher":"ACM","publication_status":"published","author":[{"full_name":"Gordon, Andrew","last_name":"Gordon","first_name":"Andrew"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Aditya","last_name":"Nori","full_name":"Nori, Aditya"},{"first_name":"Sriram","last_name":"Rajamani","full_name":"Rajamani, Sriram"}],"date_created":"2018-12-11T11:51:45Z","date_updated":"2021-01-12T06:50:22Z","publist_id":"5816","ec_funded":1,"main_file_link":[{"url":"https://doi.org/10.1145/2593882.2593900","open_access":"1"}],"oa":1,"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","doi":"10.1145/2593882.2593900","conference":{"location":"Hyderabad, India","start_date":"2014-05-31","end_date":"2014-06-07","name":"FOSE: Future of Software Engineering"},"language":[{"iso":"eng"}],"month":"05"},{"day":"01","month":"04","page":"101","citation":{"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.","mla":"Stock, Miriam. 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.","ista":"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."},"language":[{"iso":"eng"}],"supervisor":[{"full_name":"Cremer, Sylvia M","orcid":"0000-0002-2193-3868","id":"2F64EC8C-F248-11E8-B48F-1D18A9856A87","last_name":"Cremer","first_name":"Sylvia M"}],"date_published":"2014-04-01T00:00:00Z","alternative_title":["IST Austria Thesis"],"type":"dissertation","publist_id":"5803","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."}],"publisher":"IST Austria","department":[{"_id":"SyCr"}],"publication_status":"published","status":"public","title":"Evolution of a fungal pathogen towards individual versus social immunity in ants","year":"2014","_id":"1404","acknowledgement":"This work was funded by the DFG and the ERC.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","date_created":"2018-12-11T11:51:49Z","date_updated":"2021-01-12T06:50:30Z","author":[{"id":"42462816-F248-11E8-B48F-1D18A9856A87","first_name":"Miriam","last_name":"Stock","full_name":"Stock, Miriam"}]},{"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1516","year":"2014","status":"public","title":"On the BCS gap equation for superfluid fermionic gases","publication_status":"published","publisher":"World Scientific Publishing","department":[{"_id":"RoSe"}],"author":[{"full_name":"Bräunlich, Gerhard","last_name":"Bräunlich","first_name":"Gerhard"},{"first_name":"Christian","last_name":"Hainzl","full_name":"Hainzl, Christian"},{"full_name":"Seiringer, Robert","first_name":"Robert","last_name":"Seiringer","id":"4AFD0470-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6781-0521"}],"date_updated":"2021-01-12T06:51:19Z","date_created":"2018-12-11T11:52:28Z","oa_version":"Preprint","type":"conference","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"}],"publist_id":"5661","publication":"Proceedings of the QMath12 Conference","citation":{"short":"G. Bräunlich, C. Hainzl, R. Seiringer, in:, Proceedings of the QMath12 Conference, World Scientific Publishing, 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.","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","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.","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","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."},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1403.2563"}],"oa":1,"external_id":{"arxiv":["1403.2563"]},"quality_controlled":"1","page":"127 - 137","conference":{"name":"QMath: Mathematical Results in Quantum Physics","end_date":"2013-09-13","start_date":"2013-09-10","location":"Berlin, Germany"},"doi":"10.1142/9789814618144_0007","date_published":"2014-01-01T00:00:00Z","language":[{"iso":"eng"}],"month":"01","day":"01","article_processing_charge":"No"},{"_id":"1629","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","title":"Edit propagation using geometric relationship functions","status":"public","ddc":["000"],"intvolume":" 33","pubrep_id":"577","oa_version":"Submitted Version","file":[{"file_name":"IST-2016-577-v1+1_2014.TOG.Paul.EditingPropagation.final.pdf","access_level":"open_access","file_size":9832561,"content_type":"application/pdf","creator":"system","relation":"main_file","file_id":"4876","date_created":"2018-12-12T10:11:22Z","date_updated":"2020-07-14T12:45:07Z","checksum":"7f91e588a4e888610313b98271e6418e"}],"type":"journal_article","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."}],"issue":"2","publication":"ACM Transactions on Graphics","citation":{"ista":"Guerrero P, Jeschke S, Wimmer M, Wonka P. 2014. Edit propagation using geometric relationship functions. ACM Transactions on Graphics. 33(2), 15.","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","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.","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","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.","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.","short":"P. Guerrero, S. Jeschke, M. Wimmer, P. Wonka, ACM Transactions on Graphics 33 (2014)."},"date_published":"2014-03-01T00:00:00Z","day":"01","has_accepted_license":"1","year":"2014","publication_status":"published","publisher":"ACM","department":[{"_id":"ChWo"}],"author":[{"first_name":"Paul","last_name":"Guerrero","full_name":"Guerrero, Paul"},{"full_name":"Jeschke, Stefan","first_name":"Stefan","last_name":"Jeschke","id":"44D6411A-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Michael","last_name":"Wimmer","full_name":"Wimmer, Michael"},{"last_name":"Wonka","first_name":"Peter","full_name":"Wonka, Peter"}],"date_updated":"2021-01-12T06:52:06Z","date_created":"2018-12-11T11:53:08Z","volume":33,"article_number":"15","file_date_updated":"2020-07-14T12:45:07Z","publist_id":"5526","oa":1,"quality_controlled":"1","doi":"10.1145/2591010","language":[{"iso":"eng"}],"month":"03"},{"status":"public","title":"Clustered planarity testing revisited","intvolume":" 8871","_id":"10793","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","alternative_title":["LNCS"],"type":"conference","abstract":[{"lang":"eng","text":"The Hanani–Tutte theorem is a classical result proved for the first time in the 1930s that characterizes planar graphs as graphs that admit a drawing in the plane in which every pair of edges not sharing a vertex cross an even number of times. We generalize this classical result to clustered graphs with two disjoint clusters, and show that a straightforward extension of our result to flat clustered graphs with three or more disjoint clusters is not possible.\r\n\r\nWe also give a new and short proof for a related result by Di Battista and Frati based on the matroid intersection algorithm."}],"page":"428-436","publication":"International Symposium on Graph Drawing","citation":{"ista":"Fulek R, Kynčl J, Malinović I, Pálvölgyi D. 2014. Clustered planarity testing revisited. International Symposium on Graph Drawing. , LNCS, vol. 8871, 428–436.","ieee":"R. Fulek, J. Kynčl, I. Malinović, and D. Pálvölgyi, “Clustered planarity testing revisited,” in International Symposium on Graph Drawing, 2014, vol. 8871, pp. 428–436.","apa":"Fulek, R., Kynčl, J., Malinović, I., & Pálvölgyi, D. (2014). Clustered planarity testing revisited. In International Symposium on Graph Drawing (Vol. 8871, pp. 428–436). Cham: Springer Nature. https://doi.org/10.1007/978-3-662-45803-7_36","ama":"Fulek R, Kynčl J, Malinović I, Pálvölgyi D. Clustered planarity testing revisited. In: International Symposium on Graph Drawing. Vol 8871. Cham: Springer Nature; 2014:428-436. doi:10.1007/978-3-662-45803-7_36","chicago":"Fulek, Radoslav, Jan Kynčl, Igor Malinović, and Dömötör Pálvölgyi. “Clustered Planarity Testing Revisited.” In International Symposium on Graph Drawing, 8871:428–36. Cham: Springer Nature, 2014. https://doi.org/10.1007/978-3-662-45803-7_36.","mla":"Fulek, Radoslav, et al. “Clustered Planarity Testing Revisited.” International Symposium on Graph Drawing, vol. 8871, Springer Nature, 2014, pp. 428–36, doi:10.1007/978-3-662-45803-7_36.","short":"R. Fulek, J. Kynčl, I. Malinović, D. Pálvölgyi, in:, International Symposium on Graph Drawing, Springer Nature, Cham, 2014, pp. 428–436."},"date_published":"2014-01-01T00:00:00Z","scopus_import":"1","day":"01","article_processing_charge":"No","publication_status":"published","department":[{"_id":"UlWa"}],"publisher":"Springer Nature","year":"2014","date_created":"2022-02-25T10:32:14Z","date_updated":"2023-02-23T10:08:04Z","volume":8871,"author":[{"full_name":"Fulek, Radoslav","orcid":"0000-0001-8485-1774","id":"39F3FFE4-F248-11E8-B48F-1D18A9856A87","last_name":"Fulek","first_name":"Radoslav"},{"first_name":"Jan","last_name":"Kynčl","full_name":"Kynčl, Jan"},{"first_name":"Igor","last_name":"Malinović","full_name":"Malinović, Igor"},{"last_name":"Pálvölgyi","first_name":"Dömötör","full_name":"Pálvölgyi, Dömötör"}],"related_material":{"record":[{"relation":"later_version","status":"public","id":"1642"}]},"place":"Cham","quality_controlled":"1","external_id":{"arxiv":["1305.4519"]},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-45803-7_36","month":"01","publication_identifier":{"issn":["0302-9743"]}},{"scopus_import":1,"day":"01","page":"95 - 114","citation":{"ista":"Fuchsbauer G. 2014. Constrained Verifiable Random Functions . SCN 2014. SCN: Security and Cryptography for Networks, LNCS, vol. 8642, 95–114.","apa":"Fuchsbauer, G. (2014). Constrained Verifiable Random Functions . In M. Abdalla & R. De Prisco (Eds.), SCN 2014 (Vol. 8642, pp. 95–114). Amalfi, Italy: Springer. https://doi.org/10.1007/978-3-319-10879-7_7","ieee":"G. Fuchsbauer, “Constrained Verifiable Random Functions ,” in SCN 2014, Amalfi, Italy, 2014, vol. 8642, pp. 95–114.","ama":"Fuchsbauer G. Constrained Verifiable Random Functions . In: Abdalla M, De Prisco R, eds. SCN 2014. Vol 8642. Springer; 2014:95-114. doi:10.1007/978-3-319-10879-7_7","chicago":"Fuchsbauer, Georg. “Constrained Verifiable Random Functions .” In SCN 2014, edited by Michel Abdalla and Roberto De Prisco, 8642:95–114. Springer, 2014. https://doi.org/10.1007/978-3-319-10879-7_7.","mla":"Fuchsbauer, Georg. “Constrained Verifiable Random Functions .” SCN 2014, edited by Michel Abdalla and Roberto De Prisco, vol. 8642, Springer, 2014, pp. 95–114, doi:10.1007/978-3-319-10879-7_7.","short":"G. Fuchsbauer, in:, M. Abdalla, R. De Prisco (Eds.), SCN 2014, Springer, 2014, pp. 95–114."},"publication":"SCN 2014","date_published":"2014-01-01T00:00:00Z","alternative_title":["LNCS"],"type":"conference","abstract":[{"text":"We extend the notion of verifiable random functions (VRF) to constrained VRFs, which generalize the concept of constrained pseudorandom functions, put forward by Boneh and Waters (Asiacrypt’13), and independently by Kiayias et al. (CCS’13) and Boyle et al. (PKC’14), who call them delegatable PRFs and functional PRFs, respectively. In a standard VRF the secret key sk allows one to evaluate a pseudorandom function at any point of its domain; in addition, it enables computation of a non-interactive proof that the function value was computed correctly. In a constrained VRF from the key sk one can derive constrained keys skS for subsets S of the domain, which allow computation of function values and proofs only at points in S. After formally defining constrained VRFs, we derive instantiations from the multilinear-maps-based constrained PRFs by Boneh and Waters, yielding a VRF with constrained keys for any set that can be decided by a polynomial-size circuit. Our VRFs have the same function values as the Boneh-Waters PRFs and are proved secure under the same hardness assumption, showing that verifiability comes at no cost. Constrained (functional) VRFs were stated as an open problem by Boyle et al.","lang":"eng"}],"intvolume":" 8642","status":"public","title":"Constrained Verifiable Random Functions ","_id":"1643","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","oa_version":"Submitted Version","month":"01","project":[{"name":"Provable Security for Physical Cryptography","call_identifier":"FP7","_id":"258C570E-B435-11E9-9278-68D0E5697425","grant_number":"259668"}],"main_file_link":[{"open_access":"1","url":"http://eprint.iacr.org/2014/537"}],"oa":1,"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-10879-7_7","conference":{"end_date":"2014-09-05","start_date":"2014-09-03","location":"Amalfi, Italy","name":"SCN: Security and Cryptography for Networks"},"publist_id":"5509","ec_funded":1,"department":[{"_id":"KrPi"}],"publisher":"Springer","editor":[{"first_name":"Michel","last_name":"Abdalla","full_name":"Abdalla, Michel"},{"full_name":"De Prisco, Roberto","first_name":"Roberto","last_name":"De Prisco"}],"publication_status":"published","year":"2014","volume":8642,"date_created":"2018-12-11T11:53:13Z","date_updated":"2021-01-12T06:52:12Z","author":[{"id":"46B4C3EE-F248-11E8-B48F-1D18A9856A87","last_name":"Fuchsbauer","first_name":"Georg","full_name":"Fuchsbauer, Georg"}]},{"publist_id":"5435","abstract":[{"text":"In this paper we present INTERHORN, a solver for recursion-free Horn clauses. The main application domain of INTERHORN lies in solving interpolation problems arising in software verification. We show how a range of interpolation problems, including path, transition, nested, state/transition and well-founded interpolation can be handled directly by INTERHORN. By detailing these interpolation problems and their Horn clause representations, we hope to encourage the emergence of a common back-end interpolation interface useful for diverse verification tools.","lang":"eng"}],"alternative_title":["EPTCS"],"type":"conference","oa_version":"Submitted Version","volume":169,"date_updated":"2021-01-12T06:52:38Z","date_created":"2018-12-11T11:53:33Z","author":[{"last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh"},{"full_name":"Popeea, Corneliu","first_name":"Corneliu","last_name":"Popeea"},{"first_name":"Andrey","last_name":"Rybalchenko","full_name":"Rybalchenko, Andrey"}],"intvolume":" 169","department":[{"_id":"ToHe"}],"publisher":"Open Publishing","status":"public","title":"Generalised interpolation by solving recursion free-horn clauses","publication_status":"published","_id":"1702","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","year":"2014","month":"12","day":"02","language":[{"iso":"eng"}],"date_published":"2014-12-02T00:00:00Z","doi":"10.4204/EPTCS.169.5","conference":{"end_date":"2014-07-17","location":"Vienna, Austria","start_date":"2014-07-17","name":"HCVS: Horn Clauses for Verification and Synthesis"},"page":"31 - 38","quality_controlled":"1","oa":1,"citation":{"mla":"Gupta, Ashutosh, et al. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 169, Open Publishing, 2014, pp. 31–38, doi:10.4204/EPTCS.169.5.","short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing, 2014, pp. 31–38.","chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Generalised Interpolation by Solving Recursion Free-Horn Clauses.” In Electronic Proceedings in Theoretical Computer Science, EPTCS, 169:31–38. Open Publishing, 2014. https://doi.org/10.4204/EPTCS.169.5.","ama":"Gupta A, Popeea C, Rybalchenko A. Generalised interpolation by solving recursion free-horn clauses. In: Electronic Proceedings in Theoretical Computer Science, EPTCS. Vol 169. Open Publishing; 2014:31-38. doi:10.4204/EPTCS.169.5","ista":"Gupta A, Popeea C, Rybalchenko A. 2014. Generalised interpolation by solving recursion free-horn clauses. Electronic Proceedings in Theoretical Computer Science, EPTCS. HCVS: Horn Clauses for Verification and Synthesis, EPTCS, vol. 169, 31–38.","apa":"Gupta, A., Popeea, C., & Rybalchenko, A. (2014). Generalised interpolation by solving recursion free-horn clauses. In Electronic Proceedings in Theoretical Computer Science, EPTCS (Vol. 169, pp. 31–38). Vienna, Austria: Open Publishing. https://doi.org/10.4204/EPTCS.169.5","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Generalised interpolation by solving recursion free-horn clauses,” in Electronic Proceedings in Theoretical Computer Science, EPTCS, Vienna, Austria, 2014, vol. 169, pp. 31–38."},"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1303.7378v2"}],"publication":"Electronic Proceedings in Theoretical Computer Science, EPTCS"},{"_id":"1708","year":"2014","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publisher":"Neural Information Processing Systems","department":[{"_id":"GaTk"}],"intvolume":" 3","publication_status":"published","status":"public","title":"Spatio-temporal representations of uncertainty in spiking neural networks","author":[{"id":"3933349E-F248-11E8-B48F-1D18A9856A87","first_name":"Cristina","last_name":"Savin","full_name":"Savin, Cristina"},{"last_name":"Denève","first_name":"Sophie","full_name":"Denève, Sophie"}],"volume":3,"oa_version":"None","date_updated":"2021-01-12T06:52:40Z","date_created":"2018-12-11T11:53:35Z","type":"conference","issue":"January","publist_id":"5427","abstract":[{"text":"It has been long argued that, because of inherent ambiguity and noise, the brain needs to represent uncertainty in the form of probability distributions. The neural encoding of such distributions remains however highly controversial. Here we present a novel circuit model for representing multidimensional real-valued distributions using a spike based spatio-temporal code. Our model combines the computational advantages of the currently competing models for probabilistic codes and exhibits realistic neural responses along a variety of classic measures. Furthermore, the model highlights the challenges associated with interpreting neural activity in relation to behavioral uncertainty and points to alternative population-level approaches for the experimental validation of distributed representations.","lang":"eng"}],"main_file_link":[{"url":"http://papers.nips.cc/paper/5343-spatio-temporal-representations-of-uncertainty-in-spiking-neural-networks.pdf"}],"citation":{"ieee":"C. Savin and S. Denève, “Spatio-temporal representations of uncertainty in spiking neural networks,” presented at the NIPS: Neural Information Processing Systems, Montreal, Canada, 2014, vol. 3, no. January, pp. 2024–2032.","apa":"Savin, C., & Denève, S. (2014). Spatio-temporal representations of uncertainty in spiking neural networks (Vol. 3, pp. 2024–2032). Presented at the NIPS: Neural Information Processing Systems, Montreal, Canada: Neural Information Processing Systems.","ista":"Savin C, Denève S. 2014. Spatio-temporal representations of uncertainty in spiking neural networks. NIPS: Neural Information Processing Systems vol. 3, 2024–2032.","ama":"Savin C, Denève S. Spatio-temporal representations of uncertainty in spiking neural networks. In: Vol 3. Neural Information Processing Systems; 2014:2024-2032.","chicago":"Savin, Cristina, and Sophie Denève. “Spatio-Temporal Representations of Uncertainty in Spiking Neural Networks,” 3:2024–32. Neural Information Processing Systems, 2014.","short":"C. Savin, S. Denève, in:, Neural Information Processing Systems, 2014, pp. 2024–2032.","mla":"Savin, Cristina, and Sophie Denève. Spatio-Temporal Representations of Uncertainty in Spiking Neural Networks. Vol. 3, no. January, Neural Information Processing Systems, 2014, pp. 2024–32."},"page":"2024 - 2032","quality_controlled":"1","date_published":"2014-01-01T00:00:00Z","conference":{"name":"NIPS: Neural Information Processing Systems","start_date":"2014-12-08","location":"Montreal, Canada","end_date":"2014-12-13"},"language":[{"iso":"eng"}],"scopus_import":1,"day":"01","month":"01"},{"author":[{"first_name":"Massimo","last_name":"Mongillo","full_name":"Mongillo, Massimo"},{"full_name":"Spathis, Panayotis N","first_name":"Panayotis","last_name":"Spathis"},{"full_name":"Georgios Katsaros","id":"38DB5788-F248-11E8-B48F-1D18A9856A87","last_name":"Katsaros","first_name":"Georgios"},{"last_name":"De Franceschi","first_name":"Silvano","full_name":"De Franceschi, Silvano"},{"first_name":"Pascal","last_name":"Gentile","full_name":"Gentile, Pascal"},{"last_name":"Rurali","first_name":"Riccardo","full_name":"Rurali, Riccardo"},{"full_name":"Cartoixà, Xavier","last_name":"Cartoixà","first_name":"Xavier"}],"date_created":"2018-12-11T11:53:52Z","date_updated":"2021-01-12T06:53:02Z","volume":3,"_id":"1761","acknowledgement":"This work was supported by the Agence Nationale de la Recherche and by the EU through the ERC Starting Grant HybridNano","year":"2014","status":"public","publication_status":"published","title":"PtSi clustering in silicon probed by transport spectroscopy","publisher":"American Physical Society","intvolume":" 3","abstract":[{"text":"Metal silicides formed by means of thermal annealing processes are employed as contact materials in microelectronics. Control of the structure of silicide/silicon interfaces becomes a critical issue when the characteristic size of the device is reduced below a few tens of nanometers. Here, we report on silicide clustering occurring within the channel of PtSi/Si/PtSi Schottky-barrier transistors. This phenomenon is investigated through atomistic simulations and low-temperature resonant-tunneling spectroscopy. Our results provide evidence for the segregation of a PtSi cluster with a diameter of a few nanometers from the silicide contact. The cluster acts as a metallic quantum dot giving rise to distinct signatures of quantum transport through its discrete energy states.","lang":"eng"}],"publist_id":"5363","issue":"4","extern":1,"type":"journal_article","doi":"10.1103/PhysRevX.3.041025","date_published":"2014-01-01T00:00:00Z","publication":"Physical Review X","oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1407.5413","open_access":"1"}],"citation":{"chicago":"Mongillo, Massimo, Panayotis Spathis, Georgios Katsaros, Silvano De Franceschi, Pascal Gentile, Riccardo Rurali, and Xavier Cartoixà. “PtSi Clustering in Silicon Probed by Transport Spectroscopy.” Physical Review X. American Physical Society, 2014. https://doi.org/10.1103/PhysRevX.3.041025.","mla":"Mongillo, Massimo, et al. “PtSi Clustering in Silicon Probed by Transport Spectroscopy.” Physical Review X, vol. 3, no. 4, American Physical Society, 2014, doi:10.1103/PhysRevX.3.041025.","short":"M. Mongillo, P. Spathis, G. Katsaros, S. De Franceschi, P. Gentile, R. Rurali, X. Cartoixà, Physical Review X 3 (2014).","ista":"Mongillo M, Spathis P, Katsaros G, De Franceschi S, Gentile P, Rurali R, Cartoixà X. 2014. PtSi clustering in silicon probed by transport spectroscopy. Physical Review X. 3(4).","apa":"Mongillo, M., Spathis, P., Katsaros, G., De Franceschi, S., Gentile, P., Rurali, R., & Cartoixà, X. (2014). PtSi clustering in silicon probed by transport spectroscopy. Physical Review X. American Physical Society. https://doi.org/10.1103/PhysRevX.3.041025","ieee":"M. Mongillo et al., “PtSi clustering in silicon probed by transport spectroscopy,” Physical Review X, vol. 3, no. 4. American Physical Society, 2014.","ama":"Mongillo M, Spathis P, Katsaros G, et al. PtSi clustering in silicon probed by transport spectroscopy. Physical Review X. 2014;3(4). doi:10.1103/PhysRevX.3.041025"},"quality_controlled":0,"day":"01","month":"01"}]