Seminarium Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji (SLIWOWICA)

Opowiem o pomyśle wykorzystania systemów przepisywania termów jako lepszych makroprocesorów, w szczególności opiszę tworzony obecnie system (na wczesnym etapie rozwoju) reprezentowania zapytań SQL jako termów Maude i jego zastosowanie do generowania SQL-a, modularyzacji kodu i eksperymentowania z semantycznymi rozszerzeniami języka.

Praca wspólna ze Ś. Sobieskim.

Chodzi oczywiście o formalizację w Coqu semantyki maszyny wirtualnej Javy.

Ogólnie będzie... jak zwykle, a w szczegółach - jak realizuję operacje na stosie wartości (tzw. stackop) i jakie wnioski z tego wynikają dla całej formalizacji.

W referacie (po polsku, tytuł i slajdy po angielsku) pokażę, że w arkuszach kalkulacyjnych można nie używając żadnych makr zaimplementować interpreter maszyny PRAM (Parallel Random Access Machine).

Wskazuje to zarazem na:

1) Możliwość wyrażania w arkuszach bardzo skomplikowanych obliczeń i związane z tym trudności z dowodami ich poprawności.

2) Możliwość używania arkuszy jako interfejsów do specyfikacji obliczeń równoległych ogólnego stosowania.

3) Potencjał optymalizacji obliczeń wykonywanych w arkuszach w kierunku ich zrówlnoleglania.

Opowiem o metodzie dowodzenia kompozycjonalności
równoważności behawioralnych za pomocą układów równań między
operatorami modalnymi. Najpierw przypomnę, co to są koalgebry,
bialgebry, logiki modalne i SOS.

"Fluid updates" (płynne aktualizacje?) to mechanizm stosowany przy analizie programów operujących na tablicach, przedstawiony w pracy [DDA10]. Wykorzystuje on formuły logiki pierwszego rzędu, których spełnialność weryfikowana jest przez SMT-solver.

Podczas prezentacji pokażę, jak uogólnić ów mechanizm poprzez zastosowanie dowolnej dziedziny abstrakcyjnej zamiast FOL. Pozwoli to na wnioskowanie o dowolnych słownikach (niekoniecznie indeksowanych liczbami) oraz zwiększenie wydajności (poprzez zastąpienie wywołań SMT-solvera prostszymi operacjami np. na pentagonach).

Tym razem opowiem o swojej pracy którą prezentowałem na workshopie NSAD
2011 - "Sweeping in Abstract Interpretation", swoich wrażeniach oraz
innych pracach które były tam prezentowane.

Specyfikacja kontraktowa pozwala opisać  skutki wykonania metod. Ich wykonanie zwykle zmienia niewielki fragment systemu pozostawiając resztę bez zmian. Język JML posiada mechanizm służący do specyfikacji części niezmienniczej. OCL i niektóre inne języki kontraktowej specyfikacji takich środków nie posiadają.
W tym referacie przedstawimy rozszerzenie OCL umożliwiające specyfikację części niezmienniczej. W szczególności omówimy związane z tym zagadnienia specyficzne dla języka OCL, takie jak specyfikacja asocjacji i widoków.

Będzie to powtórzenie fragmentów referatu:

Autor: Rolf Hennicker (Ludwig-Maximilians-Universität München)

Opis: Interface coherence is a key issue in component-based software
development. It concerns two dimensions of the development process:
component implementations should adhere to their interface specifications
- and - components should be composed only if their interfaces are
compatible. To achieve independent implementability it is essential that
both dimensions work properly together, i.e. that compatibility is
preserved by refinement and refinement is preserved by composition, which
are crucial requirements for any kind of interface theory. This talk
analyses solutions and challenges derived from various interface theories
based on state transition specifications with input/output-actions (e.g.
interface automata, modal I/O-transition systems and open Petri nets).
Criteria for the analysis shall be the communication style (synchronous,
asynchronous), expressiveness (observational abstraction, treatment of
data), decidability of refinement and/or compatibility, as well as
semantic soundness and completeness.

Referat będzie próbą wykrojenia publikowalnego materiału z projektu
RiTS (RCS Network Test Server) zrealizowanego przez nas dla Samsunga.

Staram się zaimplementować w Coqu semantykę bajtkodu Javy w wersji wykorzystującej "faktoryzację" i "parametryzację" (bajtkod w 12 instrukcji).

