Dynamic logics (DL) are mutli-modal logics, where modalities are parameterised over actions from some action language. The action language may be a programming language, or consist of system (or component) level steps, or of environment moves. In this talk, I introduce principles of DL, and show how DL based verification can be practically used to analyse safety and other properties on various levels of computer-based systems.

Wolfgang Ahrendt received his Ph.D. in Computer Science from the University of Karlsruhe, Germany, in 2001, and is currently Professor at Chalmers University of Technology, Gothenburg, Sweden. His contributions lie in deductive verification of software, runtime verification, and combinations of static verification with runtime verification and testing. Wolfgang Ahrendt is one of the people behind the software verification approach and system ‘KeY’. Recent application areas of his work include automotive software safety, smart contracts and, most recently, AI assisted development of robust software.