Open License Society ______Only software can be perfect

• Ministry of Education and Science of Ukraine
• Open License Society, Belgium
• Kiev National Taras Shevchenko University
• National University “Kiev-Mohila Academy”
• Berdyansk State Pedagogical University
• Institute of Nanotechnologies and System Engineering

09 September 2007 – 16 September 2007

Official languages

Ukrainian, Russian, English (minimal level of English is required)

For participants from Ukraine and countries of former Soviet Union: 400 Grivna (equivalent of 80$), for students ‑ 200 Grivna (equivalent of 40$). Foreign participants: 200$.

The conference fee includes payment of organizational expenses (i.e. communication services, rent of a conference hall, computer classes and technical equipment), printed teaching materials, awards of lectors work, coffee-breaks and lunches during all teaching period.

Program

Sunday, 09 September            –          Arrival and settlement of participants.

Monday, 10 September till
Saturday, 15 September          –          Lectures and practical lessons.

Monday, 10 September           –          The evening – the social event foracquaintance, city excursion.

Saturday, 15 September          –          The evening – the social event for goodbye, sea excursion.

Time-table of School and Seminar:

10.09.2007      Plenary session: Formal methods in Software Engineering: motivation and examples of practical use.

11.09.2007      Formal languages for systems development: foundations and examples of practical use.

                          What is specification? Why specify a system? The base mathematical concepts (Sets, Predicate and Temporal Logic).
Writing a Specification. The Specification in TLA+.

12.09.2007      The TLA+ Language. The Syntax and Grammar of TLA+.
Temporal Formulas. The Lexemes and the Operators of TLA+.
The Operators of Set Theory. The Meaning of a State Function.
Action Operators. Temporal Operators.

Lector:             Peter Protsyk

13.09.2007      The TLA+ Tools. The Syntactic Analyzer. The TLC Model Checker.
The TLATEX Typesetter. Evaluating Expressions and Temporal Formulas. Computes States. Checking Properties.

Lector:             Alexander Keda

14.09.2007      TLC using techniques: Model-Checking Mode, Simulation Mode, Debugging a Specification. How to use TLC effectively.

15.09.2007      Other existing modeling techniques. Examples of practical use.

Berdyansk (Ukrainian: Бердянськ, translit. Berdyans’k, Russian: Бердянск, Berdyansk) is a resort city in the Zaporizhia province of south central Ukraine. It is an administrative centre of the Berdyansk district and has population around 125,000 (as for 2001).

Berdyansk is an ecologically clean city at the Azov Sea North shore. The city of Berdyansk is famous for its sunny days, which are more per year than in the world known resort Nizza.

The sandy beaches of Berdyansk attract more than 500.000 tourists in summer. Berdyansk is popular with its mud-cure therapy, and mild climate health resorts since the late 19th century.

Berdyansk industries include fishing and fish processing, flour milling, oil refining, machinery and cables manufacturing, metal works, clothing and food processing.

The ancient land of the North pre-Azov region famous since the time of Herodotus (V century В.С.) as "Aghara", is remarkable for its lovely, friendly and international atmosphere.

The city was founded in 1827 under the name Kutur-Ogly, which in 1830 was changed to Novo-Nogaisk. The present name was given to the city in 1842. Between 1939 and 1958 it was known as Osipenko, the name now used by the nearby town Osypenko.

Direct train from Kiev to Berdyansk 227К

Direct train from Berdyansk to Kiev 228П

You can get there by train or plain and go to Berdyansk by bus.

Kiev–Mariupol 18²⁰ – 20⁰⁰ (ИИ 932)

Mariupol–Kiev 7¹⁵ – 9⁰⁵ (ИИ 931)

Kiev–Mariupol–Kiev flights are daily (except Sunday).

Hotels (English links)

Map