Automated Software Verification with First-Order Theorem Provers
Profile picture for user Pamina Georgiou
Pamina Georgiou

Automated Software Verification with First-Order Theorem Provers

Förderjahr 2021 / Stipendien Call #16 / Stipendien ID: 5761

Automating formal methods is an ongoing effort in software verification necessary to conclusively prove that critical software infrastructure is error-free. Applications such as IoT, cloud computing and blockchain show that bugs can have severe implications on the safety and security of software. In this thesis, we propose trace logic to automate deductive verification of software using first-order theorem proving. Automated reasoning in trace logic helps to prove safety properties of while-like programs in full first-order logic with support for theories and sorts. Our aim is to extend the logical expressiveness of program semantics in trace logic, offering a fully automated and scalable approach towards reasoning-based software verification. Specifically, our project extends reasoning with trace logic to interprocedural analysis and concurrency to make automated verification of these technologies possible and thereby pushing the state-of-the-art in automated reasoning.

Uni | FH [Universität]

Technische Universität Wien

Themengebiet

Distributed Systems
,
Sicherheit | Privacy | Überwachung

Gesamtklassifikation

Dissertation | PhD

Lizenz

CC-BY-SA

Projektergebnisse

Zwischenbericht CC-BY-SA

Progress summary of recent developments and results on our work with trace logic and the Rapid verification framework.

Datenschutzinformation
Der datenschutzrechtliche Verantwortliche (Internet Privatstiftung Austria - Internet Foundation Austria, Österreich) würde gerne mit folgenden Diensten Ihre personenbezogenen Daten verarbeiten. Zur Personalisierung können Technologien wie Cookies, LocalStorage usw. verwendet werden. Dies ist für die Nutzung der Website nicht notwendig, ermöglicht aber eine noch engere Interaktion mit Ihnen. Falls gewünscht, treffen Sie bitte eine Auswahl: