MODELS FOR SOFTWARE VERIFICATION: PROVING PROGRAM CORRECTNESS

Boro Sitnikovsk, Lidija Goracinova-Ilieva and Biljana Stojcevska
Additional contact information
Boro Sitnikovsk: University of Tourism and Management in Skopje, North Macedonia
Lidija Goracinova-Ilieva: University of Tourism and Management in Skopje, North Macedonia
Biljana Stojcevska: University of Tourism and Management in Skopje, North Macedonia

UTMS Journal of Economics, 2021, vol. 12, issue 1, 32-39

Abstract: Abstract: The accuracy of computer systems represents the property that they are working as the users expect. Very often, these computer systems give inaccurate or wrong results. However, designing correct computer systems is a complex and expensive task. There are several ways to deal with this problem. In practice, the most common approach is to design and perform tests. However, these tests can only detect a specific set of problems. Another (more expensive) approach is to do a formal proof of correctness for a given code. This proof of correctness is, in fact, mathematical proof that the software works according to given specifications. Mathematical evidence covers all possible cases, and it is this evidence that confirms that code does exactly what it is intended to do. There are several platforms and mathematical models for software verification. Formal verification is based on mathematical proofs, and these platforms are divided into manual and automatic. Among the manual proof verification software, some of the most known ones are the programming languages Coq (based on type theory), Idris, etc. These are manual theorem provers, as the proof must be handwritten. Another family of theorem provers is the so-called automatic provers, which use algorithms to automatically deduce a given theorem. The programming language Dafny is one of their best representatives. This paper aims to show the state-of-the-art tools used today.

Keywords: software verification; software verification models; software verification platform (search for similar items in EconPapers)
JEL-codes: M42 M49 (search for similar items in EconPapers)
Date: 2021
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://utmsjoe.mk/files/Vol.12.No.1/3.MODELS_FOR_ ... GRAM_CORRECTNESS.pdf Full text (application/pdf)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:ris:utmsje:0303

Access Statistics for this article

UTMS Journal of Economics is currently edited by Prof. Ace Milenkovski, PhD

More articles in UTMS Journal of Economics from University of Tourism and Management, Skopje, Macedonia Contact information at EDIRC.
Bibliographic data for series maintained by Assistant Professor. Dejan Nakovski, PhD ().