[{"month":"04","doi":"10.1007/s00429-017-1568-y","language":[{"iso":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["000428419500030"]},"oa":1,"quality_controlled":"1","isi":1,"project":[{"grant_number":"720270","_id":"25CBA828-B435-11E9-9278-68D0E5697425","name":"Human Brain Project Specific Grant Agreement 1 (HBP SGA 1)","call_identifier":"H2020"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}],"file_date_updated":"2020-07-14T12:47:20Z","ec_funded":1,"publist_id":"7192","license":"https://creativecommons.org/licenses/by/4.0/","author":[{"full_name":"Luján, Rafael","first_name":"Rafael","last_name":"Luján"},{"first_name":"Carolina","last_name":"Aguado","full_name":"Aguado, Carolina"},{"last_name":"Ciruela","first_name":"Francisco","full_name":"Ciruela, Francisco"},{"last_name":"Cózar","first_name":"Javier","full_name":"Cózar, Javier"},{"full_name":"Kleindienst, David","last_name":"Kleindienst","first_name":"David","id":"42E121A4-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Luis","last_name":"De La Ossa","full_name":"De La Ossa, Luis"},{"last_name":"Bettler","first_name":"Bernhard","full_name":"Bettler, Bernhard"},{"last_name":"Wickman","first_name":"Kevin","full_name":"Wickman, Kevin"},{"first_name":"Masahiko","last_name":"Watanabe","full_name":"Watanabe, Masahiko"},{"last_name":"Shigemoto","first_name":"Ryuichi","orcid":"0000-0001-8761-9444","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","full_name":"Shigemoto, Ryuichi"},{"first_name":"Yugo","last_name":"Fukazawa","full_name":"Fukazawa, Yugo"}],"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"9562"}]},"date_updated":"2024-03-28T23:30:31Z","date_created":"2018-12-11T11:47:29Z","volume":223,"year":"2018","publication_status":"published","department":[{"_id":"RySh"}],"publisher":"Springer","day":"01","has_accepted_license":"1","article_processing_charge":"No","scopus_import":"1","date_published":"2018-04-01T00:00:00Z","publication":"Brain Structure and Function","citation":{"ama":"Luján R, Aguado C, Ciruela F, et al. Differential association of GABAB receptors with their effector ion channels in Purkinje cells. Brain Structure and Function. 2018;223(3):1565-1587. doi:10.1007/s00429-017-1568-y","apa":"Luján, R., Aguado, C., Ciruela, F., Cózar, J., Kleindienst, D., De La Ossa, L., … Fukazawa, Y. (2018). Differential association of GABAB receptors with their effector ion channels in Purkinje cells. Brain Structure and Function. Springer. https://doi.org/10.1007/s00429-017-1568-y","ieee":"R. Luján et al., “Differential association of GABAB receptors with their effector ion channels in Purkinje cells,” Brain Structure and Function, vol. 223, no. 3. Springer, pp. 1565–1587, 2018.","ista":"Luján R, Aguado C, Ciruela F, Cózar J, Kleindienst D, De La Ossa L, Bettler B, Wickman K, Watanabe M, Shigemoto R, Fukazawa Y. 2018. Differential association of GABAB receptors with their effector ion channels in Purkinje cells. Brain Structure and Function. 223(3), 1565–1587.","short":"R. Luján, C. Aguado, F. Ciruela, J. Cózar, D. Kleindienst, L. De La Ossa, B. Bettler, K. Wickman, M. Watanabe, R. Shigemoto, Y. Fukazawa, Brain Structure and Function 223 (2018) 1565–1587.","mla":"Luján, Rafael, et al. “Differential Association of GABAB Receptors with Their Effector Ion Channels in Purkinje Cells.” Brain Structure and Function, vol. 223, no. 3, Springer, 2018, pp. 1565–87, doi:10.1007/s00429-017-1568-y.","chicago":"Luján, Rafael, Carolina Aguado, Francisco Ciruela, Javier Cózar, David Kleindienst, Luis De La Ossa, Bernhard Bettler, et al. “Differential Association of GABAB Receptors with Their Effector Ion Channels in Purkinje Cells.” Brain Structure and Function. Springer, 2018. https://doi.org/10.1007/s00429-017-1568-y."},"article_type":"original","page":"1565 - 1587","abstract":[{"text":"Metabotropic GABAB receptors mediate slow inhibitory effects presynaptically and postsynaptically through the modulation of different effector signalling pathways. Here, we analysed the distribution of GABAB receptors using highly sensitive SDS-digested freeze-fracture replica labelling in mouse cerebellar Purkinje cells. Immunoreactivity for GABAB1 was observed on presynaptic and, more abundantly, on postsynaptic compartments, showing both scattered and clustered distribution patterns. Quantitative analysis of immunoparticles revealed a somato-dendritic gradient, with the density of immunoparticles increasing 26-fold from somata to dendritic spines. To understand the spatial relationship of GABAB receptors with two key effector ion channels, the G protein-gated inwardly rectifying K+ (GIRK/Kir3) channel and the voltage-dependent Ca2+ channel, biochemical and immunohistochemical approaches were performed. Co-immunoprecipitation analysis demonstrated that GABAB receptors co-assembled with GIRK and CaV2.1 channels in the cerebellum. Using double-labelling immunoelectron microscopic techniques, co-clustering between GABAB1 and GIRK2 was detected in dendritic spines, whereas they were mainly segregated in the dendritic shafts. In contrast, co-clustering of GABAB1 and CaV2.1 was detected in dendritic shafts but not spines. Presynaptically, although no significant co-clustering of GABAB1 and GIRK2 or CaV2.1 channels was detected, inter-cluster distance for GABAB1 and GIRK2 was significantly smaller in the active zone than in the dendritic shafts, and that for GABAB1 and CaV2.1 was significantly smaller in the active zone than in the dendritic shafts and spines. Thus, GABAB receptors are associated with GIRK and CaV2.1 channels in different subcellular compartments. These data provide a better framework for understanding the different roles played by GABAB receptors and their effector ion channels in the cerebellar network.","lang":"eng"}],"issue":"3","type":"journal_article","pubrep_id":"1013","file":[{"file_name":"IST-2018-1013-v1+1_2018_Kleindienst_Differential.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":5542926,"file_id":"5157","relation":"main_file","date_created":"2018-12-12T10:15:36Z","date_updated":"2020-07-14T12:47:20Z","checksum":"a55b3103476ecb5f4f983d8801807e8b"}],"oa_version":"Published Version","_id":"612","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","title":"Differential association of GABAB receptors with their effector ion channels in Purkinje cells","ddc":["571"],"intvolume":" 223"},{"abstract":[{"text":"Parvalbumin-positive (PV+) GABAergic interneurons in hippocampal microcircuits are thought to play a key role in several higher network functions, such as feedforward and feedback inhibition, network oscillations, and pattern separation. Fast lateral inhibition mediated by GABAergic interneurons may implement a winner-takes-all mechanism in the hippocampal input layer. However, it is not clear whether the functional connectivity rules of granule cells (GCs) and interneurons in the dentate gyrus are consistent with such a mechanism. Using simultaneous patch-clamp recordings from up to seven GCs and up to four PV+ interneurons in the dentate gyrus, we find that connectivity is structured in space, synapse-specific, and enriched in specific disynaptic motifs. In contrast to the neocortex, lateral inhibition in the dentate gyrus (in which a GC inhibits neighboring GCs via a PV+ interneuron) is ~ 10-times more abundant than recurrent inhibition (in which a GC inhibits itself). Thus, unique connectivity rules may enable the dentate gyrus to perform specific higher-order computations","lang":"eng"}],"issue":"1","type":"journal_article","oa_version":"Published Version","file":[{"file_id":"5715","relation":"main_file","checksum":"9fe2a63bd95a5067d896c087d07998f3","date_updated":"2020-07-14T12:45:28Z","date_created":"2018-12-17T15:41:57Z","access_level":"open_access","file_name":"2018_NatureComm_Espinoza.pdf","creator":"dernst","content_type":"application/pdf","file_size":4651930}],"status":"public","ddc":["570"],"title":"Parvalbumin+ interneurons obey unique connectivity rules and establish a powerful lateral-inhibition microcircuit in dentate gyrus","intvolume":" 9","_id":"21","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","day":"02","has_accepted_license":"1","article_processing_charge":"No","scopus_import":"1","date_published":"2018-11-02T00:00:00Z","article_type":"original","publication":"Nature Communications","citation":{"chicago":"Espinoza Martinez, Claudia , José Guzmán, Xiaomin Zhang, and Peter M Jonas. “Parvalbumin+ Interneurons Obey Unique Connectivity Rules and Establish a Powerful Lateral-Inhibition Microcircuit in Dentate Gyrus.” Nature Communications. Nature Publishing Group, 2018. https://doi.org/10.1038/s41467-018-06899-3.","short":"C. Espinoza Martinez, J. Guzmán, X. Zhang, P.M. Jonas, Nature Communications 9 (2018).","mla":"Espinoza Martinez, Claudia, et al. “Parvalbumin+ Interneurons Obey Unique Connectivity Rules and Establish a Powerful Lateral-Inhibition Microcircuit in Dentate Gyrus.” Nature Communications, vol. 9, no. 1, 4605, Nature Publishing Group, 2018, doi:10.1038/s41467-018-06899-3.","apa":"Espinoza Martinez, C., Guzmán, J., Zhang, X., & Jonas, P. M. (2018). Parvalbumin+ interneurons obey unique connectivity rules and establish a powerful lateral-inhibition microcircuit in dentate gyrus. Nature Communications. Nature Publishing Group. https://doi.org/10.1038/s41467-018-06899-3","ieee":"C. Espinoza Martinez, J. Guzmán, X. Zhang, and P. M. Jonas, “Parvalbumin+ interneurons obey unique connectivity rules and establish a powerful lateral-inhibition microcircuit in dentate gyrus,” Nature Communications, vol. 9, no. 1. Nature Publishing Group, 2018.","ista":"Espinoza Martinez C, Guzmán J, Zhang X, Jonas PM. 2018. Parvalbumin+ interneurons obey unique connectivity rules and establish a powerful lateral-inhibition microcircuit in dentate gyrus. Nature Communications. 9(1), 4605.","ama":"Espinoza Martinez C, Guzmán J, Zhang X, Jonas PM. Parvalbumin+ interneurons obey unique connectivity rules and establish a powerful lateral-inhibition microcircuit in dentate gyrus. Nature Communications. 2018;9(1). doi:10.1038/s41467-018-06899-3"},"file_date_updated":"2020-07-14T12:45:28Z","ec_funded":1,"publist_id":"8034","article_number":"4605","date_updated":"2024-03-28T23:30:31Z","date_created":"2018-12-11T11:44:12Z","volume":9,"author":[{"first_name":"Claudia ","last_name":"Espinoza Martinez","id":"31FFEE2E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4710-2082","full_name":"Espinoza Martinez, Claudia "},{"id":"30CC5506-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2209-5242","first_name":"José","last_name":"Guzmán","full_name":"Guzmán, José"},{"last_name":"Zhang","first_name":"Xiaomin","id":"423EC9C2-F248-11E8-B48F-1D18A9856A87","full_name":"Zhang, Xiaomin"},{"last_name":"Jonas","first_name":"Peter M","orcid":"0000-0001-5001-4804","id":"353C1B58-F248-11E8-B48F-1D18A9856A87","full_name":"Jonas, Peter M"}],"related_material":{"link":[{"relation":"press_release","description":"News on IST Homepage","url":"https://ist.ac.at/en/news/lateral-inhibition-keeps-similar-memories-apart/"}],"record":[{"id":"6363","status":"public","relation":"dissertation_contains"}]},"publication_status":"published","publisher":"Nature Publishing Group","department":[{"_id":"PeJo"}],"acknowledgement":"This project received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 692692) and the Fond zur Förderung der Wissenschaftlichen Forschung (Z 312-B27, Wittgenstein award), both to P.J..","year":"2018","month":"11","language":[{"iso":"eng"}],"doi":"10.1038/s41467-018-06899-3","isi":1,"quality_controlled":"1","project":[{"name":"Biophysics and circuit function of a giant cortical glumatergic synapse","call_identifier":"H2020","_id":"25B7EB9E-B435-11E9-9278-68D0E5697425","grant_number":"692692"},{"grant_number":"Z00312","_id":"25C5A090-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"external_id":{"isi":["000449069700009"]},"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1},{"language":[{"iso":"eng"}],"doi":"10.4230/LIPIcs.CONCUR.2018.11","conference":{"end_date":"2018-09-07","start_date":"2018-09-04","location":"Beijing, China","name":"CONCUR: Conference on Concurrency Theory"},"project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts","_id":"266EEEC0-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"external_id":{"arxiv":["1806.03108"]},"publication_identifier":{"isbn":["978-3-95977-087-3"]},"month":"09","volume":118,"date_created":"2018-12-11T11:44:27Z","date_updated":"2024-03-28T23:30:34Z","related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Goharshady, Amir","last_name":"Goharshady","first_name":"Amir","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","first_name":"Rasmus"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"}],"publication_status":"published","year":"2018","ec_funded":1,"publist_id":"7988","file_date_updated":"2020-07-14T12:47:34Z","article_number":"11","date_published":"2018-09-01T00:00:00Z","citation":{"ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPIcs.CONCUR.2018.11","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and Y. Velner, “Ergodic mean-payoff games for the analysis of attacks in crypto-currencies,” presented at the CONCUR: Conference on Concurrency Theory, Beijing, China, 2018, vol. 118.","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Velner, Y. (2018). Ergodic mean-payoff games for the analysis of attacks in crypto-currencies (Vol. 118). Presented at the CONCUR: Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2018.11","ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Velner Y. 2018. Ergodic mean-payoff games for the analysis of attacks in crypto-currencies. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 118, 11.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, Y. Velner, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","mla":"Chatterjee, Krishnendu, et al. Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies. Vol. 118, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPIcs.CONCUR.2018.11.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Yaron Velner. “Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPIcs.CONCUR.2018.11."},"has_accepted_license":"1","article_processing_charge":"No","day":"01","scopus_import":"1","oa_version":"Published Version","file":[{"date_updated":"2020-07-14T12:47:34Z","date_created":"2018-12-17T12:08:00Z","checksum":"68a055b1aaa241cc38375083cf832a7d","relation":"main_file","file_id":"5696","content_type":"application/pdf","file_size":1078309,"creator":"dernst","file_name":"2018_CONCUR_Chatterjee.pdf","access_level":"open_access"}],"intvolume":" 118","title":"Ergodic mean-payoff games for the analysis of attacks in crypto-currencies","ddc":["000"],"status":"public","_id":"66","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payo games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions.","lang":"eng"}],"alternative_title":["LIPIcs"],"type":"conference"},{"language":[{"iso":"eng"}],"conference":{"name":"ESOP: European Symposium on Programming","end_date":"2018-04-19","start_date":"2018-04-16","location":"Thessaloniki, Greece"},"doi":"10.1007/978-3-319-89884-1_26","quality_controlled":"1","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"month":"04","date_updated":"2024-03-28T23:30:33Z","date_created":"2018-12-11T11:45:45Z","volume":10801,"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Goharshady, Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","first_name":"Amir","last_name":"Goharshady"},{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"}],"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"}]},"publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"Springer","acknowledgement":"The research was partially supported by Vienna Science and Technology Fund (WWTF) Project ICT15-003, Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Starting grant (279307: Graph Games).","year":"2018","file_date_updated":"2020-07-14T12:46:00Z","publist_id":"7554","ec_funded":1,"date_published":"2018-04-01T00:00:00Z","page":"739 - 767","citation":{"ista":"Chatterjee K, Goharshady AK, Velner Y. 2018. Quantitative analysis of smart contracts. ESOP: European Symposium on Programming, LNCS, vol. 10801, 739–767.","apa":"Chatterjee, K., Goharshady, A. K., & Velner, Y. (2018). Quantitative analysis of smart contracts (Vol. 10801, pp. 739–767). Presented at the ESOP: European Symposium on Programming, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89884-1_26","ieee":"K. Chatterjee, A. K. Goharshady, and Y. Velner, “Quantitative analysis of smart contracts,” presented at the ESOP: European Symposium on Programming, Thessaloniki, Greece, 2018, vol. 10801, pp. 739–767.","ama":"Chatterjee K, Goharshady AK, Velner Y. Quantitative analysis of smart contracts. In: Vol 10801. Springer; 2018:739-767. doi:10.1007/978-3-319-89884-1_26","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Yaron Velner. “Quantitative Analysis of Smart Contracts,” 10801:739–67. Springer, 2018. https://doi.org/10.1007/978-3-319-89884-1_26.","mla":"Chatterjee, Krishnendu, et al. Quantitative Analysis of Smart Contracts. Vol. 10801, Springer, 2018, pp. 739–67, doi:10.1007/978-3-319-89884-1_26.","short":"K. Chatterjee, A.K. Goharshady, Y. Velner, in:, Springer, 2018, pp. 739–767."},"day":"01","article_processing_charge":"No","has_accepted_license":"1","scopus_import":"1","oa_version":"Published Version","file":[{"relation":"main_file","file_id":"5716","date_updated":"2020-07-14T12:46:00Z","date_created":"2018-12-17T15:45:49Z","checksum":"9c8a8338c571903b599b6ca93abd2cce","file_name":"2018_ESOP_Chatterjee.pdf","access_level":"open_access","file_size":1394993,"content_type":"application/pdf","creator":"dernst"}],"title":"Quantitative analysis of smart contracts","status":"public","ddc":["000"],"intvolume":" 10801","_id":"311","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and transfer assets of considerable value (in the form of crypto-currency like Bitcoin). Hence, it is crucial that their implementation is bug-free. We identify the utility (or expected payoff) of interacting with such smart contracts as the basic and canonical quantitative property for such contracts. We present a framework for such quantitative analysis of smart contracts. Such a formal framework poses new and novel research challenges in programming languages, as it requires modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior and modeling utilities which are not specified as standard temporal properties such as safety and termination. While game-theoretic incentives have been analyzed in the security community, their analysis has been restricted to the very special case of stateless games. However, to analyze smart contracts, stateful analysis is required as it must account for the different program states of the protocol. Our main contributions are as follows: we present (i)~a simplified programming language for smart contracts; (ii)~an automatic translation of the programs to state-based games; (iii)~an abstraction-refinement approach to solve such games; and (iv)~experimental results on real-world-inspired smart contracts."}],"alternative_title":["LNCS"],"type":"conference"},{"file":[{"creator":"akafshda","content_type":"application/pdf","file_size":624338,"file_name":"blockchain2018.pdf","access_level":"open_access","date_updated":"2020-07-14T12:47:27Z","date_created":"2019-04-18T10:36:39Z","checksum":"b25c9bb7cf6e7e6634e692d26d41ead8","file_id":"6341","relation":"main_file"}],"oa_version":"Submitted Version","_id":"6340","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","ddc":["000"],"status":"public","title":"Secure Credit Reporting on the Blockchain","abstract":[{"text":"We present a secure approach for maintaining andreporting credit history records on the Blockchain. Our ap-proach removes third-parties such as credit reporting agen-cies from the lending process and replaces them with smartcontracts. This allows customers to interact directly with thelenders or banks while ensuring the integrity, unmalleabilityand privacy of their credit data. Additionally, each customerhas full control over complete or selective disclosure of hercredit records, eliminating the risk of privacy violations or databreaches. Moreover, our approach provides strong guaranteesfor the lenders as well. A lender can check both correctness andcompleteness of the credit data disclosed to her. This is the firstapproach that can perform all credit reporting tasks withouta central authority or changing the financial mechanisms*.","lang":"eng"}],"type":"conference","date_published":"2018-09-01T00:00:00Z","citation":{"ama":"Goharshady AK, Behrouz A, Chatterjee K. Secure Credit Reporting on the Blockchain. In: Proceedings of the IEEE International Conference on Blockchain. IEEE; 2018:1343-1348. doi:10.1109/Cybermatics_2018.2018.00231","apa":"Goharshady, A. K., Behrouz, A., & Chatterjee, K. (2018). Secure Credit Reporting on the Blockchain. In Proceedings of the IEEE International Conference on Blockchain (pp. 1343–1348). Halifax, Canada: IEEE. https://doi.org/10.1109/Cybermatics_2018.2018.00231","ieee":"A. K. Goharshady, A. Behrouz, and K. Chatterjee, “Secure Credit Reporting on the Blockchain,” in Proceedings of the IEEE International Conference on Blockchain, Halifax, Canada, 2018, pp. 1343–1348.","ista":"Goharshady AK, Behrouz A, Chatterjee K. 2018. Secure Credit Reporting on the Blockchain. Proceedings of the IEEE International Conference on Blockchain. IEEE International Conference on Blockchain, 1343–1348.","short":"A.K. Goharshady, A. Behrouz, K. Chatterjee, in:, Proceedings of the IEEE International Conference on Blockchain, IEEE, 2018, pp. 1343–1348.","mla":"Goharshady, Amir Kafshdar, et al. “Secure Credit Reporting on the Blockchain.” Proceedings of the IEEE International Conference on Blockchain, IEEE, 2018, pp. 1343–48, doi:10.1109/Cybermatics_2018.2018.00231.","chicago":"Goharshady, Amir Kafshdar, Ali Behrouz, and Krishnendu Chatterjee. “Secure Credit Reporting on the Blockchain.” In Proceedings of the IEEE International Conference on Blockchain, 1343–48. IEEE, 2018. https://doi.org/10.1109/Cybermatics_2018.2018.00231."},"publication":"Proceedings of the IEEE International Conference on Blockchain","page":"1343-1348","article_processing_charge":"No","has_accepted_license":"1","day":"01","scopus_import":"1","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8934"}]},"author":[{"full_name":"Goharshady, Amir Kafshdar","first_name":"Amir Kafshdar","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584"},{"first_name":"Ali","last_name":"Behrouz","full_name":"Behrouz, Ali"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"}],"date_updated":"2024-03-28T23:30:34Z","date_created":"2019-04-18T10:37:35Z","year":"2018","department":[{"_id":"KrCh"}],"publisher":"IEEE","publication_status":"published","ec_funded":1,"file_date_updated":"2020-07-14T12:47:27Z","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","doi":"10.1109/Cybermatics_2018.2018.00231","conference":{"end_date":"2018-08-03","start_date":"2018-07-30","location":"Halifax, Canada","name":"IEEE International Conference on Blockchain"},"language":[{"iso":"eng"}],"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"oa":1,"external_id":{"isi":["000481634500196"],"arxiv":["1805.09104"]},"project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"isi":1,"quality_controlled":"1","publication_identifier":{"isbn":["978-1-5386-7975-3 "]},"month":"09"}]