Abstract
Original language  Undefined 

Awarding Institution 

Supervisors/Advisors 

Sponsors  
Date of Award  1 Oct 2015 
Place of Publication  Enschede 
Publisher  
Print ISBNs  9789036539241 
DOIs  
State  Published  1 Oct 2015 
Fingerprint
Keywords
 METIS311738
 EWI26315
 IR97206
Cite this
}
Closer to Reliable Software: Verifying Functional Behaviour of Concurrent Programs. / Zaharieva, M.
Enschede : Universiteit Twente, 2015. 236 p.Research output: Scientific › PhD Thesis  Research UT, graduation UT
TY  THES
T1  Closer to Reliable Software: Verifying Functional Behaviour of Concurrent Programs
AU  Zaharieva,M.
N1  IPA Dissertation Series No. 201521
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 bugfree. 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 socalled 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 bugfree. 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 socalled 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  METIS311738
KW  EWI26315
KW  IR97206
U2  10.3990/1.9789036539241
DO  10.3990/1.9789036539241
M3  PhD Thesis  Research UT, graduation UT
SN  9789036539241
PB  Universiteit Twente
ER 