Importância do rigor em provas matemática e papel dos Proofs Assistants. Básicos de Lean, Isabelle e Lean. Prova da infinitude dos números primos em cada um.

Introdução a lógica temporal linear. Verificação em alloy. Case study usando o sistema alloy na verificação do programa de uma aeronave.

Rutherford Backscattering Spectrometry (RBS) spectra, when recorded using a nuclear microprobe (NP), allow the identification of the elemental matrix of an unknown sample, depth profiling of those elements, and visualization of their distribution in 2D maps. Using OMDAQ software, each scanned area is acquired as a 256x256 pixel map, each pixel containing all the ion beam analytical (IBA) spectra recorded during the experiment. A step forward in the analytical capabilities provided by IBA techniques and the NP would be to represent the elemental depth profiling obtained in each pixel of the map in a 3D environment. To achieve this, it is needed to analyse more than 65 thousand RBS spectra recorded, or more than 16 thousand spectra if the maps suffer a 2x2 pixel compression. In any case, the number of RBS spectra to be analyzed requires time and computing resources. To tackle this problem artificial neural networks (ANNs) model are developed, which once trained, can handle the analysis of large data sets instantaneously. The potential of ANNs to automatically render depth profiles of several types of samples in a 3D environment will definitely extend the imaging capabilities of nuclear microprobes.
In this work ANNs are used to perform an automated analysis and classification of RBS spectra recorded during an experiment in the NP of a gold coin which has a inhomogeneous region of Cu. The 3D visualization of this region is very important to try to understand its origin. Challenges as the low statistics of the RBS spectra, the estimated time requirements for training the ANNs, or the visualization in a 3D environment of the results are considered.

Trace Reconstruction é um problema que interseta biologia computacional e teoria da computação. Este envolve reconstruir uma sequência original a partir de várias versões "corrompidas" da mesma, onde cada versão passou por distorções ou erros específicos de um canal de comunicação.

The Lattice Isomorphism Problem (LIP) involves finding an isometry between two given lattices. In recent years, LIP has emerged as a fundamental assumption for constructing quantum-resistant cryptographic primitives. In this presentation, we explore some of these constructions and introduce LIP as a hardness assumption to build public key encryption schemes.