PhD in Computer Science

We are happy to announce the Moose Suite version 4.6:http://moosetechnology.org/download

What is new:

• New editors for scripting browsers and visualizations
• New parser for SQLite
• New Glamorous Inspector for working with Smalltalk objects
• Improved Glamour browser building engine
• Improved EyeSee charting engine
• Improved FAMIX API
• Improved FAMIX to support Java and C++
• Improved external importers to support Java and C++

A list of issues addressed in this release can be found at:http://code.google.com/p/moose-technology/issues/list?can=1&q=status=Fixed%20milestone=4.6.

source

We announce 4 sessions for learning Coq. Dates are 26-01-12, 09-02-12, 23-02-12, and 08-03-12. It will take place in room 178 at LaBRI. The sessions are from 15.30 to 17.30.

TITLE: Modeling and verifying algorithms in Coq: an introduction

ABSTRACT:

The Coq system provides a functional programming language and a reasoning framework based on higher order logic to perform proofs on programs. The expressive power of the language is such that advanced notions of mathematics (such as the graph theory in the four color theorem) or programs of high complexity (such as a compiler for a significant kernel of the C Programming language) can be described formally. In this school, we address the basic programming techniques and approaches to prove properties of the programs. The covered notions involve structural recursive programming, list and integer handling, proof by induction, in the key definition of data-types, pattern matching constructs and case-based reasoning, and inductive properties.

We announce the new session of the working group about software engineering at LaBRI. For this new session, Tegawendé F. Bissyandé will present his current work. It will take place at LaBRI, room 71, Thursday, the 2nd of February at 10.00 AM.

TITLE: Generation of Debugging Interfaces for Linux Kernel-level Services

ABSTRACT:

The Linux kernel does not export a stable, well-defined kernel interface, complicating the development of kernel-level services, such as device drivers and file systems. While there does exist a set of functions that are exported to external modules, these are continually changing, and have non-trivial implicit, ill-documented pre and post conditions, which, if not satisfied, can cause the entire system to crash or hang. We have observed the prevalence of such safety holes in a study of several recent releases of the Linux kernel. However, no specific debugging support is provided.

We present Diagnosys, a new approach to automatically constructing a debugging interface for the Linux kernel. Diagnosys relies on static analysis of kernel source code to infer usage preconditions of functions exported to kernel-level services. Service developers can then use the Diagnosys interface generator to produce a debugging interface that is specialized to their code. This interface is then included within a service implementation such that when the service is tested it records information about potential problems. Thanks to Diagnosys crash resilient logging system, the recorded information is then made available on reboot to the service developer on reboot after a kernel crash or hang.

We use our approach on 10 services from a range of kernel level services including file systems, network adapters, USB device drivers, multi-media drivers, and show that the debugging interfaces provide useful information in case of faults, while incurring only a slight performance overhead.

We announce the new session of the working group about software engineering at LaBRI. For this new session, Tim Sheard will present a language that mix logical and functional styles. It will take place at LaBRI, room 64, Thursday, the 18th of January at 10.00 AM.

TITLE: Mixing logic and functional programming styles

ABSTRACT:

We have been designing a language in which programmers can mix the logic and functional styles. In the functional style programmers introduce variables and assign the variables values be describing a computation that evaluates to the answer desired.

In our language one can also introduce variables by describing what properties their values should have using first order logic. The language implementation automatically searches for solutions.

The language lets the programmer mix computation based programs with search based programs in a completely transparent manner.

The kind of search is directed by the type of value being sought, and the particular operands in the logic used to describe its properties. we use general purpose tools like SAT solvers, SMT solvers, the Simplex algorithm, and Narrowing to actually perform the search.

Creation of the search tree, and the strategy of searching the tree are separated, and the user can specify a different strategy for each search, yet a single answer may involve several searches, and all these are coordinated in a transparent manner.

We announce the new session of the working group about software engineering at LaBRI. For this new session, Reinout Stevens and Andy Kellens will present there current work. It will take place at LaBRI, room 178, Tuesday, the 20th of December at 10.00 AM.

TITLE: Querying Code and History with SOUL

ABSTRACT:

The Smalltalk Open Unification Language (SOUL) is a logic programming language dedicated for reasoning over software. Its symbiosis with the underlying Smalltalk environment, and its open unification mechanism result in that SOUL is a suitable platform for building program querying tools. We give an overview of the core SOUL language, its unique features, some of the custom extensions to this language and the surrounding tool suite. In the second part of the presentation we discuss Absinthe: a recent extension of SOUL that combines quantified regular path expressions with logic queries to reason over the history of a software system. For more information about SOUL and its applications: http://soft.vub.ac.be/SOUL/.

We announce the new session of the working group about software engineering at LaBRI. For this new session, Young-Joo Moon will present her thesis work. It will take place at LaBRI, room 178, Wednesday, the 23th of November at 10.00 AM.

TITLE: Stochastic models for quality of service of components connectors

ABSTRACT:
The intensifying need for scalable software has motivated modular development and using systems distributed over networks to implement large-scale applications. In Service-oriented Computing, distributed services are composed to provide large-scale services with a specific functionality. In this way, reusability of existing services can be increased. However, due to the heterogeneity of distributed software systems, software composition is not easy and requires additional mechanisms to impose some form of a coordination on a distributed software system.

Besides functional correctness, a composed service must satisfy various quantitative requirements for its clients, which are generically called its quality of service (QoS). Particularly, it is tricky to obtain the overall QoS of a composed service even if the QoS information of its constituent distributed services is given.

For this, Stochastic Reo is proposed to specify software composition with QoS aspects and its compositional semantic models. These semantic models are also used as intermediate models to generate their corresponding stochastic models for practical analysis. Based on this, we have implemented the tool Reo2MC. Using Reo2MC, we have modeled and analyzed an industrial software, the ASK system. Its analysis results provided the best cost-effective resource utilization and some suggestions to improve the performance of the system.

Google Citation is open to all. The service tracks your publications and computes their citation metrics: http://googlescholar.blogspot.com/2011/11/google-scholar-citations-open-to-all.html.

My profile is public: http://scholar.google.com/citations?user=zRtfccEAAAAJ

From RMod:

We are proud to announce the release of 1.3 of Pharo. This new release is the result of active development from the community and it is composed of:

• Cleaning architectural dependencies
• More cleanups directed by applying code critics on the system
• Support for server and headless images. Pharo has now a support for stdin, stdout and stderr.
• More robust and better startup/shutdown
• Improved look and feel
• Better widgets
• Improved tools
• Weak Announcements
• Stratified Proxy
• More class comments
• Network improvements based on Zinc

Download 1.3 here: http://www.pharo-project.org/pharo-download/release-1-3

I printed a A5 version of my thesis.

The cover was made by Guillaume Perrin. It makes the book really beautiful.

The pdf version of the A5 format is available here.

The Sphere team is visiting the team of Tom Mens at the university of Mons.