<div class="csl-bib-body">
<div class="csl-entry">Hochrainer, C. (2020). <i>Automated reasoning over Arrays in the superposition calculus</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.77511</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2020.77511
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/15173
-
dc.description.abstract
Automated reasoning for program verification has made a lot of advancements in the past years. Nevertheless, one of the remaining challenges is automated reasoning over unbound data structures, in particular arrays, and programs manipulating them. In this thesis we will focus on program analysis and verification in full first-order logic. This work aims to provide theoretical basis to automate partial correctness proofs for software properties over integer arrays in the superposition calculus. Particularly, we are interested in properties of different quantifier settings: ∃, ∀ and ∀∃. Each of the chosen properties describe specific program behaviors that occur often in practice and are therefore important to prove. As foundation for this work we use the recently introduced trace logic, an instance of first-order logic and the framework Rapid, which provides the logical encoding of the programs. By using a generic property P, representing some property over arrays, we were able to generalize necessary lemmas and axiomatization of trace logic to produce more general proofs. These can be used to quickly instantiate a proof for a concrete property. With the insights gained throughout this work, we are now able to automate the proofs of the specific properties in general and concrete form, using the superposition-based theorem prover Vampire.
en
dc.description.abstract
In den letzten Jahren gab es enorme Fortschritte im Bereich automatisierter Softwareverifikation und Programmanalyse. Dennoch wurden einige Herausforderungen noch nicht vollständig bezwungen, sowie das automatisierte Verifizieren von unbeschränkten Datenstrukturen, insbesondere Arrays, und Programme, die diese manipulieren. In dieser Arbeiter konzentrieren wir uns auf die Programmanalyse und -verifizierung in vollständiger Logik erster Ordnung. Diese Arbeit soll theoretische Grundlagen für die Automatisierung von Beweisen zu partieller Korrektheit für Eigenschaften über ganzzahlige Arrays in dem Superposition Calculus liefern. Besonders interessieren uns hierbei Eigenschaften mit verschiedenen Quantifizierungen: ∃, ∀ und ∀∃. Jede der ausgewählten Eigenschaften beschreibt bestimmte Programmverhaltensweisen, welche häufig in der Praxis anzutreffen sind und es ist daher wichtig diese zu beweisen. Als Grundlage für diese Arbeit verwenden wir die erst kürzlich vorgestellte Trace-Logik, eine Instanz der Logik erster Ordnung, und das Framework Rapid, welches die logische Codierung der Programme liefert. Durch Verwendung einer generischen Eigenschaft P, die eine Eigenschaft über Arrays darstellt, wurden die notwendigen Lemma und die Axiomatisierung der Trace-Logik verallgemeinert und es konnten allgemeinere Beweise erstellt werden. Diese können nun verwendet werden, um Beweis für eine konkretisierte Eigenschaft zu instanziieren. Mit den durch die Beweise gewonnenen Erkenntnissen sind wir nun in der Lage automatisierte Beweise der Eigenschaften in allgemeiner oder konkretisierter Form, mit Hilfe des Superposition-basiertem Theorembeweiser Vampire, durchzuführen.
de
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
automated reasoning
de
dc.subject
program semantics
de
dc.subject
trace logic
de
dc.subject
invariants
de
dc.subject
first-order theorem proving
de
dc.subject
automated reasoning
en
dc.subject
program semantics
en
dc.subject
trace logic
en
dc.subject
invariants
en
dc.subject
first-order theorem proving
en
dc.title
Automated reasoning over Arrays in the superposition calculus
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.2020.77511
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Christoph Hochrainer
-
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
AC15692227
-
dc.description.numberOfPages
57
-
dc.thesistype
Diplomarbeit
de
dc.thesistype
Diploma Thesis
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.advisor.orcid
0000-0002-8299-2714
-
item.languageiso639-1
en
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_bdcc
-
item.fulltext
with Fulltext
-
item.openairetype
master thesis
-
item.grantfulltext
open
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E194-01 - Forschungsbereich Information und Software Engineering
-
crisitem.author.parentorg
E194 - Institut für Information Systems Engineering