JCC 2006

Porto, 14 Junho 2006, DCC-FCUP.

O Departamento de Ciência de Computadores da Faculdade de Ciências da Universidade do Porto, o núcleo de Ciência de Computadores do LIACC-UP e os Departamentos de Informática e Matemática da Universidade do Minho organizam uma Jornada de Ciência da Computação, a decorrer no DCC-FCUP a 14 de Junho. O objectivo é promover um encontro informal entre as pessoas destes departamentos com interesse nas áreas mais teóricas das Ciencias da Computação, seus interfaces e suas aplicações. O encontro consistirá em apresentações e debate sobre trabalho de investigação e projectos.

Algumas sugestões de tópicos (esta lista não é limitativa - outros tópicos que se enquadrem no espírito do encontro são igualmente bem-vindos):

• Lógica
• Modelos de Computação
• Autómatos e linguagens formais
• Especificação, refinamento e verificação
• Fundamentos de linguagens de programação
• Modelos de concorrência
• Análise e transformação de programas
• Sistemas e teoria de tipos
• Complexidade computacional
• Criptografia e segurança

Os interessados em fazer uma apresentação neste encontro devem comunicar aos organizadores, até 31 de Maio, o título e resumo (no máx. meia página) da mesma.

Web-page: http://wiki.di.uminho.pt/bin/view/Events/JCC/2006

Organizadores:

• José Carlos Bacelar, DI-UM, jba@di.uminho.pt
• José Carlos Espírito Santo, DM-UM, jes@math.uminho.pt
• Mário Florido, DCC-FCUP, amf@dcc.fc.up.pt

-- JoseBacelarAlmeida - 27 Apr 2006

JCC 2006 - Programa

Porto (DCC-FCUP), 14 Junho 2006 (9:30-17:30)

Criptografia e Segurança

(9:30) Efficient identity-based key encapsulation to multiple parties

Manuel Barbosa (DIUM)

Abstract:

We introduce the concept of identity based key encapsulation to multiple parties (mID-KEM), and define a security model for it. This concept is the identity based analogue of public key KEM to multiple parties. We also analyse possible mID-KEM constructions, and propose an efficient scheme based on bilinear pairings. We prove our scheme secure in the random oracle model under the Gap Bilinear Diffie-Hellman assumption.

(9:50) Information-Theoretic Security in Wireless Networks: From Theory to Practice.

João Barros (DCC-FCUP)

Abstract:

Recent theoretical and practical work has shown that novel physical layer security techniques have the potential to significantly strengthen the security of wireless networks. In the first part of this talk we will briefly review the fundamentals in information-theoretic security and discuss our most recent results. Formulating the problem as one in which two legitimate partners communicate over a quasistatic fading channel and an eavesdropper observes their transmissions through another independent quasi-static fading channel, we define the secrecy capacity in terms of outage probability and provide a complete characterization of the maximum transmission rate at which the eavesdropper is unable to decode any information. In sharp contrast with known results for Gaussian wiretap channels (without feedback), our results show that in the presence of fading information-theoretic security is achievable even when the eavesdropper has a better average signal-to-noise ratio (SNR) than the legitimate receiver. In the second part of the talk, we will propose a practical security scheme by which two terminals (say Alice and Bob) are able to exploit the randomness of wireless fading channels to exchange data in an information-theoretically secure way. To ensure that a potential eavesdropper (say Eve) is unable to decode any useful information, Alice sends useful symbols to Bob only when the instantaneous secrecy capacity is strictly positive. In the remaining time, a specially designed class of LDPC codes is used for reconciliation, thus allowing the extraction of a secret key, which can be distilled using privacy amplification. We believe this opportunistic approach, which borrows from techniques used typically in quantum key distribution, can be used effectively as a physical layer complement to existing cryptographic protocols. Joint work with Miguel Rodrigues (University of Cambridge, UK), Matthieu Bloch (Georgia Tech Lorraine, Metz, France) and Steve McLaughlin? (Georgia Institute of Technology, Atlanta, GA).

(10:10) INTERVALO

Lógica e Lambda-Calculus

(10:20) The Formula-tree proof method

Sabine Broda, Luís Damas (DCC-FCUP)

Abstract:

In this talk we present a proof-method based on an alternative representation for formulas or types. We illustrate its simplicity and adequateness for research in the area of provability in implicational intuitionistic logic or equivalently inhabitation of simple types.

(10:40) Lambda-calculus e cálculo de sequentes

Jose Carlos Espirito Santo, Maria João Frade e Luís Pinto (DMUM+DIUM)

Abstract:

Nesta palestra resumimos o estudo conduzido nos últimos três anos, primeiro no Dep.Matemática, depois em colaboração com o Dep. Informática, em torno da versão multiária do lambda-calculus com aplicação generalizada. Há duas abordagens deste sistema, que determinam duas vertentes do estudo, no contexto do fragmento implicacional da lógica intuicionista. Na primeira abordagem, o sistema é visto como um cálculo de anotações para um fragmento do cálculo de sequentes, e como tal, o sistema é usado como ferramenta útil para investigações em teoria estrutural da demonstração. Na segunda abordagem, o sistema é visto com uma extensão do lambda-calculus em correspondência de Curry-Howard com o mesmo fragmento do cálculo de sequentes, e, como tal, o sistema é usado para dar interpretações computacionais às derivações, ao processo de eliminação do corte, e ao fenómeno de permutabilidade relativos àquele fragmento. Por fim, apresentamos algumas das possíveis direcções futuras para este trabalho, quer na vertente lógica, quer na vertente computacional.

(11:00) INTERVALO

(11:20) Combining arrow logics with deontic and action logics: a step towards dynamic normative

Olga Pacheco (DIUM)

Abstract:

Deontic logics combined with action logics of the type ?sees to it? have been used (since the pioneering works of Kanger, Porn and Lindhal) as a formal tool suited to the static specification and analysis of normative systems. These logics support the specification and analysis of expected behavior of agents (human agents, software components,...), the detection of violations of norms when they occur, and the identification of responsible agents for norm violations. The action logic considered, relate agents with the states of affairs they bring about, abstracting from the concrete actions done to obtain that states of affairs and taking apart temporal issues. This logic is useful in high level specification of systems, where we want to focus on the agents responsible for bringing about generic states of affairs, and where we do not want to enter in details (yet) about what specific actions should be done and when. Deontic logic allow us to describe how agents should act: what they are obliged and permitted to do. It is useful to combine action logic with deontic logic, when we are facing circumstances where we have not full control over agents? actions and we have to take in consideration that agents might deviate from what is expected of them (as described by the norms). The analysis supported by these logics is static and effects of actions cannot be taken in consideration. This work aims to combine arrow logic (due to J. Van Benthem and Y. Venema) with deontic and action logics in order to include dynamics in that logical framework. We start by changing, at the semantic level, the interpretation of possible worlds to arrows, and discuss the meaning of the modal operators in this new semantic context. Then, we discuss the expressive power obtained with the logic resultant from the proposed combination.

(11:40) Linearização Fraca do Lambda-Calculus

Sandra Alves, Mário Florido (DCC-FCUP)

Abstract:

Nesta palestra identificamos uma classe restrita de termos do lambda calculus, à qual chamamos termos lineares fracos. Esta classe incluí o lambda calculus linear, mantendo as suas boas propriedades de normalização forte, redução não duplicativa e inferência de tipos em tempo polinomial. A vantagem desta classe em relação ao lambda calculus linear é a possibilidade de transformar termos gerais do lambda calculus em termos lineares fracos com a mesma forma normal. Apresentamos essa transformação e provamos a sua correcção, mostrando que preserva formas normais.

(12:00) A Local Graph-rewriting System for Deciding Equality in Sum-product Theories

Jorge Sousa Pinto/José Carlos Bacelar (DIUM)

Abstract:

In this paper we outline how a graph-based decision procedure can be given for the functional calculus with sums and products (but no exponentials ? the expressions we use here can not really be seen as a programming language). We show in turn how the system covers reflexivity equational laws, fusion laws, and cancelation laws. The decision procedure has interest independently of our initial motivation. The term language (and its theory) can be seen as the internal language of a category with binary products and coproducts. A standard approach based on term rewriting would work modulo a set of equations; the present work proposes a simpler approach, based on graph-rewriting.

(12:20) ALMOÇO

Modelos de Computação e Complexidade Computacional

(14:30) Uma Forma Normal para Autómatos Finitos Determinísticos e suas Consequências

Rogério Reis, Nelma Moreira (DCC-FCUP)

Abstract:

