Closer to Reliable Software: Verifying Functional Behaviour of Concurrent Programs

Marina Zaharieva Stojanovski

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

198 Downloads (Pure)

Abstract

If software code is developed by humans, can we as users rely on its absolute correctness? Today's software is large, complex, and prone to errors. Although many bugs are found in the process of testing, we can never slaim that the delivered software is bug-free. Errors still occur when software is in use; and errors exist that will perhaps never occur. Reaching an absolute zero bug state for usable software is practically impossible. On the other side we have mathematical logic, a very powerful machinery for reasoning and drawing conclusions based on facts. The power of mathematical logic is certainty: when a given statement is mathematically proven, it is indeed absolutely correct. When a technique for verifying software is based on logic, it allows one to mathematically prove properties about the program. These so-called formal verification techniques are very challenging to develop, but what they promise is highly valuable, and so, they certainly deserve close research attention. This thesis shows the benefits and drawbacks of this style of reasoning, and proposes novel techniques that respond to some important verification challenges. Still, mathematical logic is theory, and software is practice. Thus, formal verification can not guarantee absolute correctness of software, but it certainly has the potential to move us much closer to reliable software.
Original languageEnglish
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • Huisman, Marieke , Supervisor
Thesis sponsors
Award date1 Oct 2015
Place of PublicationEnschede
Publisher
Print ISBNs978-90-365-3924-1
DOIs
Publication statusPublished - 1 Oct 2015

Fingerprint

Formal logic
Machinery
Testing
Formal verification

Keywords

  • METIS-311738
  • EWI-26315
  • IR-97206

Cite this

Zaharieva Stojanovski, Marina. / Closer to Reliable Software : Verifying Functional Behaviour of Concurrent Programs. Enschede : Universiteit Twente, 2015. 236 p.
@phdthesis{387112e9c2624b91a29c188ef9adcb23,
title = "Closer to Reliable Software: Verifying Functional Behaviour of Concurrent Programs",
abstract = "If software code is developed by humans, can we as users rely on its absolute correctness? Today's software is large, complex, and prone to errors. Although many bugs are found in the process of testing, we can never slaim that the delivered software is bug-free. Errors still occur when software is in use; and errors exist that will perhaps never occur. Reaching an absolute zero bug state for usable software is practically impossible. On the other side we have mathematical logic, a very powerful machinery for reasoning and drawing conclusions based on facts. The power of mathematical logic is certainty: when a given statement is mathematically proven, it is indeed absolutely correct. When a technique for verifying software is based on logic, it allows one to mathematically prove properties about the program. These so-called formal verification techniques are very challenging to develop, but what they promise is highly valuable, and so, they certainly deserve close research attention. This thesis shows the benefits and drawbacks of this style of reasoning, and proposes novel techniques that respond to some important verification challenges. Still, mathematical logic is theory, and software is practice. Thus, formal verification can not guarantee absolute correctness of software, but it certainly has the potential to move us much closer to reliable software.",
keywords = "METIS-311738, EWI-26315, IR-97206",
author = "{Zaharieva Stojanovski}, Marina",
year = "2015",
month = "10",
day = "1",
doi = "10.3990/1.9789036539241",
language = "English",
isbn = "978-90-365-3924-1",
series = "IPA Dissertation Series",
publisher = "Universiteit Twente",
number = "2015-21",
school = "University of Twente",

}

Closer to Reliable Software : Verifying Functional Behaviour of Concurrent Programs. / Zaharieva Stojanovski, Marina.

Enschede : Universiteit Twente, 2015. 236 p.

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

TY - THES

T1 - Closer to Reliable Software

T2 - Verifying Functional Behaviour of Concurrent Programs

AU - Zaharieva Stojanovski, Marina

PY - 2015/10/1

Y1 - 2015/10/1

N2 - If software code is developed by humans, can we as users rely on its absolute correctness? Today's software is large, complex, and prone to errors. Although many bugs are found in the process of testing, we can never slaim that the delivered software is bug-free. Errors still occur when software is in use; and errors exist that will perhaps never occur. Reaching an absolute zero bug state for usable software is practically impossible. On the other side we have mathematical logic, a very powerful machinery for reasoning and drawing conclusions based on facts. The power of mathematical logic is certainty: when a given statement is mathematically proven, it is indeed absolutely correct. When a technique for verifying software is based on logic, it allows one to mathematically prove properties about the program. These so-called formal verification techniques are very challenging to develop, but what they promise is highly valuable, and so, they certainly deserve close research attention. This thesis shows the benefits and drawbacks of this style of reasoning, and proposes novel techniques that respond to some important verification challenges. Still, mathematical logic is theory, and software is practice. Thus, formal verification can not guarantee absolute correctness of software, but it certainly has the potential to move us much closer to reliable software.

AB - If software code is developed by humans, can we as users rely on its absolute correctness? Today's software is large, complex, and prone to errors. Although many bugs are found in the process of testing, we can never slaim that the delivered software is bug-free. Errors still occur when software is in use; and errors exist that will perhaps never occur. Reaching an absolute zero bug state for usable software is practically impossible. On the other side we have mathematical logic, a very powerful machinery for reasoning and drawing conclusions based on facts. The power of mathematical logic is certainty: when a given statement is mathematically proven, it is indeed absolutely correct. When a technique for verifying software is based on logic, it allows one to mathematically prove properties about the program. These so-called formal verification techniques are very challenging to develop, but what they promise is highly valuable, and so, they certainly deserve close research attention. This thesis shows the benefits and drawbacks of this style of reasoning, and proposes novel techniques that respond to some important verification challenges. Still, mathematical logic is theory, and software is practice. Thus, formal verification can not guarantee absolute correctness of software, but it certainly has the potential to move us much closer to reliable software.

KW - METIS-311738

KW - EWI-26315

KW - IR-97206

U2 - 10.3990/1.9789036539241

DO - 10.3990/1.9789036539241

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-365-3924-1

T3 - IPA Dissertation Series

PB - Universiteit Twente

CY - Enschede

ER -

Zaharieva Stojanovski M. Closer to Reliable Software: Verifying Functional Behaviour of Concurrent Programs. Enschede: Universiteit Twente, 2015. 236 p. (IPA Dissertation Series; 2015-21). (CTIT Ph.D. Thesis Series; 15-375). https://doi.org/10.3990/1.9789036539241