Formal verification of a red-black tree data structure

Formal verification of a red-black tree data structure. Nguyen, i. H. March, 2019.

Nowadays, although software has been integrated deeply into our society, software errors are still common. Because the failure of software can have devastating effects, being certain that a program does what it is meant to do is crucial. This thesis conducts a case study in deductive verification, which is a sub-area of formal verification. The case study involves a company in the Netherlands and their industrial red-black tree code. This thesis is intended to be an experience report to show how formal verification can be used to help proving the correctness of a program. Ultimately, we want to be able to verify the industrial red-black tree code. However, in this thesis, we only cover the verification of a standard red-black tree code. The main section presents how specifications of a red-black tree can be developed, and the obstacles that are met during the development. Finally, we conclude with the comparisons with the results of other authors and possible future work.

@misc{essay77569,
           month = {March},
          author = {ir. H.M. {Nguyen}},
            year = {2019},
           title = {Formal verification of a red-black tree data structure},
             url = {http://essay.utwente.nl/77569/},
        abstract = {Nowadays, although software has been integrated deeply into our society, software errors are still common. Because the failure of software can have devastating effects, being certain that a program does what it is meant to do is crucial. This thesis conducts a case study in deductive verification, which is a sub-area of formal verification. The case study involves a company in the Netherlands and their industrial red-black tree code. This thesis is intended to be an experience report to show how formal verification can be used to help proving the correctness of a program. Ultimately, we want to be able to verify the industrial red-black tree code. However, in this thesis, we only cover the verification of a standard red-black tree code. The main section presents how specifications of a red-black tree can be developed, and the obstacles that are met during the development. Finally, we conclude with the comparisons with the results of other authors and possible future work.}
}

Downloads: 2

{"_id":"ZzsHvnp5BKGPB953Z","bibbaseid":"nguyen-formalverificationofaredblacktreedatastructure-2019","authorIDs":[],"author_short":["Nguyen, i. H."],"bibdata":{"bibtype":"misc","type":"misc","month":"March","author":[{"firstnames":["ir.","H.M."],"propositions":[],"lastnames":["Nguyen"],"suffixes":[]}],"year":"2019","title":"Formal verification of a red-black tree data structure","url":"http://essay.utwente.nl/77569/","abstract":"Nowadays, although software has been integrated deeply into our society, software errors are still common. Because the failure of software can have devastating effects, being certain that a program does what it is meant to do is crucial. This thesis conducts a case study in deductive verification, which is a sub-area of formal verification. The case study involves a company in the Netherlands and their industrial red-black tree code. This thesis is intended to be an experience report to show how formal verification can be used to help proving the correctness of a program. Ultimately, we want to be able to verify the industrial red-black tree code. However, in this thesis, we only cover the verification of a standard red-black tree code. The main section presents how specifications of a red-black tree can be developed, and the obstacles that are met during the development. Finally, we conclude with the comparisons with the results of other authors and possible future work.","bibtex":"@misc{essay77569,\n month = {March},\n author = {ir. H.M. {Nguyen}},\n year = {2019},\n title = {Formal verification of a red-black tree data structure},\n url = {http://essay.utwente.nl/77569/},\n abstract = {Nowadays, although software has been integrated deeply into our society, software errors are still common. Because the failure of software can have devastating effects, being certain that a program does what it is meant to do is crucial. This thesis conducts a case study in deductive verification, which is a sub-area of formal verification. The case study involves a company in the Netherlands and their industrial red-black tree code. This thesis is intended to be an experience report to show how formal verification can be used to help proving the correctness of a program. Ultimately, we want to be able to verify the industrial red-black tree code. However, in this thesis, we only cover the verification of a standard red-black tree code. The main section presents how specifications of a red-black tree can be developed, and the obstacles that are met during the development. Finally, we conclude with the comparisons with the results of other authors and possible future work.}\n}\n\n\n\n","author_short":["Nguyen, i. H."],"key":"essay77569","id":"essay77569","bibbaseid":"nguyen-formalverificationofaredblacktreedatastructure-2019","role":"author","urls":{"Paper":"http://essay.utwente.nl/77569/"},"metadata":{"authorlinks":{}},"downloads":2},"bibtype":"misc","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","creationDate":"2020-03-11T13:41:07.971Z","downloads":2,"keywords":[],"search_terms":["formal","verification","red","black","tree","data","structure","nguyen"],"title":"Formal verification of a red-black tree data structure","year":2019,"dataSources":["2tJugFYAignELAmZo","zT4KxAXTKvhK2Hrr4","cCvCnPTRQYq3qPe9y"]}