Ou procure na linha do tempo com mais detalhes.

Provas de Agregação em Engenharia Informática e de Computadores

Provas de Agregação do Prof. Doutor José Luís Borbinha. Relatório da Unidade Curricular: "Systems Analysis and Modelling". Seminário: "Records management and digital preservation - Two facets of information management".

access_time 04 de fevereiro de 2019 às 14:00
place Anfiteatro PA-3: Piso -1 , Pavilhão de Matemática. Instituto Superior Técnico, Campus Alameda.
local_offer Prova de Agregação
person Candidato: Prof. Doutor José Luís Brinquete Borbinha

Techniques for Enhancing the Performance of Data-intensive Management Systems

The demand for storing and analyzing large volumes of data is today on the rise as web-based enterprises introduce innovative and interactive applications, that attract more and more users on a global scale. To cope with such data volumes, data management systems have been evolving to deliver increasingly better performance and efficiency at lower costs in large-scale scenarios. A fundamental property of these systems is data consistency. In storage systems, consistency refers to how accurate, fresh and synchronized is the state of data replicas across different machines. Most of these systems, sacrifice consistency in favor of availability and performance; while others, provide strong consistency and sacrifice availability and performance. In data processing systems, dataflow and stream continuous processing, consistency refers to the completeness state of the input that is reflected in the dataflow end output within a time frame. Traditional dataflow management systems are strongly consistent by enforcing strict temporal synchronization across processing steps. In a multitude of scenarios, such model results in inefficient executions that solely cause a marginal impact on the output, with respect to a previous state. On the other hand, stream processing systems, that deal with timestamped events, tend to be looser in terms of consistency in order to sustain low latency and not overload resources, which might not be acceptable in mission critical applications. The main goal of our research is to study performance optimizations for data-intensive management systems. At the heart of these optimizations resides the tuning of data consistency. For this tuning, we take into account the semantics of data in order to trade-off consistency for performance and resource usage in data management systems. Our evaluation indicates that we can achieve substantial performance gains, namely in terms of latency, throughput, bandwidth, and resource utilization, while keeping application outputs within acceptable levels of correctness, as defined by decision makers.

access_time 19 de dezembro de 2018 às 14:00
place Sala V0.15 (Piso 0 do Pavilhão de Civil) do IST, Alameda
local_offer Prova de Doutoramento
person Candidato: Sérgio Ricardo de Oliveira Esteves Nº 54564
supervisor_account Orientador 1: Prof. Luís Manuel Antunes Veiga
supervisor_account Orientador 2: Prof. João Nuno De Oliveira e Silva

JaVerT 2.0: Compositional Symbolic Execution for JavaScript

The dynamic nature of JavaScript and its complex semantics make it a difficult target for program analysis and verification. We will present JaVerT 2.0, a JavaScript Verification and Testing Toolchain that combines symbolic execution and compositional program reasoning based on separation logic. JaVerT 2.0 supports scalable whole-program symbolic testing, full verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the implementation. We will give an overview of the architecture and metatheory of JaVerT 2.0 and illustrate how it can be used in the verification and testing of JavaScript programs, using the example of a simple expression evaluator. Further details can be found in the eponymous paper to be presented at POPL'19 and in the original JaVerT paper published in POPL'18.

access_time 12 de dezembro de 2018 às 12:15
place IST Alameda - Room 0.19 (Informática II building) and IST TagusPark - Room 2N1.5 (through videoconference)
local_offer DEI às quartas
face José Fragoso Santos

Leveraging Existing Technologies to Improve Large Scale Recommender Systems

Research on Recommendation Systems (RS) demonstrates that, although increasingly complex techniques can improve results, it is not often that the authors show concern on how such techniques can be implemented on a large scale. Within this context, this thesis intends to approach the following hypothesis: on a traditional ratings-based RS implementation, we can replace the rating by a more informative value, such that, when a traditional recommendation algorithm is applied, higher accuracy results can be obtained. Thus, our goal is to achieve the effectiveness levels of current state-of-the-art approaches, while maintaining the efficiency and practical usability of the already existing, highly scalable, software frameworks.

access_time 10 de dezembro de 2018 às 14:30
place IST Alameda - Sala 0.20, Pavilhão Informática II
local_offer Prova de CAT
person Candidato: André Filipe Caldaça da Silva Carvalho N.º 76593
supervisor_account Orientador 1: Prof. Pável Pereira Calado
supervisor_account Orientador 2: Prof. João Paulo Baptista de Carvalho

Interactive theorem proving and software verification

Successes in the formal verification of sizeable programs, such as the CompCert C compiler, the seL4 microkernel, and the verified implementation of OpenSSL HMAC, show the growing importance of interactive theorem provers (ITPs) such as Coq and Isabelle/HOL. However, verification using ITPs continues to be an expert’s job. In this talk I will present my work on tools and methods that aim to make interactive theorem proving technology and software verification more accessible to non-experts. I will talk about my work on structure editing of handwritten mathematics and the initial steps towards a system that can formally verify handwritten calculational proofs without the need to learn the specific syntax and intricacies of ITPs.

access_time 05 de dezembro de 2018 às 13:30
place IST Alameda - Room 0.19 (Informática II building) and IST TagusPark - Room 2N1.5 (through videoconference)
local_offer DEI às quartas
face Prof. Alexandra Mendes

Navegue pelo calendário para descobrir os eventos.