French-Algerian Cycle of Seminars
Following an initiative of Marc Daumas and Professeur Mohamed Mezghiche, we had in the summer of 2007 a cycle of seminars between the University of Perpignan Via Domitia and the University M'hamed Bougara of Boumerdès in Algeria. The seminars took place in the meeting room of laboratory ELIAUS (second floor - 1er étage - of the B building) at 2PM (local time) and in PG class room of laboratory LIFAB at 1PM (local time).
The first two seminars were broadcasted live and the last two ones were recorded. Videos and slides can be downloaded from links below. Podcast videos are now available from the Open University Montpellier Languedoc-Roussillon.
| 7 juin | David Lester | Invited professor funded by the French Région Languedoc-Roussillon |
| 12 juin | Marc Daumas | CNRS-LIRMM & ELIAUS |
| 19 juin | Ren-Cang Li | Invited professor funded by the French Région Languedoc-Roussillon |
| 21 juin | César Muñoz | Invited professor funded by the UFR SEE of the University of Perpignan Via Domitia |
A Chip Multiprocessor for Large-Scale Neural Simulation
Steve Furber and David Lester
University of Manchester
We can now design chips with one billion transistors, but how are we to use this computing power effectively ? Neural Computing provides one possible answer.
The biological neuron has many beguiling properties : put simply, they are very simple, low performance, fault-tolerant, components. A human brain has 1012 neurons, with 1015 connections. The power efficiency exceeds CMOS. The individual neuron operates at about 100 Hz, and communication takes place at speeds of (typically) a few metres/second. It is redundant to a remarkable degree, since significant brain damage is required to make large performance differences.
How is performance such as the human intellect possible with such antediluvian kit?
We just don't know ! That's why we are building a system to mimic biological neural computing. That the system might be usable in many other possible Neural Network applications is also something that we wish to explore.
Stochastic Formal Methods : An application to accuracy of numeric software
We provide a bound on the number of numeric operations (fixed or floating point) that can safely be performed before accuracy is lost. This work has important implications for control systems with safety-critical software, as these systems are now running fast enough and long enough for their errors to impact on their functionality. Furthermore, worst-case analysis would blindly advise the replacement of existing systems that have been successfully running for years. We present here a set of formal theorems validated by the PVS proof assistant. These theorems will allow code analyzing tools to produce formal certificates of accurate behavior. For example, FAA regulations for aircraft require that the probability of an error be below 10-9 for a 10 hour flight.
Always Chebyshev Interpolation For Elementary Function Computations
Department of Mathematics, University of Texas at Arlington
A common practice for computing an elementary transcendental function in a libm implementation nowadays has two phases: reductions of input arguments to fall into a tiny interval and polynomial approximations for the function within the interval. Typically the interval is made tiny enough so that polynomials of very high degrees aren't required for accurate approximations. Often approximating polynomials as such are taken to be the best polynomials or any others such as the Chebyshev interpolating polynomials. The best polynomial of degree n has the property that the biggest difference between it and the function is smallest among all possible polynomials of degrees no higher than n. Thus it is natural to choose the best polynomials over others. In this talk, we'll show that the best polynomial can only be more accurate by at most a fractional bit than the Chebyshev interpolating polynomial of the same degree in computing elementary functions, or in other words the Chebyshev interpolating polynomials will do just as well as the best polynomials.
Invisible Formal Methods for Safety Assurance of Aerospace Applications
National Institute of Aerospace at NASA Langley Research Center
The expression "Invisible Formal Methods", coined by J. Rushby at SRI International, refers to the use of formal analysis tools in an unobtrusive way, e.g., in a way that is acceptable to the engineering practice. This is done by providing a set of tools that increase the safety assurance by incrementally performing a series non-trivial formal analyses. In this talk, we report on our experience at NIA on the use of invisible formal methods for the safety analysis of aerospace applications. First, we present a series of automated strategies for proving real number properties on theorem provers. These strategies are at the base of a tool that formally verifies computational errors of expressions using interval analysis. This tool requires a minimum user interaction with the theorem prover. Finally, we present an automated tool for checking safety properties of C programs involving non-linear arithmetic. This tool integrates a constraint solver for interval arithmetic to Berkeley Lazy Abstraction Software Verification Tool (BLAST).