Please use this identifier to cite or link to this item: https://hdl.handle.net/1822/80033

Full metadata record
DC FieldValueLanguage
dc.contributor.advisorPinto, Jorge Sousapor
dc.contributor.advisorWeissenbacher, Georgpor
dc.contributor.authorCruz, Carla Isabel Novaispor
dc.date.accessioned2022-10-11T13:17:05Z-
dc.date.available2022-10-11T13:17:05Z-
dc.date.issued2022-04-11-
dc.date.submitted2021-
dc.identifier.urihttps://hdl.handle.net/1822/80033-
dc.descriptionDissertação de mestrado integrado em Informatics Engineeringpor
dc.description.abstractNowadays, there currently exist many working program verification tools however, the developed tools are mostly limited to the verification of sequential code, or else of multi-threaded shared-memory programs. Due to the importance that distributed systems and protocols play in many systems, they have been targeted by the program verification community since the beginning of this area. In this sense, they recently tried to create tools capable of deductive verification in the distributed setting (deductive verification techniques offer the highest degree of assurance) and claim to have achieved impressive results. Thus, this dissertation will explore the use of the Why3 deductive verification tool for the verification of dis tributed algorithms. It will comprise the definition of a dedicated Why3library, together with a representative set of case studies. The goal is to provide evidence that Why3 is a privileged tool for such a task, standing at a sweet spot regarding expressive power and practicality.por
dc.description.abstractNos dias de hoje, possuímos diversas ferramentas de verificação, ferramentas essas limitadas à verificação de código sequencial, ou então de programas multi-thread de memória partilhada. Devido à importância que os sistemas e protocolos distribuídos desempenham em muitos sistemas, estes foram alvos por parte da comunidade de verificação de programas desde o início desta área. Neste sentido, recentemente tentaram criar ferramentas capazes de realizar a verificação dedutiva no ambiente distribuído (técnicas de verificação dedutiva que oferecem o mais elevado grau de segurança) e afirmam ter alcançado resultados impressionantes. Assim, esta dissertação irá explorar o uso da ferramenta de verificação dedutiva Why3 com o propósito de verificar algoritmos distribuídos. Irão ser desenvolvidos modos e modelos da biblioteca Why3do, juntamente com um conjunto representativo de casos de estudos. O objetivo é fornecer evidências de que Why3 é uma ferramenta privilegiada para esta tarefa, estando no ponto ideal na relação poder expressivo e praticabilidade.por
dc.description.sponsorshipThis work is financed by the ERDF – European Regional Development Fund through the North Portugal Regional Operational Programme - NORTE2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia within project NORTE-01-0145-FEDER-028550- PTDC/EEI-COM/28550/2017.por
dc.language.isoengpor
dc.relationinfo:eu-repo/grantAgreement/FCT/9471 - RIDTI/PTDC%2FEEI-COM%2F28550%2F2017/PTpor
dc.rightsopenAccesspor
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/por
dc.subjectDeductive verificationpor
dc.subjectDistributed systems and protocolspor
dc.subjectWhy3por
dc.subjectWhy3dopor
dc.subjectVerificação dedutivapor
dc.subjectSistemas e protocolos distribuídospor
dc.titleVerification of distributed algorithms with the Why3 toolpor
dc.typemasterThesiseng
dc.identifier.tid203022890por
thesis.degree.grantorUniversidade do Minhopor
sdum.degree.grade18 valorespor
sdum.uoeiEscola de Engenhariapor
dc.subject.fosEngenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informáticapor
Appears in Collections:BUM - Dissertações de Mestrado
DI - Dissertações de Mestrado

Files in This Item:
File Description SizeFormat 
Carla Isabel Novais da Cruz.pdfDissertação de mestrado4,99 MBAdobe PDFView/Open

This item is licensed under a Creative Commons License Creative Commons

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID