Na próxima terça-feira, 10, na sala 2077 do Instituto de Ciências Exatas (ICEx), de 9h30 às 12h, o pesquisador no Centro de Pesquisa Inria Nancy, uma unidade do Inria, o Instituto Nacional Francês de Pesquisa em Ciência da Computação, e membro do LORIA, o Laboratório de Ciência da Computação e suas aplicações em Nancy, Stephan Merz, irá realizar o tutorial “Modeling and Verifying Algorithms in TLA+”. A entrada é gratuita, sem necessidade prévia de inscrição e aberta ao público. Abaixo, em inglês, saiba mais sobre a palestra e o pesquisador:
SPEAKER: Stephan Merz
I am a researcher at the Inria Nancy research center, a branch of Inria, the French national research institute for computer science, and a member of LORIA, the laboratory for computer science and its applications in Nancy. I have been the head of the VeriDis team of Inria Nancy and LORIA since January 2010.
My scientific interests lie in the area of formal verification, in particular of distributed algorithms and systems. With the members of our team, I am working on methods, techniques, and tools in this field, including theorem proving and model checking. The two main software tools to which our team contributes are the TLA+ Proof System and the veriT SMT solver.
From 2016 to 2021, I was the head of science (délégué scientifique) of the Inria Nancy research center. As such, I was an ex officio member of Inria’s evaluation committee. From 2008 to 2017, I was nominated by Inria as a member of the Scientific Directorate of Schloss Dagstuhl – Leibniz Center for Informatics. From 2012 to 2016, I was co-head of the PhD committee for computer science of the graduate school IAEM. From 2005 to 2011, I was an elected member of INRIA’s evaluation committee, and from 2008 to 2012, I was a member of Section 7 of the National Committee of Scientific Research (CoNRS). Together with colleagues in Liège, Luxembourg, and Saarbrücken I am an organizer of the annual summer school VTSA (Verification Techniques, Systems, and Applications).
TITLE: Modeling and Verifying Algorithms in TLA+
TLA+ is a language for formally describing algorithms and systems, primarily intended for distributed algorithms. It is based on mathematical set theory for describing the data that an algorithm manipulates and on linear-time temporal logic for describing the executions of the algorithm. Properties of TLA+ specifications can be mechanically verified using the explicit-state model checker TLC, the symbolic model checker Apalache, and the interactive proof assistant TLAPS. We will give an overview of the language TLA+ and its support tools, illustrating their use on simple but representative examples.
