{"id":348,"date":"2023-12-11T10:57:42","date_gmt":"2023-12-11T09:57:42","guid":{"rendered":"http:\/\/cri-info.cm\/?page_id=348"},"modified":"2023-12-11T10:57:42","modified_gmt":"2023-12-11T09:57:42","slug":"keynotes","status":"publish","type":"page","link":"http:\/\/cri-info.cm\/?page_id=348","title":{"rendered":"Keynotes"},"content":{"rendered":"\n

Formal Methods and Programming Language Translation – Translating CCS (Calculus of Communicating Systems) into CSP (Communicating Sequential Processes)<\/mark><\/strong><\/p>\n\n\n\n

By G\u00e9rald Ekembe Ngondi<\/em><\/strong><\/p>\n\n\n\n

Bio<\/strong> : I have a BEng from the National School of Post & Telecommunications in Yaounde, an MSc and a PhD from the University of York, UK. My research interests include the semantics of programming languages, the unification of formal methods, the verification of programs, and the analysis of concurrent and distributed systems. I have notably extended the language CSP (Communicating Sequential Processes) with both channel mobility and process migration, in collaboration with Prof. Jim Woodcock, and provided the first correct translation of CCS (Calculus of Communicating Systems) into CSP, in collaboration with Dr. Andrew Butterfield and Dr. Vasileios Koutavas.<\/p>\n\n\n\n

Absract<\/strong> : This presentation aims to introduce Formal Methods and their application to the problem of translation between two programming languages. Formal methods denote the collection of mathematical techniques used for the analysis of computer systems. Typically, a formal method is composed of a formal specification language (or simply formal language), which determines the syntax of programs to be analysed. Different methods propose different language syntax, all of which often serve to represent the same program. A similar situation occurs with programming languages and raises the question of the equivalence between programs. I will discuss the problem of translation between two prominent formal languages, CCS (Calculus of Communicating Systems) into CSP (Communicating Sequential Processes). CCS was pioneered by Prof. Robin Milner (Turing Award 1991), may he rest in peace, and CSP by Prof. Tony Hoare (Turing Award 1980). Both CCS and CSP allow analysing concurrent programs and were considered distinct for the past 40 years, in spite of their similarities. I will notably show how different design decisions affect the degree of correctness of the translation function.<\/p>\n\n\n\n

Mod\u00e9liser et tester des syst\u00e8mes \u00e9volutifs<\/mark><\/strong><\/p>\n\n\n\n

Par Omer Nguena Timo<\/em><\/strong><\/p>\n\n\n\n

Bio<\/strong> : Omer Nguena Timo, Ph.D. est professeur agr\u00e9g\u00e9 \u00e0 l\u2019Universit\u00e9 du Qu\u00e9bec en Outaouais, codirecteur du module de l\u2019informatique et pr\u00e9sident d\u2019un comit\u00e9 de s\u00e9lection des bourses du conseil de recherches en sciences naturelles et en g\u00e9nie du Canada (CRSNG). Dans ses travaux de recherche, il d\u00e9veloppe des m\u00e9thodes de test et de v\u00e9rification \u00e0 base de la logique et des mod\u00e8les formels pour construire des syst\u00e8mes informatis\u00e9s \u00e9volutifs fiables et s\u00e9curis\u00e9s. Il a notamment travaill\u00e9 en France et au Qu\u00e9bec pour accro\u00eetre l\u2019innovation dans des industries des milieux de l\u2019automobile, de l\u2019a\u00e9ronautique et des t\u00e9l\u00e9communications. Omer est Dipl\u00f4m\u00e9 au doctorat en informatique de l\u2019Universit\u00e9 Bordeaux 1 – France et d\u2019une ma\u00eetrise en informatique de l\u2019Universit\u00e9 de Yaound\u00e9 1 \u2013 Cameroun.<\/p>\n\n\n\n

L\u2019Internet des Objets (Isol\u00e9s) par Satellite (SatIoT)<\/mark><\/strong><\/p>\n\n\n\n

Par Didier Donsez<\/em><\/strong><\/p>\n\n\n\n

Bio<\/strong> : Didier Donsez est Professeur des Universit\u00e9s en informatique \u00e0 l’Universit\u00e9 Grenoble Alpes (Grenoble, France) depuis 2007. Il est actuellement en d\u00e9l\u00e9gation au CNRS. Il a \u00e9t\u00e9 Ma\u00eetre de Conf\u00e9rences en informatique \u00e0 l’Universit\u00e9 de Valenciennes (France) de 1996 \u00e0 2001, puis \u00e0 l’Universit\u00e9 Joseph Fourier (Grenoble, France) de 2001 \u00e0 2007. Il a obtenu un doctorat en informatique (1994) \u00e0 l’Universit\u00e9 Paris VI : Pierre et Marie Curie et une HDR (Habilitation \u00e0 Diriger des Recherches) en informatique (2006) \u00e0 l’Universit\u00e9 Joseph Fourier. Son laboratoire de recherche est le LIG (Laboratoire d’Informatique de Grenoble) [https:\/\/www.liglab.fr<\/a>], au sein de l’\u00e9quipe ERODS [http:\/\/erods.liglab.fr<\/a>]. Il enseigne au d\u00e9partement d’informatique de Polytech Grenoble (\u00e9cole d’ing\u00e9nieurs). Ses domaines de recherche portent sur les syst\u00e8mes distribu\u00e9s, les intergiciels et le g\u00e9nie logiciel pour l’internet des objets (IoT) depuis 20 ans. Ses sujets actuels incluent LPGAN, SatIoT et l’intelligence artificielle \u00e0 la p\u00e9riph\u00e9rie des r\u00e9seaux (extreme edge). Il est le promoteur du projet Thingsat, un v\u00e9hicule de recherche en orbite pour l’\u00e9valuation de la modulation LoRa\u00a9 dans les applications SatIoT. Il s\u2019int\u00e9resse \u00e0 l\u2019usage de l\u2019IoT dans les sujets environnementaux et soci\u00e9taux. Il participe \u00e0 plusieurs projets logiciels open-source. Pages web :\u00a0http:\/\/www.linkedin.com\/in\/didierdonsez<\/a>,\u00a0http:\/\/membres-liglab.imag.fr\/donsez\/<\/a>,\u00a0https:\/\/gricad-gitlab.univ-grenoble-alpes.fr\/thingsat\/public\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"

Formal Methods and Programming Language Translation – Translating CCS (Calculus of Communicating Systems) into CSP (Communicating Sequential Processes) By G\u00e9rald Ekembe Ngondi Bio : I have a BEng from the National School of Post & Telecommunications in Yaounde, an MSc and a PhD from the University of York, UK. My research interests include the semantics … Continue reading Keynotes<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"http:\/\/cri-info.cm\/index.php?rest_route=\/wp\/v2\/pages\/348"}],"collection":[{"href":"http:\/\/cri-info.cm\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/cri-info.cm\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/cri-info.cm\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/cri-info.cm\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=348"}],"version-history":[{"count":1,"href":"http:\/\/cri-info.cm\/index.php?rest_route=\/wp\/v2\/pages\/348\/revisions"}],"predecessor-version":[{"id":349,"href":"http:\/\/cri-info.cm\/index.php?rest_route=\/wp\/v2\/pages\/348\/revisions\/349"}],"wp:attachment":[{"href":"http:\/\/cri-info.cm\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=348"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}