Commit 72cb5dec authored by Marc's avatar Marc
Browse files

typoes

parent 6b87553d
......@@ -20,7 +20,7 @@ Assité par\\Marc \textsc{Chevalier}\\
\maketitle
\section{Scientific context}
In some contexts, bugs might lead to serious casualties or serious economic or environmental consequences. Such software are called "critical", and we need to get some strong guaranties in terms of safety (the program behave normally) as well as in terms of security (the software is protected against hostile environment). Formal methods, especially abstract interpretation ~\cite{cousot1977abstract}, provide a way to build algorithms that prove such semantic properties.
In some contexts, bugs might lead to serious casualties or grave economic or environmental consequences. Such software are called "critical", and we need to get some strong guaranties in terms of safety (the program behave normally) as well as in terms of security (the software is protected against hostile environment). Formal methods, especially abstract interpretation ~\cite{cousot1977abstract}, provide a way to build algorithms that prove such semantic properties.
\textsc{Antique} team wrote a C analyzer, \textsc{Astrée}~\cite{astree, blanchet2003static}, specialized in the analysis of embedded programs. This analyzer holds several industrial successes such as the formal verification of flight command of Airbus A340 and A380. \textsc{Astrée} was already extended to support the analysis of asynchronous programs~\cite{astreea, mine2014relational}. Currently, \textsc{Astrée} is able to prove safety properties on real world industrial source code.
......@@ -34,7 +34,7 @@ The first step in this direction is the support in \textsc{Astrée} of C program
C aims to be portable, and thus, platform-independent. Assembly, on the contrary, is eminently dependent on the hardware. Thus, an OS cannot avoid assembly to use hardware features that lie beyond the framework of C. But not everything requires assembly. The larger part of computation and control flow can be written in C and is more clear and less error-prone this way. That's why assembly only exists as small and scattered pieces included in C code.
We also already have a formal semantics of most asm instructions (all user instructions) and of larger part of (barely) reasonable interactions between C and assembly.
We also already have a formal semantics of most assembly instructions (all user instructions) and of larger part of (barely) reasonable interactions between C and assembly.
\bigskip
......@@ -44,21 +44,21 @@ For all this missing features, we need to define a model and express the semanti
\section{Mission}
The subject imply a lot of not very explored questions. This means it is possible to choose a very theoretical subject or, on the contrary, a subject with some subtle implementations.
The subject implies a lot of not very explored questions. This means it is possible to choose a very theoretical subject or, on the contrary, a subject with some subtle implementations.
The more interesting part is probably the abstraction of paging. We need a model of the processor, define the semantics of interesting parts of the language and the properties of interest. Secondly, we shall find a good abstraction. Possibly, we could consider an implementation.
The first part should be relatively quick and easy. The question of abstraction might be much more challenging.
We can also look at the problem of stack abstraction in mixed C-asm in the case where assembly read a deep call-frame. This need extra assumptions on the compilation.
We can also look at the problem of stack abstraction in mixed C-asm in the case where assembly read a deep call-frame. This need extra assumptions on the compilation and adequate abstraction.
\section{Requisites}
There is no special requisite beyond what you probably already know, except enthusiasm.
There is no special requisite other that what you probably already know, plus enthusiasm.
\section{The team}
The internship will take place in the \textsc{Inria} project-team \textsc{Antique}, which is in the computer science department of the ENS. \textsc{Antique} team, formerly named \textsc{Abstraction} is the world leader in abstract interpretation. Abstract interpretation is a unifying theory for approximations of mathematical structures~\cite{cousot1977abstract} that was invented in 1977 by Patrick \textsc{Cousot} (founder of \textsc{Abstraction} team). Abstract interpretation is base on the ideas that 1) the behavior of dynamical systems can be observed at various level of abstractions and that 2) the comparison of two abstraction levels can be formally defined by the intermediary of algebraic objects (such as relations, \textsc{Galois} connections, closure operators, ideals, etc.). Abstract interpretation can be used to provide a framework to several static analysis methods or to derive new static analyzers directly from the definition of an abstraction relation. \textsc{Abstraction} team, then \textsc{Antique} team, develop since 2001 the \textsc{Astree} static analyzer. \textsc{Astrée}~\cite{blanchet2003static} is a static analyzer able to automatically prove the absence of runtime errors of embedded software. \textsc{Astrée} is used in industrial applications, such as avionic, nuclear, automotive and astronautics, mainly in Europe and Asia.
The internship will take place in the \textsc{Inria} project-team \textsc{Antique}, which is in the computer science department of the ENS. \textsc{Antique} team, formerly named \textsc{Abstraction} is the world leader in abstract interpretation. Abstract interpretation is a unifying theory for approximations of mathematical structures~\cite{cousot1977abstract} that was invented in 1977 by Patrick \textsc{Cousot} (founder of \textsc{Abstraction} team). Abstract interpretation is based on the ideas that 1) the behavior of dynamical systems can be observed at various level of abstractions and that 2) the comparison of two abstraction levels can be formally defined by the intermediary of algebraic objects (such as relations, \textsc{Galois} connections, closure operators, ideals, etc.). Abstract interpretation can be used to provide a framework for several static analysis methods or to derive new static analyzers directly from the definition of an abstraction relation. \textsc{Abstraction} team, then \textsc{Antique} team, develops since 2001 the \textsc{Astrée} static analyzer. \textsc{Astrée}~\cite{blanchet2003static} is a static analyzer able to automatically prove the absence of runtime errors of embedded software. \textsc{Astrée} is used in industrial applications, such as avionic, nuclear, automotive and astronautics, mainly in Europe and Asia.
\emergencystretch=1000em
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment