Computer Science Summer in Russia (CSSR)

1. Introduction to Program Semantics: Motivation

1.1. What is Semantics?

1.2. Why Formal Program Semantics?

1.3. Operational, denotational, and axiomatic semantics for an esoteric language

2. Formal semantics for a Toy Programming Language

2.1. Data Types and Their Semantics

2.2. The main ingredient: Implementation Semantics

2.3. Structural Operational Semantics

2.4. Relational Denotational Semantics

2.5. Axiomatic Semantics

3. Second-Order Semantics

3.1. Introduction to Higher-Order Logic

3.2. Second-order semantics for esoteric language

3.3. The Weakest Precondition Semantics for a Toy Programming Language

4. Elements of λ-Calculus and Classical Denotational Semantics

4.1. Syntax, Semantics and Main Properties of λ-Calculus

4.2. Denotational Semantics of a Toy Programming Language

5. Conclusion: Formal Semantics – a Gateway to Formal Verification

5.1. Example of semantics for advanced features– Calculus of Aliasing

5.2. Example of formally verified software – Mars Code

6. Lab topics (optional home tasks). Working with an esoteric programming language:

6.1. Implementation and visualization of the operational semantics

6.2. Implementation and visualization of the denotational semantics

6.3. Implementation and visualization of the second-order semantics

6.4. Implementation of the axiomatic semantics

Visualization of the axiomatic semantics

Basic programming skills,
fundamentals of set theory,
propositional logic (syntax and truth tables),
and first-order logic (syntax and the notion of model)

English or Russian depending on the audience preferences

The students are not expected to know anything in the area in advance. Knowledge of discrete mathematics (sets, relations, proofs by induction, boolean algebra, logical predicates) is required.

