Design and implementation of a behaviorally typed programming system for web services

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para a obtenção do Grau de Mestre em Engenharia Informática.

A Web-Based geographical information system prototype on Portuguese traditional food products

Dissertation submitted in partial fulfilment of the requirements for the Degree of Master of Science in Geospatial Technologies

Type System for the ComponentJ Programming Language

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para a obtenção do grau de Mestre em Engenharia Informática.

A shared-disk parallel cluster file system

Dissertação apresentada para obtenção do Grau de Doutor em Informática Pela Universidade Nova de Lisboa, Faculdade de Ciências e Tecnologia

Web GIS to support irrigation management: a prototype for SAGRA network, Alentejo Portugal

Dissertation submitted in partial fulfilment of the requirements for the Degree of Master of Science in Geospatial Technologies

Constraint-based verification of imperative programs

work presented in the context of the European Master’s program in Computational Logic, as the partial requirement for obtaining Master of Science degree in Computational Logic

A proof system for lock-free concurrency

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

Wireless triple play system

Dissertação para obtenção do Grau de Mestre em Engenharia Electrotécnica e Computadores

Preliminary study of the acoustic behavior concerning an innovative prototype for indoor modular partitioning

This paper presents a preliminary acoustic study concerning the development of the first prototype of a patented removable module for interior partitioning. It is a prefabricated, vertical element for division of interior spaces that does not require the use of gutters or technical support. A set of such modules, linearly disposed, will create a division, allowing the personalization of any indoor area, including open office spaces, rooms, among others. The main characteristic that distinguishes this element from the existing solutions available on the market is that its mobility relies exclusively on a set of integrated bearings at the base of each module. Through an incorporated elevation system, the user can lower the module, move it to the desired position and re-elevate it until pressed against the ledge of the ceiling, making it stable. In this sense, and taking into account its acoustic behavior, several tests were made in the LNEC acoustics lab. Airborne sound insulation tests for different typologies of the prototype were conducted, according to the applicable standards EN ISO 354:2003, EN ISO 717-1:2013 and EN ISO 10140-2:2010. Some important conclusions and analysis of the prototype viability were extracted.

A type system for value-dependent information flow analysis

Information systems are widespread and used by anyone with computing devices as well as corporations and governments. It is often the case that security leaks are introduced during the development of an application. Reasons for these security bugs are multiple but among them one can easily identify that it is very hard to define and enforce relevant security policies in modern software. This is because modern applications often rely on container sharing and multi-tenancy where, for instance, data can be stored in the same physical space but is logically mapped into different security compartments or data structures. In turn, these security compartments, to which data is classified into in security policies, can also be dynamic and depend on runtime data. In this thesis we introduce and develop the novel notion of dependent information flow types, and focus on the problem of ensuring data confidentiality in data-centric software. Dependent information flow types fit within the standard framework of dependent type theory, but, unlike usual dependent types, crucially allow the security level of a type, rather than just the structural data type itself, to depend on runtime values. Our dependent function and dependent sum information flow types provide a direct, natural and elegant way to express and enforce fine grained security policies on programs. Namely programs that manipulate structured data types in which the security level of a structure field may depend on values dynamically stored in other fields The main contribution of this work is an efficient analysis that allows programmers to verify, during the development phase, whether programs have information leaks, that is, it verifies whether programs protect the confidentiality of the information they manipulate. As such, we also implemented a prototype typechecker that can be found at http://ctp.di.fct.unl.pt/DIFTprototype/.