Na seminarium przedstawię definicje typów dla struktur czasu wykonania. Mam nadzieję na dyskusję i rady co do sensowności owijania wszystkiego we własne definicje, ukrywania za sygnaturą itp.

O pracy Cousot, Cousot, Logozzo z POPL2011 o takim tytule.

Abstract: Working in an arbitrary institution, we discuss property-oriented
semantics of specifications built using some collection of
specification-building operations. As a typical example we consider the
structured specifications built from flat specifications using union,
translation and hiding. For such specifications we have the standard
compositional proof system, which determines the standard
property-oriented semantics assigning a theory to each structured
specification. It is not complete (unless the underlying logic has
interpolation and enjoys some other technical properties) but otherwise it
is "as good as can be expected". In particular, it is sound, monotone (and
hence compositional) and one-step complete. The last property means that
the semantics (and the corresponding proof system) allows us to deduce all
true consequences for specifications built by applying any
specification-building operation to argument specifications, assuming that
there is no discrepancy between the classes of models of the argument
specifications and the classes of models of their respective
property-oriented meanings. This is a strong property which was believed
to ensure that the semantics is "as strong as possible" without loosing
soundness or compositionality. We question this claim and show that it
holds assuming in addition that the semantics considered are not
"absent-minded", i.e., do not loose axioms of flat specifications. We
sketch an example to show that by excluding deduction of some axioms in
flat specifications we may offer a stronger rule for natural
specification-building operation so that for some specifications the
resulting semantics is stronger than the standard one.

Poza referatem na tym pierwszym po feriach spotkaniu będziemy ustalać plan referatów na drugi semestr, zachęcam do zgłaszania tematów i terminów, osobiście na seminarium lub zdalnie emailem do mnie (P.Czarnika).

Przedstawię swoje prace nad dziedzinami do reprezentowania zawartości tablic. Zaprezentuję dwa rozwiązania:
 - wydajne, ale mało precyzyjne, oparte o dziedzinę przedziałową (wykorzystujące drzewa przedziałowe),
 - mniej wydajne, ale dokładniejsze, oparte o pentagony.

Opowiesci o spotkaniu w Schloss Daghstul, 1-3.12.2010.

Przypominamy, że do końca grudnia seminarium odbywa się w ZMIENIONEJ SALI: 5850 

Opowiem o aktualnych pracach związanych z dziedziną abstrakcyjną 'Weighted Hexagons'.
Pokażę jak rozszerzyć WH, aby obsługiwały również ostre nierówności. Opowiem o (dotychczas nieudanych) próbach zaadaptowania WH do przypadku całkowitoliczbowego (gdzie wartości zmiennych są liczbami całkowitymi).
Powiem też jakie były główne uwagi do tej dziedziny na prezentacji na NSAD2010.

RiTS to wewnętrzna nazwa jednego z projektów realizowanych w ramach współpracy UW z firmą Samsung. Głównym celem projektu jest zbudowanie systemu wspierającego testowanie klientów zestawu protokoów "Rich Communication Suite".

Na najbliższym seminarium opowiem pobieżnie o protokołach RCS i dokładniej o zasadach działania systemu i opracowanych w ramach projektu językach:

- definiowania środowiska testowego

- definiowania scenariuszy testowych.

Temat RiTS będzie najprawdopodobniej kontynuowany na następnym seminarium, kiedy postaram się podać więcej szczegółów protokołów RCS i przedstawić ciekawe elementy naszej implementacji.

Po wakacyjnej przerwie zapraszamy na seminarium SLIWOWICA.

W poniedziałek 4 października przewidujemy spotkanie organizacyjne, na którym ustalimy wstępną listę referatów (lub co najmniej prelegentów) na semestr zimowy. Gorąco prosimy o zgłaszanie propozycji. Osoby, które nie będą mogły się pojawić, proszę o nadesłanie propozycji mailowo, na adres czarnik@mimuw.edu.pl.

Projekt RiTS jest realizowany w ramach współpracy Uniwersytetu Warzawskiego z firmą Samsung Electronics. Głównym celem projektu jest zbudowanie testowego serwera zestawu usług Rich Communication Suite. W ramach projektu poznajemy i analizujemy technologie i protokoły komunikacyjne, o które oparty jest RCS.

