Português English
Contato
Publicado em: 24/03/2010

Série de Seminários do Instituto de Informática no dia 26/03

Na próxima sexta-feira, 26 de março,às 13h30min, no Auditório José Mauro Volkmer de Castilho, acontecerá a palestra com o Prof. Florian Kammüller, pesquisador da Universidade Técnica de Berlin.
Série de Seminários do Instituto de Informática da UFRGS
———————————————-

Sexta-feira – 26/03/2010
Horário: 12:45 h – 13:30h
Local: Auditório José Mauro Volkmer de Castilho
———————————————-

Instituto de Informática
Universidade Federal do Rio Grande do Sul
———————————————-

Title:
ASPfun: a Calculus for Distributed Active Objects

by Dr. Florian Kammüller

ABSTRACT:
Programming in large networks of computers, like the Internet, poses newproblems of safely implementing parallel activities, code distribution,and complex communication structures. This talk presents a foundation for autonomous objects and their communication: ASPfun is a calculus for functional distributed objects that communicate asynchronously.
Requests to objects are method calls represented by so-called futures; replies finally return the result to the object containing the future.

ASPfun is completely formalized and its properties proved in the interactive theorem prover Isabelle/HOL. This includes a type system and a proof of type-safety which implies deadlock-freedom.

This talk presents the ASPfun language, outlines its Isabelle/HOL development, and motivates its application by example from service oriented applications. Information flow security is finally discussed as the next goal for the static analyis of ASPfun.

SHORT BIO:
Florian Kammüller is Privatdozent (honorary professor) at the Technische Universität Berlin. He studied Computer Science at the Universität Kaiserslautern and Technische Universität Berlin graduating in 1995. He received his PhD from the University of Cambridge in 1999. After two years of postdoctoral research at the GMD First Institute, he became a junior lecturer at the Technische Universität in Berlin. Since then, he has completed a research year at INRIA Sophia-Antipolis, France, and a
guest professorship at the University of Cape Town. 2006 he received his Habilitation for his work on interactive theorem proving in software engineering. In his research work that is amply documented in publications in journals and at international conferences he focusses on the support of formal methods with automated verification ranging from bytecode verifiers to UML development and from model checking to constructive type theory. Currently he is leading two projects funded by the German Research Foundation (DFG):  ASCOT a project on the formal analysis of aspect-oriented programming and ASPEN a project in collaboration with INRIA Sophia-Antipolis on mechanizing a calculus for distributed components.