<div class="csl-bib-body">
<div class="csl-entry">Georgiou, P. (2019). <i>Trace Reasoning for formal verification : guiding vampire in induction</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.71683</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2019.71683
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/11483
-
dc.description
Decomposed Zeichen konvertiert!
-
dc.description.abstract
Automatisierte Softwareverifikation gewinnt durch die fortschreitende Digitalisierung zunehmend an Bedeutung. Unter diesem Licht widmet sich diese Masterarbeit der automatisierten Softwareverifikation mit Hilfe von automatisierten Beweissystemen in Prädikatenlogik. Insbesondere werden Programme mit Arrays und Schleifen hinsichtlich funktionaler Korrektheit für einfache, als auch relationale Spezifikationen untersucht. Vor allem werden relationale Eigenschaften typischerweise verwendet, um Sicherheits- und Datenschutzgarantien in Anwendungen der Systemsicherheit zu formulieren. Dies erfordert oftmals Quantorenalternierung. Für die Verifizierung dieser Eigenschaften werden imperative Programme auf ein Gültigkeits- problem in eine neue Logik, die sogenannte Trace Logic, reduziert. Durch Reasoningaktivitäten über natürliche und ganze Zahlen, erfordern automatisierte Beweise in dieser Logik auch induktive Schlüsse, die nur schwer automatisch vollzogen werden können. In diesem Sinne widmet sich diese Arbeit der Formulierung geeigneter Lemmata, genannt Trace Lemmas, die das automatische Beweissystem bei Schlüssen, die Induktion erfordern, leitet. Das Ziel der Arbeit ist es geeignete Sets an Trace Lemmas für verschiedene Eigenschaften zu definieren und zu formulieren, sodass automatisierte Beweise mit Hilfe des VAMPIRE-Beweissystems generiert werden können ohne von programmspezifischen Annotationen durch Experten abhängig zu sein.
de
dc.description.abstract
This work is motivated by automating reasoning for program analysis and verification in full first-order logic. We are interested in reachability and relational properties about functional correctness of programs with loops and arrays. Particularly, relational properties are typically used to formulate security and privacy guarantees in applications of system security, and often require reasoning about first-order formulas with quantifier-alternations. In our approach, we reduce the verification task of reachability and relational properties of imperative programs to a validity problem into a new logic, called trace logic, that is an expressive instance of first-order logic. Properties in trace logic involve reasoning about natural numbers and integers, and thus impose the burden of automating inductive reasoning in the full first-order setting of theorem proving. We address this challenge by automatically instantiating a set of so-called trace lemmas that guide first-order provers in inductive reasoning. The aim of this thesis is to identify a "reasonable" set of sound trace lemmas that allow superposition-based automated theorem provers to prove inductive (non-)relational properties, without relying on user-provided program annotations like program-specific loop invariants. To discharge verification conditions we rely on the first-order theorem prover Vampire.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
formal methods
de
dc.subject
software verification
de
dc.subject
system security
de
dc.subject
automated reasoning
de
dc.subject
first-order theorem proving
de
dc.subject
formal methods
en
dc.subject
software verification
en
dc.subject
system security
en
dc.subject
automated reasoning
en
dc.subject
first-order theorem proving
en
dc.title
Trace Reasoning for formal verification : guiding vampire in induction
en
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2019.71683
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Pamina Georgiou
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
dc.type.qualificationlevel
Diploma
-
dc.identifier.libraryid
AC15530600
-
dc.description.numberOfPages
58
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:1-131509
-
dc.thesistype
Diplomarbeit
de
dc.thesistype
Diploma Thesis
en
tuw.author.orcid
0000-0003-4856-4596
-
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
item.openaccessfulltext
Open Access
-
item.openairecristype
http://purl.org/coar/resource_type/c_bdcc
-
item.grantfulltext
open
-
item.mimetype
application/pdf
-
item.languageiso639-1
en
-
item.openairetype
master thesis
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering