Homepage of Dr. Nikolay V. Shilov

  

1. Personal Data

Date of Birth: April 24, 1961
Sex: Male
Family status: Married (4 sons, 2 daughters, and 1 wife;-)
Citizenship: Russia

Mailing address:
Innopolis University, 1, Universitetskaya Str., Innopolis, Republic of Tatarstan, 420500, Russia

Email: n.shilov@innopolis.ru, shiloviis@mail.ru, shilov@iis.nsk.su

Personal web-page: http://persons.iis.nsk.su/en/person/shilov
Official web-page: https://innopolis.university/professor/nikolay-shilov/ (In Russian)

Phone: +7 913 727 04 38

SCOPUS Author ID: 8403015400
ORCID Author ID: 0000-0001-7515-9647
ResearcherID: F-9116-2012
ResearchGate: https://www.researchgate.net/profile/Nikolay_Shilov3

Please refer Detailed CV if needed: CV_Shilov_N_V

2. Summary

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 multiagent systems.

I have more than 23 years of teaching experience (including 7 years overseas) 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 blend 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:

Innopolis University (full time Assitant Professor)

4. Selected Major Publications

Google Scholar: https://scholar.google.ru/citations?user=kEHqrCcAAAAJ&hl=en

DBLP entry: http://dblp.uni-trier.de/pers/hd/s/Shilov:Nikolay_V=

  1. Dissertations and Thesis
    1. Program Logics and their Applications. Ph.D. thesis (in Russian), Novosibirsk Computing Center of Siberian Branch of the Soviet Academy of Science, 1987
  2. Peer review journals (indexed by Web of Science and/or Scopus)
    1. Program schemata vs. automata for decidability of program logics. Theoretical Computer Science, v. 175, 1997, p.15-27. (See draft.)
    2. 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.)
    3. Engaging Students with Theory through ACM Collegiate Programming Contests. Communications of ACM, v.45, n.9, 2002 (with Yi K.)
    4. 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.)
    5. 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.)
    6. 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.
    7. Verification of Backtracking and Branch and Bound Design Templates. Automatic Control and Computer Sciences, v.46, n.7, 2012, p.402–409.
    8. Some Results on Multiagent Algorithms in Social Computing/Software Context. Information, v.17, n.1, 2014, p.229-240 (with Satykbayeva A.) (See draft.)
    9. Teaching Formal Models of Concurrency Specification and Analysis . Modeling and Analysis of Information Systems. v.22, n.6, 2015, p.783-794.
    10. Program schemata technique for propositional program logics: A 30-year history. Programming and Computer Software, v.42, n.4, 2016, p.239–256 (with S.O. Shilova and A.Yu. Bernsain). See draft, 33 p.
  3. Peer review book chapters
    1. 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.)
    2. 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).
  4. Current Drafts
    1. No current drafts...
  5. Proceedings of peer review International Conferences and Workshops
    1. Model Checking Knowledge and Time in Systems with Perfect Recall. LNCS, v. 1738, 1999 (with van der Meyden R.)
    2. 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.)
    3. 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.)
    4. 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.)
    5. 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.)
    6. 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).
    7. 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).
    8. 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).
    9. 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.)
    10. Realization Problem for Formal Concept Analysis. Proceedings of the 21st International Workshop on Description Logics (DL2008). CEUR Workshop Proceedings, v.353, 2008.
    11. 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).
    12. 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
    13. 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.)
    14. 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.)
    15. 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.
    16. 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.)
  6. Books
    1. Introduction to Program Syntax, Semantics, Specification and Verification. Novosibirsk State University, 2012. (In Russian. See draft.)
  7. Other selected publications of recent years to represent current research activities not presented above
    1. 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.).
    2. Unifying Dynamic Programming Design Patterns. Bulletin of the Novosibirsk Computing Center (Series: Computer Science, IIS Special Issue), v.34, 2012, p.135-156.
    3. 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.
    4. 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.).
    5. On the Need to Specify and Verify Standard Functions. Bulletin of the Novosibirsk Computing Center (Series: Computer Science, IIS Special Issue), v.38, 2015, p.105-119.
    6. Etude on recursion elimination. Modeling and Analysis of Information Systems. v.25(5), 2018, p.549–560.

5. Current Teaching and Related Activities

  • since 2004 – Jury member of Open All-Siberian Programming Contests;
  • undergraduate course on Probability & Statistics, on Calculus for Software Engineers, on Differential Equations, on Digital Signal Processing, and undergraduate & graduate courses on Discrete Mathematics & Logic at Innopolis University.

6. Service to Academia

(Only current activities.)

  1. Program Committee member of FM 2019, the 23rd international symposium in a series organized by Formal Methods Europe (FME), October 7-11, 2019, Porto, Portugal.
  2. Since 2009 - member (since 2016 - co-chair) of the Program Committee of International workshops Program Semantics, Specification & Verification: Theory and Application (PSSV).
  3. Since 2012 - member of the Program Committee of Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE).

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. Current research projects (in which I am involved) with external funding

Title Performing Institution Duration Sponsor Principal Investigator Responsibility
Research on Platform-independent approach to formal specification and verification of standard mathematical functions A.P. Ershov Institute of Informatics Systems 2017-2019 Russian Basic Research Foundation Me General management and research.
Research on Methods for generation of formal models and requirements from technical documentation presented in a natural language and their verification A.P. Ershov Institute of Informatics Systems 2017-2019 Russian Basic Research Foundation Natalya O. Garanina Research on logics for formal specifications.

Updated by Nikolay V. Shilov
December 30, 2018