Theoretical Computer Science Research Group

He is associate professor of Computer Science at the Federal Center of Techonology of Rio de Janeiro (CEFET/RJ) since 2010 and professor of Technology of Computing Systems from CEDERJ/UFF since 2015. He holds a Phd in Computer Science from UFF (2013). His research interests lie in the areas of computational modeling and applied mathematics, with particular emphasis on the numerical methods and data structures. He has been involved in the development of adaptivity mesh refinement, inverse problems and computational fluid dynamics. Other areas of interest and current research emphasis include artificial neural network to predict environmental properties, numerical analysis and gp-gpu applied to numerical methods. He is a member of SBC and SBMAC.

He studied at Universidade de Brasília (BS in Math, 1983) and PUC-Rio (MSc in CS, 1986 and DSc in CS, 1990). From 1986 to 1990 he taugh at Universidade Federal Fluminense. Since 1991 he has been teaching at PUC-Rio. His research interests are Proof Theory, Automated Theorem Proving, Logical Systems, Category Theory (CT), Toposes and Higher-Order Theories and their Models, Semantics, and the application of this knowledge and the techniques emerged from them in Software Development and Validation together with Structural and Computational Complexity. He has written, together with Paulo Blauth Menezes, a book on Category Theory for Computer Science, in Portuguese, aimed at helping teaching CT to undergraduated students.

Narciso Marti-Oliet is a full professor in the Computer Science Department of Universidad Complutense de Madrid (UCM) in Madrid, Spain. He obtained his PhD in Mathematics-Computer Science in 1991 from UCM with a thesis supervised by J. Meseguer on the categorical semantics of linear logic and order-sorted algebra. His research took place from 1988 at the research center SRI International, in Menlo Park, CA, USA, where he was also a postdoctoral international fellow until his return to Madrid in 1994. In 1995 Marti-Oliet took a permanent position as an associate professor in the Computer Science Department of UCM. Since then his research has been focused on the subjects of declarative multiparadigm programming, and algebraic and logical methods for software specification, design and verification, and in particular on several aspects around the use of rewriting logic in such research areas. Marti-Oliet currently leads the research group on Formal Analysis and Design of Software Systems (FADOSS) at UCM, where he has supervised four PhD theses and is currently supervising three more. He is principal investigator of several national and regional projects. He is also a member of the international team led by J. Meseguer that designs and develops the language and system Maude, based on equational and rewriting logic. Marti-Oliet has been a member of several program committees for international conferences, and has also organized some of them. An important contribution has been the joint authorship of the book "All About Maude, A High-Performance Logical Framework" published in 2007 in the Springer series Lecture Notes in Computer Science. Since 2008 he is also vicedean for graduate studies in the School of Computer Science and Engineering at UCM.

Alberto Pardo is Full Professor at Instituto de Computación, Engineering School, Universidad de la República, Montevideo, Uruguay. He coordinates the Formal Methods Group and holds a Dr.rer.nat. (PhD) from the Darmstadt University of Technology, Germany.

Senior Executive acting in IT consulting for Metals and Mining industries. International experience selling, implementing and supporting projects in Brazil, Argentina, Colombia, Mexico, USA, England, Spain, Portugal, Mozambique and Singapore. Technical background on Sales and Logistics processes. Specialties: SAP R/3 implementation in the following industries: Mining, Oil and Gas, Retail, and Communication.

Joint work with Óscar Martín and Alberto Verdejo

Oct. 25, 2018 Room 213

Rewriting logic is naturally concurrent: several subterms of the state term can be rewritten simultaneously. But state terms are global, which makes compositionality difficult to achieve. Compositionality here means being able to decompose a complex system into its functional components and code each as an isolated and encapsulated system. Our goal is to help bringing compositionality to system specification in rewriting logic. The base of our proposal is the operation that we call synchronous composition. The talk presents the motivations and implications of our proposal, and shows its power with some example specifications.

Joint work with Isabel Pita, Rubén Rubio, and Alberto Verdejo

Oct. 23, 2018 TecMF Seminars, PUC-Rio

Strategies and parameterization are two convenient tools for building clear and easily configurable specifications of complex computational systems, compositionally. Parameterization is already a widely used feature of the Maude rewriting framework, which has recently been given full support for a strategy language and modules. This talk describes the Maude strategy language and the associated parameterization techniques. Then, the specification and analysis of some examples of strategy parameterized systems are shown.

June 4th and 8th, 2018, 11 h Room 315

One common approach in the design of a provable correct compiler is to write first the compiler, having in mind in that process the definitions of the syntax and semantics of the involved languages, and then, as a second step, to develop the correctness proof. This approach is known as externalist and has been investigated in several formal settings such as formal specification methods, categorical formalisations of programming languages, dependent types, etc. In this talk, we present on-going work on an alternative approach to formal compiler construction that follows an internalist discipline in which we develop simultaneously the compiler and its correctness proof. Our approach is based on the use of dependent types. The idea is to enrich the types of the abstract syntax trees of the languages with their own semantic values and then write the compiler as a function between those semantically enriched types where the correctness property is represented in the type of the function. As a result, that function plays the double role of compiler (i.e. AST translator) and proof term of the correctness property. In the talk we show the application of this approach to the translation between a simple while language and a semi-structured code for a stack machine.

May 9th, 2018, 14 h Room 215

Industrial applications involving formal methods are still exceptions to the general rule. Lack of understanding, employees without proper education, difficulty to integrate existing development cycles, no explicit requirement from the market, etc. are explanations often heard for not being more formal. Hence the feedback provided by industry to academics is not as constructive as it might be. Summarizing a 25-year return of experience in the effective application of a formal method - namely B and Event-B - in diverse application domains (railways, smartcard, automotive), this presentation makes clear why and where formal methods have been applied, explains the added value obtained so far, and tries to anticipate the future of these two formalisms for safety critical systems. Some live demonstrations (Atelier B, ClearSy Safety Platform, Formal Data Validation) allow to understand better how formal methods could fit with industrial needs.

May 10th, 14 - 17 h Lab. 305

ClearSy Safety Platform is a new technology aimed at revolutionizing the development of lightweight safety critical applications, up to Safety Integrity Level 4. Its building blocks are already embedded in certified railway applications (platform screen-doors controllers of Stockholm Citybanan and São Paulo L15 metros) and are expected to significantly lower the development and production costs of such systems. It is based on two concepts: (i) A unique formal model (B language) of a function, to obtain a safe application embedding two redundant binaries of this function (4-out-of-4 software architecture) (ii) A low cost high integrity execution platform, to ensure a safe execution through the detection of any divergent behaviour (2-out-of-2 hardware architecture). During the session, you will discover the main safety principles, the programming model and experiment the platform through several examples of increasing difficulty. No particular prior knowledge is required for this course. The formalism and syntax will be introduced only when needed.