et en

Non-standard semantics

Standard semantics attempt to capture the real-world behaviour of the program. We may allow some abstractions and approximations, but the idea is to stay true to the original meaning of the program. Non-standard semantics deliberately deviate and ascribe peculiar meanings to programs, meanings that are nevertheless useful for specific applications. In order to prove the correctness of static analyzers or program slicers, so called collecting semantics are used; these collect the set of all possible program states that may reach a given program point. Härmel Nestra has conducted research into transfinite semantics, which conceive programs as continuing execution beyond infinite loops! This is critical to prove the correctness of program transformations, such as slicing, that may eliminate non-terminating loops from the program.

In this context, you may explore which transfinite semantics can be used to prove the correctness of such transformations in the presence of various programming constructs, such as probabilistic statements, multi-threading, and recursion. This is a purely theoretical exploration and is well-suited to students who like mathematics and would like to view programming through a mathematical lens.

Contact: Härmel Nestra