11th International Colloquium on Theoretical Aspects of Computing
17-19 September 2014, Bucharest, Romania

Free tutorial

We are pleased to announce that Jin Song Dong kindly offered to give a free tutorial on 16th of September 2014 between 17:00-19:00.

Jin-Song Dong

National University of Singapore, Singapore

Tutorial title:
Pervasive Model Checking

Abstract: Model checking has established as an effective method for automatic system analysis and verification. Popular model checkers like SPIN, SMV, and FDR are designed for specialized domains and are based on restrictive modelling languages. In this tutorial, we introduce the process analysis toolkit (PAT), which is a self-contained, extensible reasoning system for system specification, simulation, and verification. PAT currently supports a wide range of 20 different modeling formalism/languages, including CSP# (short for "communicating sequential programs," which is based on Hoare's CSP). The idea is to treat sequential terminating programs--which may indeed be C# programs--as internal events. The result is a highly expressive modeling language which covers many application domains. PAT has attracted more than 3000 registered users from 800+ organisations in 71 countries.

Bio: Jin-Song Dong received Bachelor (1st hon) and PhD degrees in Computing from University of Queensland in 1992 and 1996. From 1995 to 1998, he was research scientist at CSIRO in Australia. Since 1998 he has been in the School of Computing at the National University of Singapore (NUS) where he is currently Associate Professor. He is the deputy director of Singapore-French joint Research lab IPAL. Jin Song is on the editorial board of ACM Transaction on Software Engineering and Methodology and Formal Aspects of Computing. He has been general/program chair for a number of international conferences, including the general chair of 19th FM 2014 in Singapore. Jin Song has been a Visiting Fellow (2006) at Oxford University, UK, and a Visiting Professor (since 2009) at National Institute of Informatics, Japan. Outside of work, he plays competitive tennis and coaches top ranked junior players in Singapore (including his own 3 kids). He also developed Markov Decision Process (MDP) models for tennis strategy analysis in PAT with a special case study on Federer vs Nadal.

Please signal your intention to participate in the above tutorial, by sending an email to ictac2014@fmi.unibuc.ro with the subject "ICTAC tutorial".


The tutorial will be held at the Faculty of Mathematics and Computer Science, University of Bucharest - address: Str. Academiei nr. 14, 010014, Bucharest - 500 meters away (towards south) from the venue of the conference. Once you are in the building, go to the 3rd floor at lecture hall "Titeica".