A SURVEY ON PROBABILISTIC PROGRAM TERMINATION ANALYSIS

PhD Qualifying Examination


Title: "A SURVEY ON PROBABILISTIC PROGRAM TERMINATION ANALYSIS"

by

Mr. Sergei NOVOZHILOV


Abstract:

Formal verification is a branch of computer science focused on ensuring the 
correctness of software and hardware systems. Many programming tasks, such as 
machine learning, randomized algorithms, and cyber-physical systems, require 
programs to make probabilistic choices, posing challenges to traditional 
verification methods.

In this survey, we concentrate on a fundamental program property: whether a 
program completes its work on a given input in a finite number of steps. We 
describe two probabilistic versions of this property: almost sure termination 
(AST) and positive almost sure termination (PAST).

Further, we survey two types of results. The first type is devoted to proving 
methods for establishing whether a program possesses either property. Most 
proof rules are based on a combination of ranking functions and martingale 
theory.

The second type of results we consider involves complexity results, which 
establish the theoretical difficulty of deciding the AST or PAST properties.


Date:                   Tuesday, 3 September 2024

Time:                   4:00pm - 6:00pm

Venue:                  Room 5501
                        Lifts 25/26

Committee Members:      Dr. Amir Goharshady (Supervisor)
                        Dr. Sunil Arya (Chairperson)
                        Dr. Dimitris Papadopoulos
                        Prof. Pedro Sander