Na manipulação simbólica de autómatos finitos é importante ter uma representação compacta que os caracterize univocamente, de forma a ser fácil determinar a igualdade entre objectos ou propriedades relacionadas. Apresentamos uma representação por palavras (strings) de autómatos finitos determinísticos inicialmente conexos (ICDFA's), isto é, autómatos em que cada estado é atingível do estado inicial. O método permite enumeração exacta e a geração ordenada de todos os autómatos com n estados sobre um alfabeto de k símbolos. Como cada linguagem regular é caracterizada por um autómato finito mínimo (que é um ICDFA) é possível deste modo determinar o número de linguagens regulares distintas aceites por autómatos de n estados sobre um alfabeto de k símbolos. O método de geração é facilmente paralelizável e juntamente com uma implementação eficiente de um algoritmo de minimização permite que essa computação seja feita em tempo razoável, para valores pequenos de n e k. Mostramos também como podemos gerar aleatoriamente, com uma distribuição garantidamente uniforme, um autómato com um número considerável de estados e símbolos, com base numa tabela de valores pré-calculados. Com base na mesma tabela mostramos como obter uma codificação óptima para os ICDFA's.

(14:50) Um modelo de computação reversível

Armando C. Matos (DCC-FCUP)

Abstract:

As computações logicamente reversíveis não apagam a informação, sendo por isso candidatas a implementações físicas em que não existe dissipação de calor associada à perda de informação. Apresentaremos um modelo concreto de computação reversível: uma linguagem de registos em que cada registo pode conter um inteiro (positivo, nulo ou negativo). Este modelo corresponde de certa maneira à versão recursiva das transformações definidas por recursão primitiva. Compararemos este modelo, que é intrinsecamente reversível, com outros que são derivados de "reversibilizações" de modelos clássicos.

(15:10) Worst-Case Running Times for Average-Case Algorithms

Luís Antunes (DCC-FCUP)

Abstract:

Under a standard hardness assumption we exactly characterize the worst-case running time of languages that are in average polynomial-time over all polynomial-time samplable distributions.

More precisely we show that if exponential time is not in subexponential space, then the following are equivalent for any algorithm A: - For all p-samplable distributions mu, A runs in time polynomial on mu-average. - For all polynomial p, the running time for A is bounded by 2^{O(K^p(x)-K(x)+\log|x|)} for all inputs x.

To prove this result we explore the time-bounded Kolmogorov distribution, m^t(x)=2^{-K^t(x)} where K^t(x) is the Kolmogorov complexity (smallest program size to generate x) with programs limited to run in time t(|x|) and show that under the hardness assumption, the time-bounded Kolmogorov distribution is a universal samplable distribution.

(15:30) INTERVALO

Análise e Verificação de Programas

(15:40) Type-safe Two-Level Data Transformations

Alcino Cunha, Joost Visser, José Nuno Oliveira (DIUM)

Abstract:

A two-level data transformation consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. Examples of two-level data transformations include XML schema evolution coupled with document migration, and data mappings that couple a data format mapping with conversions between mapped formats.

In the 2LT project we apply theories of calculational data refinement and of point-free program transformation to two-level transformations. A refinement of an abstract type into a concrete type B can be modeled by a type-changing rewrite system, where each rewite step produces not only a new type, but also the conversion functions between the old and new type. By repeatedly applying such rewrite steps, complex conversion functions are calculated incrementally while a new type is being derived. The complex conversion functions derived after type-changing rewriting can be subjected to subsequent simplification using laws of point-free program calculation. The same holds for compositions of conversion functions with queries on the target or source data types. Such simplifications then amount for instance to (i) generation of efficient low-level data migrations from high-level migrations (ii) program migration of queries on the source data type to queries on a target data type.

We have implemented both type-changing rewrite systems and type-preserving rewrite systems in Haskell. The implementations involve generalized algebraic datatypes (GADTs), strategy combinators, type-safe representations of types and of functions, and other advanced Haskell techniques. Appropriate front-ends allow us to apply two-level transformations to SQL databases and to XML schemas and documents.

(cancelada) Verificação formal de programas: a perspectiva do Interior

Simão Melo Sousa (UBI)

Abstract:

Proponho apresentar dois projectos de investigação desenvolvidos no Departamento de Informática da Universidade da Beira Interior.

• Fundamentos, metodologias e ferramentas para a verificação formal desistemas de larga escala.

A verificação formal e a transformação de programas são temas sobre os quais existe um grande conjunto de resultados de investigação obtidos ao longo de décadas, com recurso a um conjunto de técnicas e abordagens muito diverso, bem suportado ao nível teórico. As experiências de aplicação destes resultados a ´software´ de dimensão realista são no entanto muito limitadas: invariavelmente limita-se o estudo de viabilidade prática a pequenos exemplos-brinquedo. Com este projecto pretende-se transpor esta barreira de escala e conceber uma plataforma para a verificação formal e a transformação de programas com uma sólida base teórica, mas suficientemente robusta para suportar programas de grande dimensão. A plataforma de transformação "JaKarTa", desenvolvida nos meus trabalhos de doutoramento, é um caso de sucesso neste aspecto, contendo no entanto alguns operadores de transformação resultantes de uma abordagem ´ad hoc´. Com o presente projecto, pretende-se criar um formalismo rigoroso e abrangente, baseado por exemplo na interpretação abstracta, que sirva de enquadramento uniforme para todas as classes de transformações efectuadas em "JaKarTa", entre outras transformações consideradas úteis no contexto da verificação formal de correcção em larga escala.

• Plataformas "Proof Carrying Code" com construção de certificados ao nível do código fonte.

Conceptualmente o Proof Carrying Code (PCC) oferece um nível de segurança inovador particularmente adequado às plataformas de execução de código móvel, sem no entanto penalizar o desempenho geral da arquitectura de execução. Numa tal arquitectura, o produtor de código deve juntar ao código transmitido uma prova formal facilmente verificável, designada de certificado, de que este pode ser executado com segurança, restando assim ao consumidor de código a tarefa de verificar a validade da demonstração fornecida. Neste projecto pretendemos propôr de arquitectura de suporte ao PCC que flexibiliza e extende as capacidades das arquitecturas actualmente existentes. De facto nestas plataformas o certificado é construído com base no código binário. É nossa opinião que a verificação formal de código móvel, para ser alvo de uma utilização industrial, deve ser realizada ao nível do código fonte. Um programador pode desconhecer os pormenores da arquitectura alvo, ou no mínimo se sentir desconfortável em raciocinar sobre estruturas de baixo nível enquanto as suas construções algorítmicas são de nível mais alto.

(16:00) Aplicações de model checking à análise de software

José Creissac Campos (DIUM)

Abstract: Apresentar-se-ão, de forma sumária, dois projectos neste momento a decorrer e em que se estuda a aplicação de técnicas de model checking à análise de software. No primeiro (IVY - um abiente de análise de usabilidade baseado em modelos) está a desenvolver-se uma ferramenta para a modelação e verificação de sistemas interactivos. A ferramenta funciona como um front-end para o model checker SMV e permite/permitirá a edição de modelos e de propriedades a verificar, bem como a análise dos resultados do processo de verificação. Neste contexto estão também a ser estudadas técnicas de engenharia reversa para a geração dos modelos a partir de código.

No segundo projecto (SCAPS - Controlo seguro de sistemas automatizados de produção) pretende estudar-se a aplicação de model checking temporizado na verificação da programação de PLCs (Programmable Logic Controllers). Este projecto está em fase incial e o model checker seleccionado é o Uppaal.

(16:20) Análise de Recursos: o tamanho é importante

Pedro Vasconcelos (DCC-FCUP)

Abstract:

A previsão estática dos recursos de tempo ou memória é importante no desenvolvimento de "software" para sistemas críticos e de tempo-real. Nesta palestra apresentamos um trabalho de modelação de recursos combinando um sistema de tipos com anotações de tamanhos com um sistema de efeitos. Este sistema foi implementado como uma análise de programa capaz de inferir automaticamente métricas lineares para recursos de memória de uma linguagem funcional de primeira ordem. Este trabalho foi desenvolvido na Universidade de St. Andrews no contexto do projecto "Hume" para computação com recursos garantidos, sob a orientação de Kevin Hammond.

(16:40) INTERVALO

(17:00) Painel de Discussão

.natBreadCrumbs { width:0px; height:0px; overflow:hidden; }

.twikiToc { padding-top:0px; padding-bottom:0px; background: white; border-top:0px; border-bottom:0px; }

.avisos { color: #444; font-size:11px; }

.natSideBarContents .natExternalLink:after { margin-left:0px; margin-right:0px; content:""; }

.natMainFooterContents, .natMainHeaderContents { padding:0px; margin:0px 0px; }

See also the faster WebTopicList

• AlcinoCunha

Format: <space><space><space>, followed by:
* Main.yourWikiName (if you want that the e-mail address in your home page is used)
* Main.yourWikiName - yourEmailAddress (if you want to specify a different e-mail address)
* Main.anyTWikiGroup (if you want to notify all members of a particular TWikiGroup)

Related topics: TWikiUsers, TWikiRegistration

Warning

Can't INCLUDE TWiki.WebSearchAdvanced repeatedly, topic is already included.

Statistics for Events/JCC Web

Notes:

• Do not edit this topic, it is updated automatically. (You can also force an update)
• TWikiDocumentation tells you how to enable the automatic updates of the statistics.
• Suggestion: You could archive this topic once a year and delete the previous year's statistics from the table.