20 November 2009 14:00, room 0.2.90
Program Testing via Hoare-style Specifications.
Alan Mycroft, Cambridge University
[Joint work with Kathy Gray, extending FASE'2009 work]
Program Validation (testing) and Verification (formal proof) are too often seen as disjoint subject areas. We observe that a typical `unit test' (e.g. in JUnit) first creates some data structure, then invokes the procedure under test, then checks an assertion -- in essence a Hoare Triple {P}C{Q} but opaquely coded.
The Hoare-triple view of tests greatly simplifies the coding of tests, expecially for procedures which mutate data structures or raise exceptions.
Such tests can be implemented using transactional memory to provide access to both x and old(x), and for more high-level constructs such as modifiesonly(x.f,y.g)
We show how such tests may be compiled into standard Java.
Moreover, this view encourages generalised tests in which preconditions can use logical forms such as `forall' and implication.
Transactional techniques allow such generalised tests to be used during execution on real data as a form of a test mode.
19 November 2009 10:00, room 0.2.13
Funktionsorienteret programmering som industrielt redskab
Christoffer Rosenkilde Nielsen og Jacob Volstrup
Netcompany
Dette seminar præsenterer F# og funktionel programmering som et brugbart industrielt redskab. Christoffer, der har arbejdet med funktionel programmering i over 8 år nu og er Ph.D. fra DTU, vil præsentere eksempler på sit programmeringsarbejde lavet i forbindelse med ICFP-konkurrencen, som han har deltaget i de sidste 4 år.
Jacob, der er kandidat i datalogi fra AAU, vil derefter give en introduktion til LINQ. LINQ og F# har mange træk til fælles, så det er oplagt at drage paralleller. Derefter vil nogle af mulighederne ved at have et funktionelt sprog i .NET platformen blive beskrevet, såsom at kalde metoder på tværs af sprogene eller ligefrem definere en extension method i F# og bruge dem i en C# LINQ query.
7 September 2009 10:00, room 0.2.12
Developing a language with the Dynamic Language Runtime
Harry Pierson
Microsoft
From the start, Microsoft’s Common Language Runtime (or CLR) was designed to support cross-language integration. In .NET Framework 4.0, Microsoft introduces the Dynamic Language Runtime (or DLR), a library that extends the CLR’s cross-language support to dynamic languages. In this session, we’ll take a look under the hood of the DLR to see what capabilities it provides for language developers.
NB!
At 15:00 in 0.2.13, Harry Pierson and Martin Esmann (also from Microsoft) will give an industrial seminar titled Pumping Iron: Dynamic Languages on .NET
22 January 2009 14:30, room 0.2.12
Introductory Lecture: My past and current research in multimedia databases
Ira Assent
Department of Computer Science
Aalborg University
I would like to introduce myself by giving an overview over my past and current research in multimedia databases.
Many database applications require efficient access to relevant content. Similarity search, for example, retrieves the most relevant database objects for a given query. When databases are large and the features describing the objects are high dimensional, simple one-to-one comparison between the query and all objects in the database is clearly infeasible. Knowledge discovery in databases is similarly slowed down by high dimensional large databases. Knowledge discovery tasks such as classification or clustering require efficient algorithms for large scale applications. Our approaches for runtime improvement include multistep filter-and-refine algorithms and index structures. We provide guarantees on the correctness of the result and demonstrate efficiency in experimental evaluations.
20 December 2008 14:00, room 0.2.13
Towards programming Safety Critical Systems in Java
Bent Thomsen
Department of Computer Science
Aalborg University
Java and Real-time programming is by many considered as an oxymoron.
However, Java was originally developed as a programming language for embedded systems, but it was the Internet that propelled Java into mainstream computing, because there was a need for a language that was portable and truly object-oriented, eliminating the error-prone programming of memory allocation and pointer manipulation. Unfortunately, precisely those features made it less suited for predictable, real-time embedded systems. Especially the virtual machine, that gave portability, was considered inefficient. However, with recent advances in JVM implementations, especially the emergence hardware JVMs such as the aJ-100 and JOP, it is now possible to write real-time applications in Java that executes as efficiently as their non-Java alternatives.
In this talk I will give an overview of research activities at CISS (Center for Indlejrede Software Systemer) concerned with programming Safety Critical Systems in Java.
I will in particular go into details about a new, minimal specification for real-time Java for safety critical applications. The intention is to provide a profile that supports programming of applications that can be validated against safety critical standards such as DO-178B. The proposed profile is in line with the Java specification request JSR-302: Safety Critical Java Technology, which is still under discussion. In contrast to the current direction of the expert group for the JSR-302 we do not subset the rather complex Real-Time Specification for Java (RTSJ). Nevertheless, our profile can be implemented on top of an RTSJ compliant JVM and has indeed been on both the aJ-100 processor and JOP.
One aim with this profile is that it should be relatively easy for Java midlet/J2ME programmers to move into programming Safety Critical Systems in Java. Another aim is that programs written for this profile should be analyzable wrt. Schedulability, Worst Case Execution Time and Memory consumption with tools such as UPPAAL.
Joint work with:
Martin Schoeberl
Institute of Computer Engineering
Vienna University of Technology, Austria
Hans Søndergaard
Vitus Bering Denmark University College
Stephan Korsholm
KIRK telecom and CISS
Anders P. Ravn and Lone Leth Thomsen
Department of Computer Science
1 June 2007 at 12:30 in E3-109
SpaceTwist: A Flexible Approach for Hiding User Location
Man Lung Yiu
Department of Computer Science
Aalborg University
Recently, location-based service users are increasingly
aware of their privacy — they hope to enjoy location-based
services without disclosing their exact locations. Existing
location privacy protection methods can be broadly classified
into: (i) spatial cloaking techniques, and (ii) cryptographic
matching solutions. The former requires complex
server implementations and transmits huge number of
unnecessary objects over communication network. On the
other hand, the latter does not offer guarantee on the accuracy
of results. To overcome all the above problems, we propose
a novel approach, called SpaceTwist, for hiding user
location. Its main advantages are: a high degree of privacy
can be achieved, the user has flexibility to control the search
process dynamically, and the server implementation is simple.
In addition, we develop a granular searching technique
to reduce the communication cost while guaranteeing the
accuracy bound of the returned results. Experimental results
on real datasets show that our technique retrieves results
with good accuracy at low communication cost.
29 May 2007 at 12:30 in E1-214
The TaskTrainer - A Training Environment for (C#) Undergraduate Programming Education.
Matthias Längrich
University of Applied Sciences, Zittau/Görlitz, Germany
It is widely accepted that learning without intelligent practicing
doesn't lead to a lasting increase of competencies. Although,
practicing is often compared to boredom and drill by the students. On
the other hand, tutors feel overburden when working with 15 or more
students in a class where all of them would like to be supported
individually, instantly and competently.
Concerning these aspects a tool named TaskTrainer (TT) has been
developed at the University of Applied Sciences Zittau / Görlitz
(Germany) to assist tutors in Undergraduate Programming Education
(UPE) and to provide a didactically and psychologically reasoned
training environment for students. Several evaluations have shown that
the level of education has raised. This presentation will briefly
describe the challenges we are facing and will explain the part of the
TT.
After the seminar, from 13.30 - appr. 14.30 there will be a chance to
have informal discussions with Matthias Längrich about the TT.
9 May 2007 at 13:00 in E3-109
Supporting associations in C#
Kasper Østerbye
IT University of Copenhagen
In the transition from class diagrams to code, associations as found in UML
are often poorly supported.
Typically, associations are either translated into collections and
references by hand, which is error prone if the association is
bi-directional. Or the association code is generated by a code generation
tool, which introduces synchronization problems between hand-written code
and UML design. No main stream programming language supports associations,
and no mainstream library has to my knowledge ever supported associations.
An association library should support both consistency, e.g. for a 1-Many
association. It should allow instances of a class to be associated with
instances of other classes, as well of itself. It should be possible to
traverse the associations in a natural OO manner, and it should be
reasonably simple to specifiy an association. In addition, it should be easy
to declare reflexive relationsships, so one can build tree-structures
easily. In this talk I will outline the issues in building a library of
associations, which can be reused across a number of applications. The
library is intended to work well with C# 3.0 and Linq.
12 March 2007 at 14:30 in E1-214
Anekdoter fra en karierre som systemchef - hvad der kan gå galt, vil gå galt
(Anecdotes from a career as systems manager - what can go wrong will go wrong!)
Lars Fischer
CTO Nordunet
(og tidligere F-studerende og ex F-junta)
2 February 2007 at 13:00 in E3-209
IBMs udlægning af SOA
Finn Grønbæk
IBM Danmark
Abstract:
Finn Grønbæk er senior IT arkitekt hos IBM Danmark, hvor han hjælper danske virksomheder og offentlige organisationer med at få designet og implementeret enterprise arkitekturer. Dette involverer komponter som portaler, J2EE applikationsservere, information management sytemer og integrations-"middleware". gennem de sidste 2.3 tre år har det været med stigende fokus på introduktion af forretningsservices implementeret som web services og etablering af Service Orienteret Arkitektur.
Finn Grønbæk har også arbejdet meget med design af applikationsarkitektur med anvendelse af patterns som Model-View-Control, J2EE best practices, frameworks som Struts, Jave Server Faces, Java Portlets mv., understøttelse af software life cycle metodisk og anvendelse af platforme som eclipse, versions- og konfigurationsstyringssystemer, samt kodegenereringsteknikker som Ant, Doclets m.v.
Før sit job hos IBM har Finn Grønbæk været udviklingschef i internetvirksomheden Framfab, undviklingschef og chef-arkitekt hos Infoware, konsulent og teamleader i Dansk Teknologisk Institut, Datateknik, og endelig konsulent og afdelingsleder i Teknisk Informatik Center (TICA) på Aarhus Tekniske Skole.
14 December 2006 at 13:00 in G5-112
Algorithmic and a Geometric Characterization of Coarsening At Random
Richard Gill
University of Leiden
The Netherlands
(currently visiting Institute of Mathematical Sciences, Århus Univ.)
Abstract:
We show that the class of conditional distributions satisfying the Coarsening at Random (CAR) property has a simple algorithmic description based on randomized uniform multicovers, which are combinatorial objects generalizing the notion of partition of a set. The maximum needed height of the multicovers is exponential
in the number of points in the sample space. This algorithmic characterization stems from a geometric interpretation of the set of CAR distributions as a convex polytope and a characterization of its extreme points. The hierarchy of CAR models defined in this way can be useful in parsimonious statistical modelling of CAR mechanisms.
19 December 2006 at 10:00 in E3-109
Analyzing Ambiguity of Context-Free Grammars
Claus Brabrand
Department of Computer Science
Århus University
(joint work with Robert Giegerich and Anders Møller)
Abstract:
It has been known since 1962 that the ambiguity problem for context-free grammars is undecidable. Ambiguity in context-free grammars is a recurring problem in language design and parser generation, as well as in applications where grammars are used as models of real-world physical structures. However, the fact that the problem is undecidable does not mean that there are no useful approximations to the problem.
We observe that there is a simple linguistic characterization of the grammar ambiguity problem, and we show how to exploit this to conservatively approximate the problem based on local regular approximations and grammar unfoldings. As an application, we consider grammars that occur in RNA analysis in bioinformatics, and we demonstrate that our static analysis of context-free grammars is sufficiently precise and efficient to be practically useful.
24 October 2006 at 14:30 in D2-106
Static Analysis for Java Servlets and JSP
Christian Kirkegaard and Anders Møller
Department of Computer Science
Århus University
Abstract:
Developers of Web applications that use, for example, Java Servlets and JSP, often face the following problem: How can we guarantee that the dynamically generated output of the programs is always well-formed and valid XML?
The talk presents a program analysis that attacks this problem. The approach builds on a collection of program analysis techniques developed earlier in the JWIG and XACT projects, combined with Knuth's classical work on balanced context-free grammars. Together, this provides the necessary foundation concerning reasoning about output streams and application control flow in the Web application code.
(This work was presented at the 13th International Static Analysis Symposium (SAS'06); see href=http://www.brics.dk/~amoeller/papers/servlets/)