Towards a formally verified microkernel using the Frama-C toolset

This dissertation is included in the MSc course in Computer Science of the University of Beira Interior. It is a Formal Method’s related dissertation, where it’s used an Hoare Logic based paradigm, the Design by Contract (DbC). This project consists in doing a Formal Verification of an industrial re...

Full description

Bibliographic Details
Main Author: Carloto, Carlos José Abreu Dias da Silva (author)
Format: masterThesis
Language:eng
Published: 2015
Subjects:
Online Access:http://hdl.handle.net/10400.6/3716
Country:Portugal
Oai:oai:ubibliorum.ubi.pt:10400.6/3716