RADICAL 2019

In her talk, Marieke Huisman will present an approach based on program annotations. She will briefly describe the fundamentals of annotation-based verification, and then discuss what is needed to use this approach for concurrent and distributed software. In particular, for concurrent and distributed software the program annotations have to take care of what part of the memory is affected by a thread or process. To take care of this, the program annotations will be based on concurrent separation logic. She will describe how this is done, and how reasoning about concurrent and distributed programs is supported by the VerCors verifier.

She will then also describe a further extension, which allows one to reason about behavioural properties of a concurrent or distributed program. She will show how to define an abstract model that captures the behaviour of the program. Program logic is then used to show that the program behaves as described by the abstract model, while model checking is used to reason about properties of the abstract model.

Short bio:

Marieke Huisman is a professor in Software Reliability at the University of Twente. She is well-known for her work on program verification of concurrent software. In 2011, she obtained an ERC Starting Grant, which she used to start development of the VerCors verifier, a tool for the verification of concurrent software. Currently, as part of her NWO personal VICI grant Mercedes, she is working on further improving verification techniques, both by enabling the verification of a larger class of properties, and by making verification more automatic. A main characteristic of the VerCors verifier is that it can reason about different kinds of concurrent programs. In particular, VerCors was originally developed to reason about Java programs, but it can also be used to reason about OpenCL kernels (for GPU), or to prove that compiler directives for parallellisation, such as in OpenMP, are correct. Moreover, VerCors can be also be used to reason about classical distributed programs.

Games have long been a mathematical model for social agency, for distributed computing, and for basic activities of argumentation and dialogue. In this lecture I explore the interface of games, agency and computation from a logical perspec-tive, and discuss some current issues that represent major broader challenges. Topics include the choice of structural equivalences for games (sequential and concurrent), the role of agent diversity in game play, and the tension between 'high' and 'low' rationality in classical versus evolutionary games. In addition to analysis, we will also consider the design of new games from a logical perspec-tive: as we shall see, ‘gamification’ has a long history in logic and mathematics. 

References (1) J. van Benthem, 2014, Logic in Games, The MIT Press, Cambridge MA. (2) J. van Benthem, 2018, 'Computation as Social Agency', Information and Computation 261:3, 519–535. (3) J. van Benthem & D. Klein, 2019, 'Logics for Analyzing Games', Stanford Electronic Encyclopedia of Philosophy.

Short bio:

Johan van Benthem is University Professor of Logic em. (Amsterdam), Henry Waldgrave Stuart Professor of Philosophy (Stanford), and Jin Yuelin Professor of Logic (Tsinghua University). He has worked in modal logic, epistemology/ philosophy of science, logic of natural language, time and space, and logics of information, computation and communication. His books include The Logic of Time (1983), Modal Logic and Classical Logic (1985), Language in Action (1991), Logical Dynamics of Information and Interaction (2011) and Logic in Games (2014). His current interests include interfaces of logic with the social and cognitive sciences, as well as with probability. Co-editor of the Handbook of Logic and Language (1997), Handbook of Modal Logic (2006), Handbook of Spatial Logics (2007), Handbook of the Philosophy of Information (2008). First director, Institute for Logic, Language and Computation (ILLC, University of Amsterdam, 1986–1998), co-director UvA-Tsinghua Research Center in Logic.