## Homepage of Dr. Nikolay V. Shilov |

## 1. Personal DataDate of Birth: April 24, 1961 Mailing address: A.P. Ershov Institute of Informatics Systems Lavrentev av., 6, Novosibirsk, 630090, Russia, ## 2. SummaryMy research interests are around Theory, Logic, and Formal Methods in Computer Science, Software Engineering, and Information Technology. I am experienced in theory of program logics and algorithms for reasoning about program systems. I have a sound knowledge of Formal Description Techniques (FDT) for distributed systems. I also have research experience with design, implementation and use of model checking algorithms in formal verification of FDT-specifications. Recently my research interests expanded to theory of knowledge representation, processing, and reasoning, multiagent systems and distributed algorithms, computer languages ontology and methodology. I have more than 30 years of experience in Applied Logic: dynamic logic, temporal logic, logic of knowledge, description logic, etc. I am especially interested in algorithmic problems (i.e. model checking, decidability, and axiomatization) for propositional versions of these logics. The main application areas of my theoretical research are formal methods, formal ontologies (for example, for classification of Computer Languages), knowledge representation and reasoning formalisms (like Formal Concept Analysis, Description and Epistemic Logics), distributed and multiagent systems. I have more than 23 years of teaching experience (including 7 years oversees) in Computer Science (in particular in Algorithms, Program Languages and Theory), in Discrete Mathematics (especially in Mathematical Logic) at different levels (college, undergraduate, graduate, and postgraduate). I am very much interested in different programming contests and Olympiads for students. In particular I am involved into organization of regional competitions of this kind. I also have supervisor/adviser experience at undergraduate, graduate, and postgraduate levels. I like very much popularization of Computer Science and Mathematical Logic among high school pupils and undergraduate students. I have teaching experience with higher education systems in Australia, New Zealand, South Korea, Kazakhstan (a bland of British/American systems) and Russia (very traditional European- styled system). I have published more than 100 articles, papers and reports: 9 papers have been published in journals indexing by Web of Science and/or Scopus (in particular, in Communications of ACM), more than 40 in proceedings of peer review International conferences and workshops (including >20 papers proceedings indexed by Scopus, in Lecture Notes in Computer Science in particular). Many times I participated in International Program Committees, organized several national and international workshops, have delivered invited talks at international level. ## 3. Affiliation:Institute of Informatics Systems of Russian Academy of Science (IIS) (full time Senior Researcher position, A.P. Ershov INSTITUTE OF INFORMATICS SYSTEMS, ## 4. Selected Major Publications- Dissertations and Thesis
- Peer review journals (indexed by Web of Science and/or Scopus)
*Program schemata vs. automata for decidability of program logics*. Theoretical Computer Science, v. 175, 1997, p.15-27. (See draft.)- Specification and verification of distributed systems by means of Elementary-REAL. Programming and Computer Software, v.25, n.4, 1999, p.222-232 (with Nepomniaschy V.A. and Bodin E.V.)
*Engaging Students with Theory through ACM Collegiate Programming Contests*. Communications of ACM, v.45, n.9, 2002 (with Yi K.)*Update and Abstraction in Model Checking of Knowledge and Branching Time*. Fundameta Informaticae, v.72, n.1-3, 2006, p.347-361 (with Garanina N. O. and Choe K.-M.) (See draft.)*Generation of verification conditions for imperative programs*. Programming and Computer Software, v.34, n.6, 2008, p.307–321. (with Anureev I.S. and Bodin E.V.) (See draft.)*F@BOOL@: Experiment with a simple verifying compiler based on SAT-solvers*. Automatic Control and Computer Sciences, v.45, n.7, 2011, p.428-436.*Verification of Backtracking and Branch and Bound Design Templates*. Automatic Control and Computer Sciences, v.46, n.7, 2012, p.402–409.*Some Results on Multiagent Algorithms in Social Computing/Software Context*. Information, v.17, n.1, 2014, p.229-240 (with Satykbayeva A.) (See draft.)*Teaching Formal Models of Concurrency Specification and Analysis*. Modeling and Analysis of Information Systems. v.22, n.6, 2015, p.783-794.*Program Schemata Technique 30 Years After*. To appear in*Programming and Computer Software*, v.42, n.4, 2016, 24 p. (in Russian, with S.O. Shilova and A.Yu. Bernsain). See draft, 33 p.
- Peer review book chapters
*How to find a coin: propositional program logics made easy*. In Current Trends in Theoretical Computer Science, World Scientific, v. 2, 2004 p.181-214 (with Yi K.) (See a preliminary version published in The Bulletin of European Association for Theoretical Computer Science, v. 75, 2001.)*Modal Logics for reasoning about Multiagent Systems*. In Encyclopedia of Artificial Intelligence. J.R. Rabuсal, J. Dorado, A.P. Sierra, editors. Information Science Reference. 2008, p.1089-1094 (with N.O. Garanina).
- Current Drafts
- No current drafts...
- Proceedings of peer review International Conferences and Workshops
*Model Checking Knowledge and Time in Systems with Perfect Recall*. LNCS, v. 1738, 1999 (with van der Meyden R.)*On Expressive and Model Checking Power of Propositional Program Logics*. Proc. of int. Conf. Perspectives of System Informatics PSI’01, Russia, 2001, Springer LNCS, v.2244, 2001 (with Yi K.)*Basic-REAL: integrated approach for design, specification and verification of distributed systems*. Proc. of int. Conf. Integrated formal Methods IFM’02, Finland, 2002, Springer LNCS, v.2335, 2002 (with Nepomniaschy V.A. Bodin E.V. and Kazura V.E.)*Polynomial Approximations for Model Checking*. Proc. of int. Conf. Perspectives of System Informatics PSI’03, Russia, 2003, Springer LNCS, v.2890, 2004 (with Garanina N.)*Model Checking Mu-Calculus in Well-Structured Transition Systems*. Proc. of International Symposium Temporal Representation And Reasoning TIME’04, France, 2004, IEEE Press, 2004 (with Kouzmin E.V. and Sokolov V.A.)*Proofs about folklore: why model checking = reachability? MATHEMATICAL LOGIC IN ASIA, Proceedings of the 9th Asian Logic Conference*. Word Scientific Publishing Co., 2006, p.41-50 (with K.-M. Choe, H. Eo, S.-H. O, and K. Yi).*Well-structured Model Checking of Multiagent Systems*. Proceedings of 6th International Conference Perspectives of System Informatics, Springer Lecture Notes in Computer Science, v. 4378, 2006, p.351-365 (with N.O. Garanina).*A proposal of Description Logic on Concept Lattices*. Proceedings of the Fifth International Conference on Concept Lattices and their Applications, 2007. CEUR Workshop Proceedings, v.331, 2008, p.165-176. (with S.-Y. Han).*Combining Two Formalism for Reasoning about Concepts.*Proceedings of the 2007 International Workshop on Description Logics. CEUR Workshop Proceedings, v.250, 2007, p.459-466. (with Anureev I.S. and Garanina N.O.)*Realization Problem for Formal Concept Analysis*. Proceedings of the 21st International Workshop on Description Logics (DL2008). CEUR Workshop Proceedings, v.353, 2008.*Towards Description Logic on Concept Lattices*. Proceedings of International conference on concept lattices and their applications (CLA-2013, La Rochelle, France, October 15-18, 2013) CEUR Workshop Proceedings, v. 1062 p.287-292 (with J.V. Grebeneva and N.O. Garanina).*Algorithm Design Template base on Temporal ADT.*Proceedings of 18th International Symposium on Temporal Representation and Reasoning (12-14 September, 2011, Lubeck, Germany). IEEE Computer Society, 2011, p.157-162*Combined Logics of Knowledge, Time, and Actions for Reasoning about Multiagent Systems*. Knowledge Processing and Data Analysis. Lecture Notes in Computer Science, v.6581, 2011, p.48-58. (with Garanina N.O.)*Development of the Computer Language Classification Portal*. Proceedings of 8th International Conference Perspectives of System Informatics, Springer Lecture Notes in Computer Science, v.7162, 2012, p. 340-348 (with Akinin A.A., Zubkov A.V., Idrisov R.I.)*Agent Knowledge and Beliefs in a Cloud*. Post-proceedings of Kazakh-British workshop Embracing Global Computing in Emerging Economies (26-28 February 2015, Almaty, Kazakhstan). Springer series Communications in Computer and Information Science, vol. 514, 2015, p.11-20.*Program Scheme Technique to Solve Propositional Program Logics Revised*. To appear in post-proceedings of 10th Ershov Informatics Conference (PSI-2015, 25-27 August 2015, Innopolis, Kazan, Russia, a former International Conference Perspectives of System Informatics) to be published by Springer Lecture Notes in Computer Science, v.9609, 15 p. (See draft.)
- Books
- Introduction to Program Syntax, Semantics, Specification and Verification. Novosibirsk State University, 2012. (In Russian. See draft.)
- Other selected publications of recent years to represent current research activities not presented above
*SAT vs. SMV for automatic validation of tabular property of superintuitionistic logics*. Bulletin of Novosibirsk Computing Center, Special issue of A.P. Ershov Institute of Informatics Systems, Computer Science Series, v.25, 2006 (with Schreiner P.A. , Grebeneva J.V. and O S.).*Unifying Dynamic Programming Design Patterns*. Bulletin of the Novosibirsk Computing Center (Series: Computer Science, IIS Special Issue), v.34, 2012, p.135-156.*An approach to design of automata-based axiomatization for propositional program and temporal logics (by example of linear temporal logic)*. In: Logic, Computation, Hierarchies. Series:Ontos Mathematical Logic, v.4 Ontos-Verlag/De Gruyter, Germany, 2014, p.297-324.*Alias calculus for a simple imperative language with decidable pointer arithmetic*. Bulletin of the Novosibirsk Computing Center (Series: Computer Science, IIS Special Issue), v.37, 2014, p.131-147 (with Satekbayeva A., Vorontsov A.).*On the Need to Specify and Verify Standard Functions*Has been accepted for publication at Bulletin of the Novosibirsk Computing Center (Series: Computer Science, IIS Special Issue), v.39, 2015. (See draft.)
## 5. Current Teaching and Related Activities- since 2004 – Jury member of Open All-Siberian Programming Contests;
- Academic year 2014-15: graduate course on
*Formal Methods*at Mathematics and Machanics Department of Novosibirsk State University. (Joint course with N. Garanina, D. Ponamarev and course supervisor V. Shelekhov.) In 2016 the course was awarded by grant of*Vladimir Potanin Foundation*for new graduate courses and programs.
## 6. Service to Academia(Only current activities.) - Program Committee member of 25th International Joint Conference on Artificial Intelligence (New York City, 9th-15th July, 2016).
- Since 2009 - member of the Program Committee of
International workshops Program
Semantics, Specification & Verification: Theory and Application (PSSV).
**New**: This year the workshop will run June 14 & 15, 2016, in affiliation with the 11th*International Computer Science Symposium in Russia*(CSR-2016, June 9–13, 2016, St. Petersburg, Russia); submission deadline is April 16, 2016. - Since 2012 - member of the Program Committee of
Spring/Summer Young
Researchers' Colloquium on Software Engineering (SYRCoSE).
**New**: This year the workshop will run May 30 - June 01, 2016, in Krasnozavidovo (near Moscow, Russia); submission deadline is April 11, 2016. - Since 2008 – member of the Editorial Board of Computer Science and Telecommunications electronic journal, published by Georgian Technical University and St. Andrew the First Called Georgian University of The Patriarchy of Georgia.
## 7. Some people whom I work(ed) with and related research topics- Scientific Adviser of my Master and Ph.D. Thesis was Valery A. Nepomniaschy . In 1982-90 we developed Program Schemata Technique for Propositional Dynamic Logic.
- In 1990-2002 a focus of our collaboration with Valery A. Nepomniaschy moved to design of new FDT on base of program logics and to specification and verification of distributed systems.
- In 1998-99 we worked together with Ron van der Meyden on model checking knowledge and linear time logic.
- In 2000-05 we worked together with Kwang Yi on model checkers of program logics and better education on theory of Computer Science.
- Since 2002 we with Natalia Garanina study the model checking knowledge, actions, and branching time and their applications for reasoning about multiagent systems.
- In 2007-10 we worked together with Sang Yong Han on combination of Description Logic and Formal Concept Analysis for Knowledge Representation and Reasoning.
## 8. Former Master and Ph.D. students:- Mr. Peter Schneider;
- Dr. Sergey Berezin (alternative spelling: Berrezine);
- Mr. Evgeny Bodin.;
- Dr. Natalia Garamina;
- Dr. Aizhan Sateckbayeva.
## 9. Recent research projects in which I am/was involved
Updated by Nikolay V. Shilov |