Knowledge of any functional programming language (Haskell, OCaml, F#, Clojure) is a plus but is not required.

Russian

- Modern Testing Techniques

• Triple-V model of testing and verification;
• Developing sample system with the TDD approach;
• Developing sample system with the BDD approach;
• Spec Explorer in action: generation of unit-tests by a given behavior automaton.

- Formal Verification in Action

• Purpose of verification;
• Verification of actor-based systems and protocols with Spin;
• An Example of solving search problems in Spin: Hanoi Towers;
• Contract based programming with the MS Contracts approach.

- Formal Verification in Action (2)

• The Weakest Precondition approach and verification of C programs with Frama-C;
• Cyber-Physical Systems: issues of definition and verification;
• Introduction to CPS verification: verification systems from various domains.

Russian

Basic knowledge of algorithms and data structures, and mathematical logic at the bachelor level.

Russian

- Introduction

• The infinite state problems from recreational mathematics tackled by FCM: Fibonacci words and MUpuzzle
• Origins of the method and early work in security analysis
• Generic requirements for FO logic encodings used in the method

- FCM for the classes of infinite state and parameterized problems

decision procedure for the safety of lossy channel systems
verification of parameterized cache coherence protocols
verification of string and term rewriting systems
linear systems of automata and mutual exclusion protocols

- Relative completeness

For proving safety, the FCM method is as powerful as any method using regular invariants, e.g.:

• regular model checking
• regular tree model checking
• tree automata completion

- Limitations and challenges

Restrictions caused by regular invariants.

• Simple tasks, for which FCM does not work, as it requires nonregular invariants.
• Tasks, for which FCM is good in theory, but is slow in practice.
• Can we improve FCM? Open problems to explore.

Russian or English depending on the audience preferences

- Repetition of logical foundations

• propositional, first-order, and dynamic logic

- Control theory based on examples

• plant model, controller, implementation as formulated in MatlabSimulink(R)

- Current quality assurance techniques for control software

• simulation

- Hybrid automata as realized by theorem prover KeYmaera

• tiny examples
• calculus rules (also for handling ordinary differential equations (ODEs))

- Using Domain-Specific Languages to bridge MatlabSimulink(R) to hybrid automata

• defining a DSL in syntax with XText
• implement generator for proof obligations
• visualize results

- The one-tank model as running example

Basic knowledge of (some) logics (e.g., propositional, first-order, or modal):
syntax, semantics, sequent calculus

English

During the first lecture we will have a look at the world around us and pinpoint places, where software languages and compilers exist, emerge, and operate, shifting the focus from traditional compilers to domain-specific languages and language workbenches. We will also have a brief overview of tools that people who are not necessarily system programmers can use to automate tedious and error-prone tasks of language processing, like configuration files handling or dealing with XML and JSON.

The second lecture will be rather technical and will go deeper into the actual techniques that have either emerged or have been improved during the last decade, including grammar extraction, convergence, adaptation, bidirectional transformation, testing, deployment, etc.

The last lecture will highlight a few areas that still deserve much attention, and will be mostly interesting for BSc/MSc/PhD students searching for an inspiring research topic.

Outline

• Grammarware as the future of compilers

• Language workbenches and other advanced tools

• Domain-specific and fourth generation languages

• Software language engineering

• Language design with intent

• Modern parsing algorithms: GLL, ALL(*), SGLR, Packrat

• Semi-parsing, error recovery, graceful degradation

• Parsing in a broad sense

• Grammar extraction and recovery

• Grammar quality and grammar smells

• Grammar equivalence and convergence

• Code generation with frameworks

• Bidirectional and coupled transformations

• Semantics and interpretation

• Meta-programming, analysis, and comprehension

• Between interpretation and compilation

• Compiler testing and fuzzing

• Language documentation

• Compiler deployment and integration

• Machine learning in compiler construction

• Open problems of the future

Either a finished BSc in Computer Science or Software Engineering,
or a completed compiler construction / formal language course.

English or Russian depending on the audience preferences

In the lecture, we will focus on the most interesting and actual topics:

- The background of the Uma.Tech company;

- Solution Development and how Data Science helps in creating new solutions;

- The popular CRISP-DM methodology;

- We will describe a solution to a real-world problem of predicting user drop-off based on a proposed process model.

At the end of the lecture, you will be provided a ''home task''.

no special prerequisites

Russian

1. Logic Tools of Ontology Modeling

• Justification of logic as a formalization tool for ontologies. Basics of Description Logics EL and ALC: syntax and semantics. Basic reasoning problems: ontology consistency, concept satisfiability, concept disjointness. The problem of concept classification. Terminologies and expansions.

2. Automated Reasoning in Description Logics.

• The complexity of reasoning in the logic EL. The complexity of concept satisfiability in ALC wrt the empty and a non-empty ontology. The relationship between the expressiveness and complexity of a logic. Consequence-based calculus for EL. Tableaux for ALC.

3. Automated Reasoning for Explaining Ontology Properties

• The problem of inconsistency explanation. Minimal justifications and maximal counterexamples for an inference. The number of minimal justifications for an inference in the logic EL, the complexity of finding a justification of a given size.
• Glass-box approach to computing justifications by modifying the reasoning procedure. Reducing computation of minimal justifications in EL to SAT (the satisfiability problem for boolean formulas). The search for minimal justifications with a modification of tableaux for ALC.
• Black-box approach to computing justifications without modifying the reasoning procedure.

4. Computing concept definitions in ontologies

• Explicit and implicit concept definitions. The number and the size of pairwise incomparable shortest concept definitions in the logics EL and ALC. Relationship between definitions and minimal justifications.
• Extracting concept definitions from proofs. Computing concept definitions with a modified consequence-based reasoning procedure for EL. Rewriting ontologies with explicit definitions.

Basic knowledge of any formal logic (syntax and semantics).

English or Russian depending on the audience preferences

Ontology-based data access (OBDA) is regarded as a key ingredient of the new generation of information systems. In the OBDA paradigm, an ontology defines a high-level global schema of (already existing) data sources and provides a vocabulary for user queries. An OBDA system rewrites such queries and ontologies into the vocabulary of the data sources and then delegates the actual query evaluation to a suitable query answering system such as a relational database management system.

This course will start with the overview of ideas and technologies that led to OBDA such as RDF-graphs, SPARQL queries, linked data, knowledge representation and description logics. Then we focus on OBDA with OWL 2 QL, one of the three profiles of the W3C standard Web Ontology Language OWL 2, and relational databases. We finish with a hands-on session with the OBDA system Ontop.

There are no hard prerequisites for the course. However, the students with a background in formal logic will feel more comfortable than those without.

Also a basic experience with SQL is desirable for the hands-on session where it will be used for mapping a relational database on the ontology vocabulary.

English or Russian depending on the audience preferences

In this course you will learn about principles, methods, and basic problems in automated reasoning. The development of logic methods and automated reasoning tools has begun right from the beginning of the computer era. For instance, Lisp, one of the first high-level programming languages, can be viewed as an implementation of the lambda-calculus. Later history has evidenced the rise and fall of applications of logic in Information Technologies. Nowadays, this topic is again at the top, which is due to applications for program, protocol, and system verification, knowledge analytics, and data processing. Recently, there have appeared numerous automated reasoning tools for solving these tasks.

Basics of discrete mathematics: sets, relations, proof by induction, Boolean algebra, logic predicates.
Understanding of the concept of imperative program.

Russian, with slides in English

This course is on Applied Automated Reasoning. We will present recent developments in the application of automated reasoning (AR) methods and techniques, such as automated theorem (dis)proving and SAT solving, in Experimental Mathematics.

We will consider applications of AR in computational topology (knot theory), combinatorial number theory, and combinatorial group theory.

1. In the first part of the course we will present a recent application of automated reasoning to (un)knot detection, which is a classical problem in computational topology.


- We will show that the problem can be equivalently reformulated as a task of proving/disproving a first-order formula, which specifies the properties of a quandle, an algebraic invariant of the knot.

- We will adopt a two-pronged experimental approach, using a theorem prover to try to establish a positive result (i.e., that a knot is the unknot), whilst simultaneously using a model to try to establish a negative result (i.e., that the knot is not the unknot). The theorem proving approach utilises equational reasoning, whilst the model finder searches for a minimal size counter-model.

- We will further show that by using explicit knowledge of existing quandle families one can reformulate the disproving task in terms of quandle colourings and reduce it to a SAT solving problem, which in turn can be tackled very efficiently by off-the-shelf SAT solvers. This leads to the empirically most efficient non-trivial knot recognition procedure.

We will further discuss using different algebraic structures (such as knot semigroups) or topological objects (tangles) in the automated reasoning about knots trading efficiency of the proofs for their transparency.


2. In the second part of the course we will overview the results related to the Erdos Discrepancy Problem.

In the 1930s, Paul Erdos conjectured that for any positive integer C in any infinite sequence (x_n) consisting of numbers 1 and -1, there exists a subsequence x_d, x_{2d}, x_{3d},\dots, x_{kd}, for some positive integers k and d, such that the absolute value of the sum of the elements of the subsequence is greater than C. The conjecture has been referred to as one of the major open problems in combinatorial number theory and discrepancy theory.

For the particular case of C=1 a human proof of the conjecture existed; for C=2 the status of the conjecture remained open until March 2014. We show that by encoding the problem into the Boolean satisfiability and applying the state of the art SAT solver, one can prove the conjecture for C=2 using a subsequence of length 1160. These results appeared in 2014-2015. Later, in autumn 2015, the general case of EDP was solved by Terence Tao, not using automated reasoning or any other computational approach.

3. In the third part of the course, we will present the applications of the automated theorem proving to the exploration of the open Andrews-Curtis conjecture in the combinatorial group theory. The approach employs generic proof search for the search of simplifications implied by the conjecture in a very efficient way, outperforming all known specialized algorithms.

The course is suitable for people with some mathematical background, including familiarity with abstract algebra (at least definitions of groups/semigroups).

Less classical concepts (quandles, tangles, etc) will be defined during the course and should be accessible for the mathematically curious audience.

The familiarity with automated theorem proving, SAT solving is useful, but not crucial.

English or Russian depending on the audience preferences

In this course, you will learn to apply the Deep Learning techniques to a range of Computer Vision tasks through a series of hands-on exercises. You will work with widely-used Deep Learning tools, frameworks, and workflows to train and deploy neural network models on a fully-configured GPU accelerated workstation in the cloud.

After a quick introduction into the Deep Learning, you will learn how to build and deploy Deep Learning applications for image classification and object detection and how to tune neural networks to improve their accuracy and performance. Finally, you will implement this workflow in a project, which combines Machine Learning and conventional Software Development techniques. After the course you will provided with access to additional resources to create Deep Learning applications on your own.

Upon successful completion of this course, you will obtain a NVIDIA DLI Certification.

Familiarity with programming basics such as functions and variables

English or Russian depending on the audience preferences

This course presents a unique Machine Learning method, which has been developed in the Novosibirsk Scientific Center and has proved to be useful in solving numerous practical tasks. In the first part of the course, we will introduce the basics of the logic-and-probabilistic method of Knowledge Discovery and compare it with other methods for Data Analysis. We will consider an algorithm of the Semantic Probabilistic Inference, which is at the core of the method. Finally, we will give examples of real-world problems, which are solved with this approach.

The second part will be devoted to the application of the method in Adaptive Control. We will first introduce you to the fundamentals of Reinforcement Learning and then give examples of logic-and-probabilistic models of self-learning control systems based on neurophysiological theories of brain activity. In the concluding part, we will address the control problem for hyper-redundant and modular robots.

• Introduction to the logic-and-probabilistic method of Data and Knowledge Mining

• Use cases for Knowledge Mining and prediction for various subject domains

• Hierarchical control systems based on the modern neurophysiological theories of brain activity

• The control problem in hyper-redundant and modular robotics

Basic knowledge of logic and probability (logic predicates, boolean operators, the notion of probability).

Russian