Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
doctorat
seminaire_inria
Commits
0dcfbd1d
Commit
0dcfbd1d
authored
5 years ago
by
Marc
Browse files
Options
Download
Email Patches
Plain Diff
Still better?
parent
aeba632c
master
v1.0
No related merge requests found
Pipeline
#42
passed with stage
in 26 seconds
Changes
1
Pipelines
2
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
7 additions
and
7 deletions
+7
-7
seminaire.tex
seminaire.tex
+7
-7
No files found.
seminaire.tex
View file @
0dcfbd1d
...
...
@@ -295,17 +295,17 @@
\frametitle
{
\insertsubsection
{}
-- 2
$^
\text
{
nd
}$
iteration
}
\begin{ccode}
int i = 0; //
$
i
\in
[
0
,
0
]
$
while(i < 1000)
{
//
$
i
\in
[
0
,
1
]
=
[
0
,
0
]
\cup
^
\sharp
[
1
,
1
]
$
while(i < 1000)
{
//
$
i
\in
[
0
,
0
]
\cup
^
\sharp
[
1
,
1
]
=
[
0
,
1
]
$
i = i + 1; //
$
i
\in
[
1
,
2
]
$
}
\end{ccode}
\end{frame}
\begin{frame}
[fragile]
\frametitle
{
\insertsubsection
{}
-- 3
$^
\text
{
n
d
}$
iteration
}
\frametitle
{
\insertsubsection
{}
-- 3
$^
\text
{
r
d
}$
iteration
}
\begin{ccode}
int i = 0; //
$
i
\in
[
0
,
0
]
$
while(i < 1000)
{
//
$
i
\in
[
0
,
2
]
=
[
0
,
1
]
\cup
^
\sharp
[
1
,
2
]
$
while(i < 1000)
{
//
$
i
\in
[
0
,
1
]
\cup
^
\sharp
[
1
,
2
]
=
[
0
,
2
]
$
i = i + 1; //
$
i
\in
[
1
,
3
]
$
}
\end{ccode}
...
...
@@ -379,7 +379,7 @@
\frametitle
{
\insertsubsection
{}
-- 2
$^
\text
{
nd
}$
iteration
}
\begin{ccode}
int i = 0;
while(i < 1000)
{
//
$
i
\in
[
0
,
+
\infty
]
=
[
0
,
0
]
\nabla
[
1
,
1
]
$
while(i < 1000)
{
//
$
i
\in
[
0
,
0
]
\nabla
[
1
,
1
]
=
[
0
,
+
\infty
]
$
i = i + 1; //
$
i
\in
[
1
,
+
\infty
]
=
[
1
,
999
]
\cup
^
\sharp
[
1000
,
+
\infty
]
$
}
//
$
i
\in
[
1000
,
+
\infty
]
$
\end{ccode}
...
...
@@ -397,7 +397,7 @@
\vfill
We can sti
ff
refine the invariant a posteriori.
We can sti
ll
refine the invariant a posteriori.
\end{frame}
\section
{
Past and future
}
...
...
@@ -420,7 +420,7 @@
Bad things:
\begin{itemize}
\item
Incompleteness
\item
A lot of work if
current
domains are not powerful enough
\item
A lot of work if
existing
domains are not powerful enough
\item
Some properties are very difficult to prove with this method
\end{itemize}
\end{frame}
...
...
@@ -436,7 +436,7 @@
\vfill
Properties are not visible from C (
check some CPU's registers
, mainly): inline assembly
$
\Ra
$
analyze assembly. Impacts everything.
Properties are not visible from C (
about CPU state
, mainly): inline assembly
$
\Ra
$
analyze assembly. Impacts everything.
\end{frame}
...
...
This diff is collapsed.
Click to expand it.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment