1. Personal Data
Date of Birth: April 24, 1961
Family status: Married (4 sons, 2 daughters, and 1 wife)
A.P. Ershov Institute of Informatics Systems Lavrentev av., 6, Novosibirsk, 630090, Russia,
Phone: +7 383 330 6253 Fax: +7 383 332 3494
Please refer Detailed CV if needed: cv-nikolayshilov.pdf
My 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
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-
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.
Institute of Informatics Systems of Russian Academy of Science (IIS) (full time Senior Researcher position, A.P. Ershov INSTITUTE OF INFORMATICS SYSTEMS,
Russian Academy of Sciences, Siberian Division
6, Acad. Lavrentjev pr., Novosibirsk 630090, Russia
Phone +7 383 3308652 Fax +7 383 3323494 e-mail: email@example.com)
4. Selected Major Publications
Proceedings of peer review International Conferences and Workshops
- Dissertations and Thesis
- Program Logics and their Applications. Ph.D. thesis (in Russian), Novosibirsk Computing Center of Siberian Branch of the Soviet Academy of Science, 1987
- 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.)
- 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...
- 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.
Other selected publications of recent years to represent current research activities not presented above
- Introduction to Program Syntax, Semantics, Specification and Verification. Novosibirsk State University, 2012.
(In Russian. See draft.)
- 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,
- 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.
5. Current Teaching and Related Activities
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
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:
9. Recent research projects in which I am/was involved
||A.P. Ershov Institute of Informatics Systems
||Russian Basic Research Foundation
|| Dr. M. Valiev
||Research on knowledge representation, reasoning,
privacy issues of
formal Models for
and alias calculus.
Updated by Nikolay V. Shilov
February 01 2016