Change search
ReferencesLink to record
Permanent link

Direct link
Explanation of Counterexamples in the Context of Formal Verification
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2016 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesis
Abstract [en]

With the current rapid computerisation and automation of systems, which were previously controlled manually, a growing demand for measures to ensure correctness of systems is arising. This can be achieved with formal verification. With formal verification, systems can be proved to satisfy, or not satisfy, a set of given properties. In cases where a system does not satisfy the given properties, a counterexample is presented, but counterexamples are, more often than not, hard to interpret manually. Thus, automatic procedures for explaining counterexamples are needed but unfortunately few. This thesis will focus on the explanation of counterexamples from failed formal verifications of systems. An algorithm for doing such is presented in this thesis. This algorithm is shown to give desired explanations for some cases whilst just the bare minimum for the majority of cases. A number of procedures to obtain the latter are already known. However, a small problem, left unsolved, can bring desired explanations to the majority of cases if solved. The presented algorithm is, unfortunately, not free from flaws nor errors, but it is still unclear how severe these are.

Place, publisher, year, edition, pages
2016. , 40 p.
Series
IT, 16051
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-301330OAI: oai:DiVA.org:uu-301330DiVA: diva2:954017
Educational program
Bachelor Programme in Computer Science
Supervisors
Examiners
Available from: 2016-08-19 Created: 2016-08-19 Last updated: 2016-08-31Bibliographically approved

Open Access in DiVA

fulltext(688 kB)13 downloads
File information
File name FULLTEXT01.pdfFile size 688 kBChecksum SHA-512
3ed9b7926c55a7ccffaadd039a8cf957c4969eb299c16be042cc2c16347bd0a858e625301cdec7c1ac24188f0e0a7c86aa62ce0fc4ed2dfadc0a8eed3c96e693
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 13 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 59 hits
ReferencesLink to record
Permanent link

Direct link