- Homepage
- About the Joint Centre
- Research Areas & Projects
- Researchers
- News & Events
- Open Positions
My main research interest revolves around the formal description of algorithms and mathematical theories. By formal description, I mean descriptions that can be completely checked by computer programs: theorem proving tools.
We talk about theorem proving tools, because we try to prove every property that we state about algorithms. So each new algorithm that we study gives rise to a few theorems that need to be entirely verified on the computer. At least one theorem has the statement of the form, if we feed this algorithm inputs that satisfy property so and so, then the algorithm performs without error and returns outputs that satisfy such and such properties.
the long term dream is that this kind of technique could be used to develop all the software that we use in everyday life, so that bugs would be detected very early in the design process. A bug would appear when some algorithm requires that its input has a given property, but this algorithm receives its outputs from another algorithm which only ensures a weaker property. Checking that some property entails another one is also among the theorems that we need to prove.
2013
Conference papers
Books
2008
Conference papers