| dc.contributor | Moura, Flávio Leonardo Cavalcanti de | |
| dc.creator | Queiroz, João Paulo Carvalho Colu de | |
| dc.date | 2012-10-24T11:08:41Z | |
| dc.date | 2012-10-24T11:08:41Z | |
| dc.date | 2012-10-24T11:08:41Z | |
| dc.date | 2012-07-06 | |
| dc.date.accessioned | 2017-03-07T12:44:32Z | |
| dc.date.available | 2017-03-07T12:44:32Z | |
| dc.identifier | QUEIROZ, João Paulo Carvalho Colu de. Um estudo sobre verificação formal de sistemas concorrentes. 2012. ix, 64 f., il. Dissertação (Mestrado em Ciência da Computação)—Universidade de Brasília, Brasília, 2012. | |
| dc.identifier | http://repositorio.unb.br/handle/10482/11471 | |
| dc.identifier.uri | http://repositorioslatinoamericanos.uchile.cl/handle/2250/354224 | |
| dc.description | Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2012. | |
| dc.description | Este trabalho apresenta um estudo de metodologias para veri cação formal de aplicativos desenvolvidos em linguagens imperativas, em especial, na linguagem Java. Os formalismos teóricos mostrados incluem a Lógica de Hoare, usada para representar pro-
priedades de aplicações imperativas, e construções da linguagem de especi cação JML
(baseada na Lógica de Hoare), usada para especi car o comportamento esperado de apli-
cações codi cadas em Java. As ferramentas mostradas são o sistema Krakatoa, usado
para converter especi cações JML em obrigações de prova, e o ambiente interativo de provas Coq, usado para veri car obrigações de prova. Finalmente, exibe-se um estudo de
caso que utiliza o ferramental teórico e prático proposto. ______________________________________________________________________________ ABSTRACT | |
| dc.description | This work presents a study of methodologies to formally verify applications developed
with imperative languages, specially with the Java language. The theoretical formalisms
shown include Hoare Logic, which is used to sketch properties on imperative languages,
and JML constructions (based on Hoare Logic), which is a speci cation language used
to specify the expected behavior from Java programs. The tools shown are the Krakatoa
system, used to convert JML speci cations into proof obligations, and the Coq interactive proof environment, used to verify proof obligations. Finally, this paper presents a case study that employs the theoretical and practical proposed framework. | |
| dc.language | por | |
| dc.rights | Open Access | |
| dc.subject | Linguagem de programação (Computadores) | |
| dc.subject | Java (Linguagem de programação de computador) | |
| dc.title | Um estudo sobre verificação formal de sistemas concorrentes | |
| dc.type | Tesis | |
