Petak, 07. maj 2004. u 14h, sala 2 MI SANU :

Peter O'Hearn, Queen Mary Colledge, London University
SEPARATION LOGIC

Abstract: Separation logic is an extension of Hoare's logic to programs than mutate data structures with pointers. The main novelty of the logic is the "separating conjunction" P*Q, which holds when the program state can be partitioned into two portions, one of which makes P true and the other of which makes Q true. The separating conjunction allows local reasoning about portions of state to be done in isolation, and then combined in a modular way. Separation logic has been developed in a series of papers by Reynolds, O'Hearn, Yang and others; this will be an introductory talk that describes its central ideas.

Petak, 14. maj 2004. u 14h, sala 2 MI SANU:

Dr Rade Zivaljevic, Matematicki institut SANU, Beograd
TOPOLOSKA TEORIJA GRAFOVA

Rezime: Bojenje grafova je zanimljiv problem, interesatan i sa teoretskog i prakticnog stanovista. Ovo pitanje se na primer pojavljuje u (pojednostavljenom) modelu alociranja frekvencija u mobilnoj telefoniji. Najslavniji matematicki problem u kategoriji bojenja grafova je svakako problem cetiri boje, resen od strane Haken-a i Appell-a 1977. sa najnovijim dokazom koji su dali Robertson, Sanders, Seymour i Thomas.

U predavanju ce biti prikazana ona grana teorije bojenja grafova koja se oslanja na upotrebu topoloskih metoda primenjenih na tzv. (simplicijalne) graf-komplekse. Osnovni rezultat u oblasti je znamenito resenje Kneser-ove hipoteze (L. Lovasz, 1978) a najnoviji prodor su ostvarili E. Babson i D. Kozlov, resenjem tzv. Lovasz-ove hipoteze. Pokazuje se da su topoloske metode ne samo korisne, nego u nekim slucajevima i jedine poznate metode za nalazenje dobrih donjih ocena za hromatski broj vaznih klasa grafova.

Petak, 21. maj 2004. u 14h, sala 2 MI SANU:

Dr Vladimir Dragovic, drBorislav Gajic, Matematicki institut SANU, Beograd
SISTEMI HES - APELJROTOVOG TIPA

Rezime: Lagranzeva dvojna cigra je novi integrabilni sistem dinamike krutog tela na so(4) X so(4). Izucavanje dinamickih i geometrijskih svojstava ovog sistema motivise uvodjenje nove klase integrabilnih dinamickih sistema -- izoholomorfnih sistema. Odredjene perturbacije izoholomorfnih sistema daju prve primere visedimenzionih uopstenja klasicnog Hes-Apeljrotovog sistema.

Petak, 28. maj 2004. u 14h (MF):

Prof. Miodrag Raskovic, Uciteljski fakultet, Beograd Zoran Markovic, Zoran Ognjanovic, Radosav Djordjevic, Matematicki institut SANU
NEKI NOVI REZULTATI U TEORIJI VEROVATNOSNIH LOGIKA

Rezime: U okviru projekta 1379 jedna grupa istrazivaca se bavi verovatnosnim logikama. U izlaganju ce biti prikazani rezultati ove grupe koji su publikovani ili prihvaceni za publikovanje tokom rada projekta. To se odnosi na razvoj: verovatnosnih logika sa intuicinostickom logikom kao baznom, verovatnosnih logika sa operatorima za uslovnu verovatnocu, kao i verovatnosnih logika kod kojig su kodomeni verovatnoca konacni.

U petak, 07.05. u 16h, sala 2 SANU, u okviru Seminara za logiku odrzace se drugi deo predavanja na temu SEPARATION LOGIC:

A DECIDABLE FRAGMENT OF SEPARATION LOGIC Josh Berdine (joint with Cristiano Calcagno and Peter O'Hearn)

ABSTRACT: A small fragment of separation logic and a procedure for deciding validity of entailments between formulae is described. The fragment includes only a single inductive predicate, describing segments of linked lists (essentially reachability), and restricts formulae to a special form whose main characteristic is the inability to express `unspecified sharing''. That is, general separation logic formulae are sometimes modeled by heaps (worlds) where some parts of a heap model multiple subformulae. The fragment rules out such formulae, roughly leaving only those whose models can be split into separate pieces for each subformula. While admittedly very small, the observation that the specifications of many list-manipulating pointer programs fit into this fragment motivated our investigation. The key to decidability is the inability of formulae in the fragment to distinguish between different models (of the inductive case) of the list segment predicate. This, together with separation logic's finite model property, allows ignoring all but a couple heaps in the search for a countermodel. Proof theoretically, this manifests as a rule which infers an inductive property from non-inductive premisses.

Ovo obavestenje mozete naci i na Internetu: www.mi.sanu.ac.yu