PhD in Computer Science

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.