Na seminarium opowiem o standardzie RCS i usługach/protokołach wchodzących w jego skład, a także o założeniach i bieżącym statusie projektu, z naciskiem na wstępny projekt architektury systemu.

It has been a common belief that the standard results of universal
algebra as developed since the work of Birkhoff and others in the
thirties carry over without much change to the framework of
many-sorted algebras. Perhaps the only notable exception widely
noticed by the community is the care needed in the treatment of
many-sorted equational logic. However, while the standard results
remain valid in essence in the many-sorted frameworks, some nuances
and technicalities require considerably more care in formulation and
proof of the results. We give some examples of such situation,
indicating how equational calculus, Birkhoff's variety theorem and
interpolation results should be adjusted for many-sorted algebras.

Na seminarium przedstawię (w zarysie) semantykę operacyjną i
denotacyjną rachunku procesów, nad którym ostatnio pracuję. Rachunek
przypomina CSP Hoare'a, ma jednak kilka nietypowych cech:

- Alfabety procesów podzielone są na akcje wejściowe i wyjściowe.

- Semantyka uwzględnia obliczenia nieskończone bezpośrednio (a nie
jako granice łańcuchów obliczeń skończonych).

- Obliczenia procesu reprezentowane są nie przez ciągi (czyli liniowe
porządki) akcji, a przez częściowe porządki etykietowane akcjami (tzw.
pomsety).

Opowiemy jak zwykle o abstrakcyjnej interpretacji. Tym razem będziemy opisywać naszą abstrakcyjną dziedzinę numeryczną - Weighted Hexagons. Pozwala ona reprezentować:

• zależności postaci x <= a*y, gdzie x,y są zmiennymi oraz a jest stałą dodatnią,
• zależności przedziałowe czyli a <= x <=b gdzie x jest zmienną, stałe a i b oznaczają krańce przedziału.

Prerun przed Bytecode 2010.

Abstrakt pracy:

  One of the biggest obstacles in the formalisation of the Java
  bytecode is that the language consists of 200 instructions.
  However, a rigorous handling of a programming language in the
  context of program verification and error detection requires a
  formalism which is compact in size.  Therefore, the actual Java
  bytecode instruction set is never used in the context.  Instead, the
  existing formalisations usually cover a `representative' set of
  instructions.  This paper describes how to reduce the number of
  instructions in a systematic and rigorous way into a manageable set
  of more general operations that cover the full functionality of the
  Java bytecode. The factorisation of the instruction set is based on
  the use of the runtime structures such as operand stack, heap etc.
  This is achieved by presentation of a formal semantics for the Java
  Virtual Machine.

Aleksy opowie o wspólnej z Jackiem i Patrykiem pracy - sprowadzeniu całej funkcjonalności i wszystkich instrukcji Maszyny Wirtualnej Javy (JVM) do 12 instrukcji i zapisaniu operacyjnej semantyki małych kroków w postaci 23 reguł. Oczywiście instrukcje są sparametryzowane, aby móc reprezentować wszystkie instrukcje oryginalnego języka, a wybór 12 instrukcji jest oparty o sposób korzystania ze struktur danych JVM.

Staraliśmy się pokryć cały język JVML i co najmniej umożliwić uwzględnienie wszystkich aspektów, takich jak współbieżność czy Java Memory Model. Na seminarium przedstawione zostaną też pomysły na dalsze rozwinięcie tego tematu w kierunku formalizcji tej pracy w Coqu, wykorzystania do analiz statycznych/abstrakcyjnych interpretacji, czy opracowania analogicznie "skompresowanego" języka specyfikacji dla JVM.

Podczas seminarium opowiem o moich zmaganiach z pokazaniem istnienia wszystkich granic w kategorii Preord!, której obiekty to praporządki, zaś morfizmy spełniają dwa warunki:

(1) są monotoniczne

(2) słabo odbijają domknięcia w dół, czyli dla f : A -> B, a\in A, b'\in B, jeśli b'<=f(a), to istnieje a'\in A, że f(a')=b' i a'<=a

Trudne okazało się zwłaszcza zdefiniowanie produktów w tej kategorii. Postaram się przystępnie przedstawić problem i podać uzasadnienie, dlaczego kategoria Preord! może być interesująca dla informatyka.