Abstract

Ever since the first computer programs were written, programming errors have been a fundamental problem for developers as well as users. They cause computers to crash, medical equipment to malfunction and rockets to explode. To make sure that a program is free of error, one can run it to test if it behaves correctly. In practice however, programs have infinitely many possible inputs and behaviours. Alternatively one can try to formally verify by rigorous mathematics that a program is correct. To give this a sound basis, one has to formally define what a program (of a certain programming language) is and what it actually does. In my talk I will explain how this can be done and give an overview of the general research area.