Title #1: Practical Aspects of Connecting Theories Through Algebraic Relations
Speaker: Carlos G. Lopez Pombo, University of Buenos Aires and CONICET (Argentina)
Date: Friday, July 22, 2016
Time: 10:00am
Location: NIA, Room 101
Host: Mariano Moscato, Research Scientist, NIA
Abstract: The problems associated to applying formal methods do not end once we write a theory specifying the behavior of a certain software artifact and prove properties about it. In general, different problems require different axiomatizations and tracking the connections between them becomes a problem in its own right if we want to transfer properties proved in different but equivalent formalizations. In this way, sound connections between theories result in the possibility of (partial) borrowing of results proven from one formal description, in the other. In this talk we will discuss the practical aspects and tools derived from the these theoretical connections from the field of universal algebra and algebraic specification.
Bio: Carlos G. Lopez Pombo studied computer science in the School of Science of the University of Buenos Aires. Got a PhD under the supervision of Prof. Marcelo Frías from the same institution and during his studies worked at SRI International with Natarajan Shankar and Sam Owre on semantic embeddings of logics into the datatype theory of PVS. He specialized on topics related to foundations of heterogeneous and structured specifications and applied category theory, but also focused on the construction of tools providing tool support for effective software analysis and verification. Carlos G. Lopez Pombo is a Professor at the University of Buenos Aires, Associated Professor at McMaster University (Canada), Associated Researcher of the Argentine Council for Science and Technical Research (CONICET), and member of the IFIP TC 1.3 – Foundations of software specification.
Title #2: Proof Certificates in PVS
Speaker: Frederic Gilbert, INRIA (France).
Time: 10:30 AM
Abstract: A possible way to reach higher safety guarantees using PVS is to allow independent proof systems to rerun and verify PVS results afterwards. This can be done modifying PVS to output proof certificates. Unlike the existent notion of PVS proofs, which allows PVS to rerun its own results efficiently, these certificates must be expressed in a sufficiently explicit and generic language to be understood by third party systems. The instrumentation of PVS allows to build such certificates step by step during the proof search process. These certificates are expressed and externally checked using Dedukti, a universal proof language. At the current stage of this work, some PVS reasoning steps cannot be fully verified using Dedukti. In order to reach a complete certification process of PVS, we performed an integration with the automated theorem prover MetiTarksi, which is used to prove those gaps independently.
Bio: Frederic Gilbert is a PhD student at Inria in France. His main topics of research are formal methods and logics, more specifically the formalization of mathematical
proofs.