published: April 16, 2009, recorded: February 2009, views: 745
Report a problem or upload filesIf you have found a problem with this lecture or would like to send us extra material, articles, exercises, etc., please use our ticket system to describe your request and upload the data.
Enter your e-mail into the 'Cc' field, and we will keep you updated with your request's status.
Watch videos: (click on thumbnail to launch)
Dynamic Logic was developed in the late 1970s by David Harel building on previous work by V.R.Pratt. It is a modal logic and as any modal logic it allows to reason about the truth of statements in different states (or worlds). It extends classical modal logic however by taking explicitly into account the transitions from one state to the next state(s). Descriptions of actions (events, or programs) are part of the syntax of Dynamic Logic. This course will start with an introduction into the logical theory of propositional and first-order dynamic logic with respect to a very fine grained notion of actions. At the next level a Dynamic Logic for an abstract programing language will be considered. We will end by presenting a Dynamic Logic for a real programming language and show how this can be used in software verification including a demo of a working system.
Link this pageWould you like to put a link to this lecture on your homepage?
Go ahead! Copy the HTML snippet !