Encontrados 4 documentos, a visualizar página 1 de 1
Partial derivative automata formalized in Coq
Almeida, José Bacelar; Moreira, Nelma; Pereira, David; Sousa, Simão Melo deIn this paper we present a computer assisted proof of the correctness of a partial derivative automata construction from a regular expression within the Coq proof assistant. This proof is part of a for- malization of Kleene algebra and regular languages in Coq towards their usage in program certification.
Model-checking temporal properties of real-time HTL programs
Carvalho, André Ribeiro de; Carvalho, Joel; Pinto, Jorge Sousa; Sousa, Simão Melo deThis paper describes a tool-supported method for the formal verification of timed properties of HTL programs, supported by the automated translation tool HTL2XTA, which extracts from a HTL program (i) an Uppaal model and (ii) a set of properties that state the compliance of the model with certain automatically inferred temporal constraints. These can be manually extended with other temporal properties provided ...
Secure biometric authentication with improved accuracy
Barbosa, Manuel Bernardo; Sousa, Simão Melo de; Brouard, Thierri; Cauchie, StéphaneWe propose a new hybrid protocol for cryptographically secure biometric authentication. The main advantages of the proposed protocol over previous solutions can be summarised as follows: (1) potential for much better accuracy using different types of biometric signals, including behavioural ones; and (2) improved user privacy, since user identities are not transmitted at any point in the protocol execution. The...
Lissom, a source level proof carrying code platform
Gomes, João; Martins, Daniel; Sousa, Simão Melo de; Pinto, Jorge SousaThis paper introduces a proposal for a Proof Carrying Code (PCC) architecture called Lissom. Started as a challenge for final year Computing students, Lissom was thought as a mean to prove to a sceptic community, and in particular to students, that formal verification tools can be put to practice in a realistic environment, and be used to solve complex and concrete problems. The attractiveness of the proble...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||