b2llvm: B developments onto the LLVM

Abstract
In this talk we describe a multi-platform code generator for the B method. In particular, we present a translation procedure from a large subset of the B language for implementations towards LLVM source code. This translation is defined formally as a set of rules defined recursively on the abstract syntax for B implementations. It already handles most elements of the B language and is being extended to the full language. We describe different strategies to validate the generated LLVM code.

Short bio
Dr. David Deharbe is associate professor at Federal University of Rio Grande do Norte (Natal, Brazil) where he has been since 1997. He is a member of the research group ForAll (Formal Methods and Languages Laboratory) and CNPq has granted him a research productivity grant. He is an associate member of VeriDis team, colocated at INRIA (Nancy, France) and Max-Planck Institute (Saarbrücken, Germany). David Deharbe holds a Doctorate degree in Computer Science from Université de Grenoble (France). He did a post-doc at Carnegie Mellon University (Pittsburgh, USA), and two sabbatical at LORIA (Nancy, France). His areas of interest are formal methods (primarly the B-method) and formal verification techniques (first symbolic model checking and then satisfiability modulo theory). In 2014, he served the program committee of ABZ, ICTAC, iFM, SBMF, and co-organized SMT-COMP. He his one of the main developers of the SMT-solver veriT.

Narciso Martí-Oliet
Universidad Complutense de Madrid, Madrid, Spain

TUESDAY (30/09/2014) – 09:00 – 10:30 (Auditorium 1 and Auditorium 2)

Equational abstractions in rewriting logic and Maude

Abstract
(joint work with J. Meseguer, M. Palomino, F. Durán and A. Verdejo)

Short bio
Dr. Narciso Martí-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. He is principal investigator of several projects of the Spanish Ministry for Science and Innovation and of the Madrid Regional Government, in collaboration with other research groups from Universidad Politecnica de Madrid and UCM. 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. An important contribution has been the book "All About Maude, A High-Performance Logical Framework" published in 2007 in the Springer series Lecture Notes in Computer Science. Marti-Oliet has been a member of several program committees for international conferences, and has also organized conferences such as WRLA'04 on Rewriting Logic and its Applications in Barcelona, Spain, RULE'05 on Rule Based Programming in Nara, Japan, and WADT 2012 on Algebraic Development Techniques in Salamanca, Spain. Moreover, since 2008 he is the vicedean in charge of graduate studies at the Computer Science Department of UCM.