WEBVTT
Kind: captions
Language: en

00:00:01.160 --> 00:00:06.690 align:start position:0%
 
[Music]

00:00:06.690 --> 00:00:06.700 align:start position:0%
 
 

00:00:06.700 --> 00:00:09.230 align:start position:0%
 
[Music]

00:00:09.230 --> 00:00:09.240 align:start position:0%
[Music]
 

00:00:09.240 --> 00:00:11.509 align:start position:0%
[Music]
hello<00:00:09.679><c> thank</c><00:00:09.960><c> you</c><00:00:10.360><c> so</c><00:00:10.559><c> my</c><00:00:10.679><c> name</c><00:00:10.840><c> is</c>

00:00:11.509 --> 00:00:11.519 align:start position:0%
hello thank you so my name is
 

00:00:11.519 --> 00:00:16.510 align:start position:0%
hello thank you so my name is
aov<00:00:12.519><c> um</c><00:00:13.320><c> the</c><00:00:13.519><c> slides</c><00:00:14.200><c> ah</c><00:00:14.400><c> here</c><00:00:14.639><c> the</c><00:00:14.920><c> slides</c><00:00:15.920><c> um</c>

00:00:16.510 --> 00:00:16.520 align:start position:0%
aov um the slides ah here the slides um
 

00:00:16.520 --> 00:00:18.510 align:start position:0%
aov um the slides ah here the slides um
happy<00:00:16.760><c> to</c><00:00:16.880><c> be</c><00:00:17.119><c> here</c><00:00:17.560><c> actually</c><00:00:17.880><c> this</c><00:00:18.000><c> is</c><00:00:18.199><c> work</c>

00:00:18.510 --> 00:00:18.520 align:start position:0%
happy to be here actually this is work
 

00:00:18.520 --> 00:00:22.070 align:start position:0%
happy to be here actually this is work
done<00:00:19.240><c> by</c><00:00:19.720><c> myself</c><00:00:20.480><c> uh</c><00:00:20.640><c> tan</c><00:00:20.920><c> hran</c><00:00:21.400><c> who's</c><00:00:21.800><c> also</c>

00:00:22.070 --> 00:00:22.080 align:start position:0%
done by myself uh tan hran who's also
 

00:00:22.080 --> 00:00:25.150 align:start position:0%
done by myself uh tan hran who's also
here<00:00:22.279><c> in</c><00:00:22.400><c> the</c><00:00:22.560><c> room</c><00:00:23.480><c> uh</c><00:00:23.599><c> EUR</c><00:00:24.000><c> C</c><00:00:24.439><c> Thomas</c><00:00:24.760><c> P</c><00:00:25.039><c> who</c>

00:00:25.150 --> 00:00:25.160 align:start position:0%
here in the room uh EUR C Thomas P who
 

00:00:25.160 --> 00:00:27.269 align:start position:0%
here in the room uh EUR C Thomas P who
is<00:00:25.279><c> also</c><00:00:25.560><c> here</c><00:00:25.840><c> and</c><00:00:26.080><c> Roberto</c><00:00:26.519><c> saltin</c><00:00:27.160><c> and</c>

00:00:27.269 --> 00:00:27.279 align:start position:0%
is also here and Roberto saltin and
 

00:00:27.279 --> 00:00:28.910 align:start position:0%
is also here and Roberto saltin and
we're<00:00:27.560><c> happy</c><00:00:27.840><c> to</c><00:00:28.039><c> have</c><00:00:28.279><c> done</c><00:00:28.480><c> this</c><00:00:28.640><c> work</c>

00:00:28.910 --> 00:00:28.920 align:start position:0%
we're happy to have done this work
 

00:00:28.920 --> 00:00:33.350 align:start position:0%
we're happy to have done this work
supported<00:00:29.320><c> by</c><00:00:29.480><c> serum</c><00:00:29.800><c> fun</c><00:00:30.439><c> found</c><00:00:31.880><c> so</c><00:00:32.880><c> if</c><00:00:33.000><c> you</c>

00:00:33.350 --> 00:00:33.360 align:start position:0%
supported by serum fun found so if you
 

00:00:33.360 --> 00:00:35.830 align:start position:0%
supported by serum fun found so if you
look<00:00:33.520><c> at</c><00:00:33.760><c> consensus</c><00:00:34.280><c> ethereum</c><00:00:34.760><c> consensus</c><00:00:35.760><c> uh</c>

00:00:35.830 --> 00:00:35.840 align:start position:0%
look at consensus ethereum consensus uh
 

00:00:35.840 --> 00:00:37.950 align:start position:0%
look at consensus ethereum consensus uh
you<00:00:36.040><c> probably</c><00:00:36.360><c> see</c><00:00:36.840><c> a</c><00:00:37.000><c> lot</c><00:00:37.160><c> of</c><00:00:37.320><c> algorithms</c>

00:00:37.950 --> 00:00:37.960 align:start position:0%
you probably see a lot of algorithms
 

00:00:37.960 --> 00:00:40.750 align:start position:0%
you probably see a lot of algorithms
starting<00:00:38.360><c> as</c><00:00:38.600><c> Casper</c><00:00:39.200><c> Gasper</c><00:00:40.160><c> now</c><00:00:40.320><c> we</c><00:00:40.480><c> have</c>

00:00:40.750 --> 00:00:40.760 align:start position:0%
starting as Casper Gasper now we have
 

00:00:40.760 --> 00:00:43.830 align:start position:0%
starting as Casper Gasper now we have
single<00:00:41.160><c> slot</c><00:00:41.840><c> finality</c><00:00:42.840><c> and</c><00:00:43.200><c> recently</c><00:00:43.600><c> on</c><00:00:43.719><c> the</c>

00:00:43.830 --> 00:00:43.840 align:start position:0%
single slot finality and recently on the
 

00:00:43.840 --> 00:00:46.950 align:start position:0%
single slot finality and recently on the
Block<00:00:44.160><c> we</c><00:00:44.360><c> have</c><00:00:44.879><c> uh</c><00:00:45.000><c> three</c><00:00:45.320><c> slot</c><00:00:45.840><c> finality</c><00:00:46.840><c> you</c>

00:00:46.950 --> 00:00:46.960 align:start position:0%
Block we have uh three slot finality you
 

00:00:46.960 --> 00:00:50.189 align:start position:0%
Block we have uh three slot finality you
can<00:00:47.199><c> check</c><00:00:47.879><c> uh</c><00:00:48.039><c> the</c><00:00:48.239><c> recent</c><00:00:48.800><c> report</c><00:00:49.719><c> uh</c><00:00:49.920><c> by</c>

00:00:50.189 --> 00:00:50.199 align:start position:0%
can check uh the recent report uh by
 

00:00:50.199 --> 00:00:53.790 align:start position:0%
can check uh the recent report uh by
Franchesco<00:00:50.879><c> Roberto</c><00:00:51.360><c> tanhai</c><00:00:51.840><c> and</c><00:00:52.480><c> Luca</c><00:00:53.480><c> and</c>

00:00:53.790 --> 00:00:53.800 align:start position:0%
Franchesco Roberto tanhai and Luca and
 

00:00:53.800 --> 00:00:55.990 align:start position:0%
Franchesco Roberto tanhai and Luca and
if<00:00:53.960><c> you</c><00:00:54.120><c> look</c><00:00:54.320><c> into</c><00:00:54.760><c> into</c><00:00:55.039><c> these</c><00:00:55.280><c> things</c><00:00:55.879><c> uh</c>

00:00:55.990 --> 00:00:56.000 align:start position:0%
if you look into into these things uh
 

00:00:56.000 --> 00:00:57.189 align:start position:0%
if you look into into these things uh
you<00:00:56.079><c> will</c><00:00:56.199><c> see</c><00:00:56.440><c> that</c><00:00:56.559><c> there</c><00:00:56.680><c> are</c><00:00:56.800><c> a</c><00:00:56.920><c> lot</c><00:00:57.039><c> of</c>

00:00:57.189 --> 00:00:57.199 align:start position:0%
you will see that there are a lot of
 

00:00:57.199 --> 00:00:59.549 align:start position:0%
you will see that there are a lot of
definitions<00:00:57.719><c> I</c><00:00:57.840><c> cannot</c><00:00:58.160><c> explain</c><00:00:58.600><c> all</c><00:00:58.760><c> of</c><00:00:58.960><c> you</c>

00:00:59.549 --> 00:00:59.559 align:start position:0%
definitions I cannot explain all of you
 

00:00:59.559 --> 00:01:01.990 align:start position:0%
definitions I cannot explain all of you
uh<00:01:00.000><c> all</c><00:01:00.120><c> these</c><00:01:00.320><c> definitions</c><00:01:00.840><c> to</c><00:01:01.039><c> you</c><00:01:01.680><c> you</c><00:01:01.800><c> will</c>

00:01:01.990 --> 00:01:02.000 align:start position:0%
uh all these definitions to you you will
 

00:01:02.000 --> 00:01:05.350 align:start position:0%
uh all these definitions to you you will
see<00:01:02.320><c> that</c><00:01:02.519><c> there</c><00:01:02.680><c> are</c><00:01:03.399><c> chain</c><00:01:03.760><c> blocks</c><00:01:04.280><c> slots</c><00:01:05.040><c> uh</c>

00:01:05.350 --> 00:01:05.360 align:start position:0%
see that there are chain blocks slots uh
 

00:01:05.360 --> 00:01:07.550 align:start position:0%
see that there are chain blocks slots uh
checkpoints<00:01:06.360><c> Justified</c><00:01:07.000><c> checkpoints</c>

00:01:07.550 --> 00:01:07.560 align:start position:0%
checkpoints Justified checkpoints
 

00:01:07.560 --> 00:01:09.630 align:start position:0%
checkpoints Justified checkpoints
finalized<00:01:08.119><c> checkpoints</c><00:01:09.119><c> votes</c><00:01:09.439><c> by</c>

00:01:09.630 --> 00:01:09.640 align:start position:0%
finalized checkpoints votes by
 

00:01:09.640 --> 00:01:12.270 align:start position:0%
finalized checkpoints votes by
validators<00:01:10.360><c> FFG</c><00:01:10.880><c> votes</c><00:01:11.600><c> uh</c><00:01:11.720><c> that</c><00:01:11.920><c> connect</c>

00:01:12.270 --> 00:01:12.280 align:start position:0%
validators FFG votes uh that connect
 

00:01:12.280 --> 00:01:14.830 align:start position:0%
validators FFG votes uh that connect
these<00:01:12.439><c> checkpoints</c><00:01:13.040><c> and</c><00:01:13.200><c> so</c><00:01:13.320><c> on</c><00:01:13.560><c> so</c><00:01:13.759><c> forth</c><00:01:14.560><c> so</c>

00:01:14.830 --> 00:01:14.840 align:start position:0%
these checkpoints and so on so forth so
 

00:01:14.840 --> 00:01:16.870 align:start position:0%
these checkpoints and so on so forth so
these<00:01:15.000><c> are</c><00:01:15.200><c> not</c><00:01:15.400><c> simple</c>

00:01:16.870 --> 00:01:16.880 align:start position:0%
these are not simple
 

00:01:16.880 --> 00:01:19.870 align:start position:0%
these are not simple
algorithms<00:01:17.880><c> so</c><00:01:18.080><c> in</c><00:01:18.200><c> our</c><00:01:18.439><c> work</c><00:01:18.720><c> we</c><00:01:18.880><c> don't</c><00:01:19.520><c> uh</c><00:01:19.720><c> we</c>

00:01:19.870 --> 00:01:19.880 align:start position:0%
algorithms so in our work we don't uh we
 

00:01:19.880 --> 00:01:22.429 align:start position:0%
algorithms so in our work we don't uh we
don't<00:01:20.200><c> have</c><00:01:20.720><c> uh</c><00:01:20.960><c> basically</c><00:01:21.360><c> time</c><00:01:21.640><c> budget</c><00:01:22.079><c> to</c>

00:01:22.429 --> 00:01:22.439 align:start position:0%
don't have uh basically time budget to
 

00:01:22.439 --> 00:01:25.270 align:start position:0%
don't have uh basically time budget to
to<00:01:23.159><c> do</c><00:01:23.479><c> everything</c><00:01:24.079><c> so</c><00:01:24.320><c> we</c><00:01:24.479><c> focus</c><00:01:24.920><c> on</c>

00:01:25.270 --> 00:01:25.280 align:start position:0%
to do everything so we focus on
 

00:01:25.280 --> 00:01:27.830 align:start position:0%
to do everything so we focus on
accountable<00:01:26.000><c> safety</c><00:01:27.000><c> which</c>

00:01:27.830 --> 00:01:27.840 align:start position:0%
accountable safety which
 

00:01:27.840 --> 00:01:30.149 align:start position:0%
accountable safety which
means<00:01:28.840><c> roughly</c><00:01:29.200><c> speaking</c><00:01:29.560><c> that</c><00:01:29.759><c> if</c><00:01:29.920><c> if</c><00:01:30.040><c> you</c>

00:01:30.149 --> 00:01:30.159 align:start position:0%
means roughly speaking that if if you
 

00:01:30.159 --> 00:01:32.789 align:start position:0%
means roughly speaking that if if you
have<00:01:30.320><c> a</c><00:01:30.439><c> fork</c><00:01:30.920><c> in</c><00:01:31.280><c> consensus</c><00:01:32.280><c> we</c><00:01:32.399><c> should</c><00:01:32.640><c> be</c>

00:01:32.789 --> 00:01:32.799 align:start position:0%
have a fork in consensus we should be
 

00:01:32.799 --> 00:01:36.350 align:start position:0%
have a fork in consensus we should be
able<00:01:33.079><c> to</c><00:01:33.280><c> identify</c><00:01:33.960><c> at</c><00:01:34.079><c> least</c><00:01:34.399><c> oneir</c><00:01:35.200><c> of</c><00:01:35.439><c> the</c>

00:01:36.350 --> 00:01:36.360 align:start position:0%
able to identify at least oneir of the
 

00:01:36.360 --> 00:01:38.670 align:start position:0%
able to identify at least oneir of the
uh<00:01:36.520><c> validators</c><00:01:37.520><c> that</c><00:01:37.720><c> are</c>

00:01:38.670 --> 00:01:38.680 align:start position:0%
uh validators that are
 

00:01:38.680 --> 00:01:41.310 align:start position:0%
uh validators that are
basically<00:01:39.680><c> uh</c><00:01:39.799><c> that</c><00:01:40.000><c> produce</c><00:01:40.399><c> this</c><00:01:40.560><c> fork</c><00:01:41.079><c> and</c>

00:01:41.310 --> 00:01:41.320 align:start position:0%
basically uh that produce this fork and
 

00:01:41.320 --> 00:01:43.990 align:start position:0%
basically uh that produce this fork and
they<00:01:41.439><c> should</c><00:01:41.640><c> be</c><00:01:42.079><c> slashed</c><00:01:43.079><c> so</c><00:01:43.280><c> we</c><00:01:43.479><c> focus</c><00:01:43.799><c> on</c>

00:01:43.990 --> 00:01:44.000 align:start position:0%
they should be slashed so we focus on
 

00:01:44.000 --> 00:01:47.069 align:start position:0%
they should be slashed so we focus on
accountable<00:01:44.520><c> safety</c><00:01:45.040><c> here</c><00:01:46.000><c> how</c><00:01:46.320><c> would</c><00:01:46.759><c> we</c><00:01:46.920><c> be</c>

00:01:47.069 --> 00:01:47.079 align:start position:0%
accountable safety here how would we be
 

00:01:47.079 --> 00:01:49.789 align:start position:0%
accountable safety here how would we be
able<00:01:47.320><c> to</c><00:01:47.520><c> check</c><00:01:48.000><c> that</c><00:01:48.240><c> these</c><00:01:48.479><c> protocols</c><00:01:49.479><c> uh</c>

00:01:49.789 --> 00:01:49.799 align:start position:0%
able to check that these protocols uh
 

00:01:49.799 --> 00:01:53.230 align:start position:0%
able to check that these protocols uh
namely<00:01:50.799><c> three</c><00:01:51.360><c> uh</c><00:01:51.479><c> three</c><00:01:51.759><c> slot</c><00:01:52.240><c> finality</c>

00:01:53.230 --> 00:01:53.240 align:start position:0%
namely three uh three slot finality
 

00:01:53.240 --> 00:01:56.230 align:start position:0%
namely three uh three slot finality
satisfy<00:01:53.880><c> accountable</c><00:01:54.479><c> safety</c><00:01:55.479><c> well</c><00:01:56.079><c> in</c>

00:01:56.230 --> 00:01:56.240 align:start position:0%
satisfy accountable safety well in
 

00:01:56.240 --> 00:01:58.910 align:start position:0%
satisfy accountable safety well in
science<00:01:56.640><c> fiction</c><00:01:57.240><c> solution</c><00:01:58.240><c> when</c><00:01:58.520><c> it's</c><00:01:58.680><c> all</c>

00:01:58.910 --> 00:01:58.920 align:start position:0%
science fiction solution when it's all
 

00:01:58.920 --> 00:02:01.990 align:start position:0%
science fiction solution when it's all
good<00:01:59.439><c> uh</c><00:01:59.560><c> we</c><00:01:59.680><c> would</c><00:01:59.960><c> take</c><00:02:00.200><c> the</c><00:02:00.960><c> code</c><00:02:01.280><c> in</c><00:02:01.520><c> Python</c>

00:02:01.990 --> 00:02:02.000 align:start position:0%
good uh we would take the code in Python
 

00:02:02.000 --> 00:02:04.350 align:start position:0%
good uh we would take the code in Python
we'll<00:02:02.280><c> take</c><00:02:02.439><c> the</c><00:02:02.600><c> executable</c><00:02:03.159><c> spec</c><00:02:03.399><c> in</c><00:02:03.600><c> Python</c>

00:02:04.350 --> 00:02:04.360 align:start position:0%
we'll take the executable spec in Python
 

00:02:04.360 --> 00:02:06.550 align:start position:0%
we'll take the executable spec in Python
produce<00:02:04.840><c> some</c><00:02:05.039><c> examples</c><00:02:05.600><c> maybe</c><00:02:05.920><c> to</c><00:02:06.119><c> convince</c>

00:02:06.550 --> 00:02:06.560 align:start position:0%
produce some examples maybe to convince
 

00:02:06.560 --> 00:02:09.309 align:start position:0%
produce some examples maybe to convince
ourselves<00:02:07.240><c> that</c><00:02:07.399><c> it</c><00:02:07.560><c> kind</c><00:02:07.680><c> of</c><00:02:07.880><c> works</c><00:02:08.840><c> but</c><00:02:09.000><c> also</c>

00:02:09.309 --> 00:02:09.319 align:start position:0%
ourselves that it kind of works but also
 

00:02:09.319 --> 00:02:11.550 align:start position:0%
ourselves that it kind of works but also
would<00:02:09.879><c> we</c><00:02:10.000><c> would</c><00:02:10.200><c> also</c><00:02:10.479><c> produce</c><00:02:10.879><c> an</c><00:02:11.039><c> automatic</c>

00:02:11.550 --> 00:02:11.560 align:start position:0%
would we would also produce an automatic
 

00:02:11.560 --> 00:02:14.190 align:start position:0%
would we would also produce an automatic
proof<00:02:11.959><c> of</c><00:02:12.319><c> accountable</c><00:02:13.200><c> safety</c>

00:02:14.190 --> 00:02:14.200 align:start position:0%
proof of accountable safety
 

00:02:14.200 --> 00:02:16.509 align:start position:0%
proof of accountable safety
unfortunately<00:02:15.160><c> that's</c><00:02:15.360><c> a</c><00:02:15.519><c> bit</c><00:02:15.720><c> of</c><00:02:16.160><c> Science</c>

00:02:16.509 --> 00:02:16.519 align:start position:0%
unfortunately that's a bit of Science
 

00:02:16.519 --> 00:02:18.350 align:start position:0%
unfortunately that's a bit of Science
Fiction<00:02:16.800><c> nowadays</c><00:02:17.599><c> there</c><00:02:17.720><c> are</c><00:02:17.920><c> no</c><00:02:18.120><c> of</c>

00:02:18.350 --> 00:02:18.360 align:start position:0%
Fiction nowadays there are no of
 

00:02:18.360 --> 00:02:19.949 align:start position:0%
Fiction nowadays there are no of
the-shelf<00:02:18.840><c> solutions</c><00:02:19.360><c> that</c><00:02:19.519><c> would</c><00:02:19.720><c> take</c>

00:02:19.949 --> 00:02:19.959 align:start position:0%
the-shelf solutions that would take
 

00:02:19.959 --> 00:02:22.670 align:start position:0%
the-shelf solutions that would take
executable<00:02:20.560><c> python</c><00:02:20.920><c> spec</c><00:02:21.599><c> and</c><00:02:21.800><c> reason</c><00:02:22.160><c> about</c>

00:02:22.670 --> 00:02:22.680 align:start position:0%
executable python spec and reason about
 

00:02:22.680 --> 00:02:25.350 align:start position:0%
executable python spec and reason about
such<00:02:23.040><c> complex</c><00:02:23.480><c> algorithms</c><00:02:24.319><c> as</c>

00:02:25.350 --> 00:02:25.360 align:start position:0%
such complex algorithms as
 

00:02:25.360 --> 00:02:27.830 align:start position:0%
such complex algorithms as
consensus<00:02:26.360><c> so</c><00:02:26.599><c> what</c><00:02:26.760><c> we</c><00:02:26.920><c> have</c><00:02:27.080><c> been</c><00:02:27.239><c> doing</c><00:02:27.640><c> in</c>

00:02:27.830 --> 00:02:27.840 align:start position:0%
consensus so what we have been doing in
 

00:02:27.840 --> 00:02:30.509 align:start position:0%
consensus so what we have been doing in
this<00:02:28.080><c> project</c><00:02:28.640><c> we</c><00:02:28.959><c> actually</c>

00:02:30.509 --> 00:02:30.519 align:start position:0%
this project we actually
 

00:02:30.519 --> 00:02:33.110 align:start position:0%
this project we actually
uh<00:02:30.680><c> VI</c><00:02:30.959><c> writing</c><00:02:31.720><c> uh</c><00:02:31.879><c> specifications</c><00:02:32.840><c> in</c>

00:02:33.110 --> 00:02:33.120 align:start position:0%
uh VI writing uh specifications in
 

00:02:33.120 --> 00:02:34.949 align:start position:0%
uh VI writing uh specifications in
temperal<00:02:33.519><c> logic</c><00:02:33.959><c> factions</c><00:02:34.640><c> that's</c><00:02:34.800><c> a</c>

00:02:34.949 --> 00:02:34.959 align:start position:0%
temperal logic factions that's a
 

00:02:34.959 --> 00:02:36.869 align:start position:0%
temperal logic factions that's a
language<00:02:35.400><c> invented</c><00:02:35.879><c> by</c><00:02:36.000><c> Les</c><00:02:36.280><c> Lampard</c><00:02:36.680><c> some</c>

00:02:36.869 --> 00:02:36.879 align:start position:0%
language invented by Les Lampard some
 

00:02:36.879 --> 00:02:39.270 align:start position:0%
language invented by Les Lampard some
time<00:02:37.040><c> ago</c><00:02:37.599><c> for</c><00:02:37.879><c> reason</c><00:02:38.239><c> about</c><00:02:38.599><c> concurrent</c><00:02:39.040><c> and</c>

00:02:39.270 --> 00:02:39.280 align:start position:0%
time ago for reason about concurrent and
 

00:02:39.280 --> 00:02:41.030 align:start position:0%
time ago for reason about concurrent and
distributed

00:02:41.030 --> 00:02:41.040 align:start position:0%
distributed
 

00:02:41.040 --> 00:02:44.589 align:start position:0%
distributed
systems<00:02:42.040><c> um</c><00:02:42.519><c> and</c><00:02:42.680><c> we</c><00:02:42.840><c> did</c><00:02:43.200><c> we</c><00:02:43.319><c> did</c><00:02:43.640><c> produce</c>

00:02:44.589 --> 00:02:44.599 align:start position:0%
systems um and we did we did produce
 

00:02:44.599 --> 00:02:46.309 align:start position:0%
systems um and we did we did produce
specifications<00:02:45.280><c> by</c><00:02:45.480><c> hand</c><00:02:45.800><c> because</c><00:02:46.040><c> there</c><00:02:46.120><c> are</c>

00:02:46.309 --> 00:02:46.319 align:start position:0%
specifications by hand because there are
 

00:02:46.319 --> 00:02:48.030 align:start position:0%
specifications by hand because there are
no<00:02:46.519><c> tools</c><00:02:47.040><c> that</c><00:02:47.200><c> would</c><00:02:47.319><c> be</c><00:02:47.440><c> able</c><00:02:47.640><c> to</c><00:02:47.760><c> do</c><00:02:47.879><c> it</c>

00:02:48.030 --> 00:02:48.040 align:start position:0%
no tools that would be able to do it
 

00:02:48.040 --> 00:02:49.550 align:start position:0%
no tools that would be able to do it
although<00:02:48.319><c> we</c><00:02:48.440><c> have</c><00:02:48.599><c> been</c><00:02:48.760><c> thinking</c><00:02:49.159><c> how</c><00:02:49.360><c> we</c>

00:02:49.550 --> 00:02:49.560 align:start position:0%
although we have been thinking how we
 

00:02:49.560 --> 00:02:51.869 align:start position:0%
although we have been thinking how we
could<00:02:49.920><c> automate</c><00:02:50.440><c> that</c><00:02:51.159><c> so</c><00:02:51.400><c> basically</c><00:02:51.760><c> the</c>

00:02:51.869 --> 00:02:51.879 align:start position:0%
could automate that so basically the
 

00:02:51.879 --> 00:02:53.630 align:start position:0%
could automate that so basically the
first<00:02:52.120><c> specification</c><00:02:52.640><c> we</c><00:02:52.800><c> wrote</c><00:02:53.159><c> was</c><00:02:53.440><c> just</c>

00:02:53.630 --> 00:02:53.640 align:start position:0%
first specification we wrote was just
 

00:02:53.640 --> 00:02:56.430 align:start position:0%
first specification we wrote was just
two<00:02:53.920><c> complex</c><00:02:54.319><c> for</c><00:02:54.480><c> the</c><00:02:54.560><c> model</c><00:02:55.120><c> Checkers</c><00:02:56.120><c> uh</c><00:02:56.239><c> we</c>

00:02:56.430 --> 00:02:56.440 align:start position:0%
two complex for the model Checkers uh we
 

00:02:56.440 --> 00:02:59.030 align:start position:0%
two complex for the model Checkers uh we
greatly<00:02:56.959><c> produced</c><00:02:57.599><c> obstructions</c><00:02:58.440><c> using</c><00:02:58.800><c> this</c>

00:02:59.030 --> 00:02:59.040 align:start position:0%
greatly produced obstructions using this
 

00:02:59.040 --> 00:03:00.350 align:start position:0%
greatly produced obstructions using this
specification

00:03:00.350 --> 00:03:00.360 align:start position:0%
specification
 

00:03:00.360 --> 00:03:01.869 align:start position:0%
specification
and<00:03:00.599><c> essentially</c><00:03:01.120><c> produced</c><00:03:01.480><c> like</c><00:03:01.599><c> four</c>

00:03:01.869 --> 00:03:01.879 align:start position:0%
and essentially produced like four
 

00:03:01.879 --> 00:03:03.990 align:start position:0%
and essentially produced like four
levels<00:03:02.159><c> of</c><00:03:02.360><c> obstructions</c><00:03:03.080><c> here</c><00:03:03.360><c> so</c><00:03:03.599><c> the</c><00:03:03.760><c> model</c>

00:03:03.990 --> 00:03:04.000 align:start position:0%
levels of obstructions here so the model
 

00:03:04.000 --> 00:03:06.670 align:start position:0%
levels of obstructions here so the model
Checker<00:03:04.440><c> could</c><00:03:04.879><c> handle</c><00:03:05.879><c> uh</c><00:03:06.040><c> the</c><00:03:06.200><c> complexity</c>

00:03:06.670 --> 00:03:06.680 align:start position:0%
Checker could handle uh the complexity
 

00:03:06.680 --> 00:03:08.390 align:start position:0%
Checker could handle uh the complexity
of<00:03:06.799><c> the</c><00:03:06.920><c> algorithm</c><00:03:07.360><c> in</c><00:03:07.480><c> the</c><00:03:07.599><c> end</c><00:03:07.879><c> we</c><00:03:08.000><c> used</c><00:03:08.280><c> the</c>

00:03:08.390 --> 00:03:08.400 align:start position:0%
of the algorithm in the end we used the
 

00:03:08.400 --> 00:03:11.509 align:start position:0%
of the algorithm in the end we used the
model<00:03:08.680><c> check</c><00:03:09.360><c> palache</c><00:03:10.360><c> which</c><00:03:10.959><c> uh</c><00:03:11.239><c> is</c>

00:03:11.509 --> 00:03:11.519 align:start position:0%
model check palache which uh is
 

00:03:11.519 --> 00:03:13.589 align:start position:0%
model check palache which uh is
offloading<00:03:12.120><c> the</c><00:03:12.239><c> verification</c><00:03:12.840><c> task</c><00:03:13.159><c> to</c><00:03:13.319><c> the</c>

00:03:13.589 --> 00:03:13.599 align:start position:0%
offloading the verification task to the
 

00:03:13.599 --> 00:03:17.149 align:start position:0%
offloading the verification task to the
smt<00:03:14.000><c> solver</c><00:03:14.879><c> Z3</c><00:03:15.879><c> and</c><00:03:16.080><c> in</c><00:03:16.239><c> addition</c><00:03:16.560><c> to</c><00:03:16.760><c> that</c><00:03:17.000><c> as</c>

00:03:17.149 --> 00:03:17.159 align:start position:0%
smt solver Z3 and in addition to that as
 

00:03:17.159 --> 00:03:20.229 align:start position:0%
smt solver Z3 and in addition to that as
things<00:03:17.519><c> were</c><00:03:17.680><c> a</c><00:03:17.760><c> bit</c><00:03:17.959><c> slow</c><00:03:18.879><c> we</c><00:03:19.120><c> also</c><00:03:19.480><c> wrote</c><00:03:20.040><c> a</c>

00:03:20.229 --> 00:03:20.239 align:start position:0%
things were a bit slow we also wrote a
 

00:03:20.239 --> 00:03:22.470 align:start position:0%
things were a bit slow we also wrote a
specification<00:03:21.040><c> in</c><00:03:21.319><c> alloy</c><00:03:21.799><c> which</c><00:03:21.920><c> is</c><00:03:22.080><c> also</c><00:03:22.360><c> a</c>

00:03:22.470 --> 00:03:22.480 align:start position:0%
specification in alloy which is also a
 

00:03:22.480 --> 00:03:24.949 align:start position:0%
specification in alloy which is also a
well-known<00:03:22.920><c> model</c><00:03:23.200><c> Checker</c><00:03:24.200><c> that</c><00:03:24.440><c> is</c><00:03:24.640><c> backed</c>

00:03:24.949 --> 00:03:24.959 align:start position:0%
well-known model Checker that is backed
 

00:03:24.959 --> 00:03:27.910 align:start position:0%
well-known model Checker that is backed
by<00:03:25.159><c> aat</c><00:03:25.680><c> solver</c><00:03:26.680><c> and</c><00:03:26.840><c> in</c><00:03:27.040><c> addition</c><00:03:27.360><c> to</c><00:03:27.560><c> that</c><00:03:27.720><c> we</c>

00:03:27.910 --> 00:03:27.920 align:start position:0%
by aat solver and in addition to that we
 

00:03:27.920 --> 00:03:30.630 align:start position:0%
by aat solver and in addition to that we
wrote<00:03:28.439><c> uh</c><00:03:28.599><c> smt</c><00:03:29.120><c> constraints</c>

00:03:30.630 --> 00:03:30.640 align:start position:0%
wrote uh smt constraints
 

00:03:30.640 --> 00:03:33.910 align:start position:0%
wrote uh smt constraints
in<00:03:31.640><c> uh</c><00:03:31.760><c> CVC</c><00:03:32.319><c> 5</c><00:03:32.599><c> using</c><00:03:32.840><c> the</c><00:03:32.959><c> theory</c><00:03:33.319><c> of</c><00:03:33.519><c> finite</c>

00:03:33.910 --> 00:03:33.920 align:start position:0%
in uh CVC 5 using the theory of finite
 

00:03:33.920 --> 00:03:36.270 align:start position:0%
in uh CVC 5 using the theory of finite
sets<00:03:34.159><c> and</c><00:03:34.439><c> cardinalities</c><00:03:35.439><c> so</c><00:03:35.599><c> we</c><00:03:35.799><c> kind</c><00:03:35.959><c> of</c><00:03:36.120><c> did</c>

00:03:36.270 --> 00:03:36.280 align:start position:0%
sets and cardinalities so we kind of did
 

00:03:36.280 --> 00:03:38.830 align:start position:0%
sets and cardinalities so we kind of did
a<00:03:36.400><c> lot</c><00:03:36.560><c> of</c><00:03:36.760><c> experiments</c><00:03:37.360><c> here</c><00:03:37.640><c> to</c><00:03:38.439><c> check</c>

00:03:38.830 --> 00:03:38.840 align:start position:0%
a lot of experiments here to check
 

00:03:38.840 --> 00:03:41.949 align:start position:0%
a lot of experiments here to check
accountable<00:03:39.400><c> safety</c><00:03:39.799><c> on</c><00:03:40.040><c> the</c><00:03:40.599><c> different</c><00:03:41.599><c> uh</c>

00:03:41.949 --> 00:03:41.959 align:start position:0%
accountable safety on the different uh
 

00:03:41.959 --> 00:03:43.110 align:start position:0%
accountable safety on the different uh
using<00:03:42.319><c> different</c>

00:03:43.110 --> 00:03:43.120 align:start position:0%
using different
 

00:03:43.120 --> 00:03:46.670 align:start position:0%
using different
tools<00:03:44.120><c> so</c><00:03:44.840><c> as</c><00:03:44.920><c> I</c><00:03:45.080><c> told</c><00:03:45.280><c> you</c><00:03:45.640><c> model</c><00:03:45.959><c> checking</c><00:03:46.560><c> uh</c>

00:03:46.670 --> 00:03:46.680 align:start position:0%
tools so as I told you model checking uh
 

00:03:46.680 --> 00:03:48.429 align:start position:0%
tools so as I told you model checking uh
could<00:03:46.879><c> help</c><00:03:47.080><c> you</c><00:03:47.280><c> how</c><00:03:47.480><c> can</c><00:03:47.599><c> it</c><00:03:47.799><c> help</c><00:03:48.000><c> you</c><00:03:48.280><c> the</c>

00:03:48.429 --> 00:03:48.439 align:start position:0%
could help you how can it help you the
 

00:03:48.439 --> 00:03:50.070 align:start position:0%
could help you how can it help you the
first<00:03:48.680><c> thing</c><00:03:49.080><c> where</c><00:03:49.159><c> it</c><00:03:49.280><c> can</c><00:03:49.480><c> help</c><00:03:49.720><c> you</c><00:03:49.879><c> is</c>

00:03:50.070 --> 00:03:50.080 align:start position:0%
first thing where it can help you is
 

00:03:50.080 --> 00:03:51.589 align:start position:0%
first thing where it can help you is
actually<00:03:50.319><c> you</c><00:03:50.439><c> can</c><00:03:50.640><c> qu</c><00:03:50.959><c> for</c><00:03:51.120><c> interest</c><00:03:51.439><c> in</c>

00:03:51.589 --> 00:03:51.599 align:start position:0%
actually you can qu for interest in
 

00:03:51.599 --> 00:03:53.710 align:start position:0%
actually you can qu for interest in
States<00:03:52.360><c> if</c><00:03:52.480><c> you</c><00:03:52.599><c> have</c><00:03:52.720><c> a</c><00:03:52.840><c> large</c><00:03:53.159><c> protocol</c><00:03:53.519><c> it's</c>

00:03:53.710 --> 00:03:53.720 align:start position:0%
States if you have a large protocol it's
 

00:03:53.720 --> 00:03:56.229 align:start position:0%
States if you have a large protocol it's
not<00:03:53.879><c> easy</c><00:03:54.120><c> to</c><00:03:54.280><c> produce</c><00:03:54.920><c> examples</c><00:03:55.920><c> and</c><00:03:56.079><c> that's</c>

00:03:56.229 --> 00:03:56.239 align:start position:0%
not easy to produce examples and that's
 

00:03:56.239 --> 00:03:58.030 align:start position:0%
not easy to produce examples and that's
what<00:03:56.360><c> model</c><00:03:56.640><c> checking</c><00:03:56.920><c> is</c><00:03:57.079><c> good</c><00:03:57.319><c> about</c><00:03:57.879><c> for</c>

00:03:58.030 --> 00:03:58.040 align:start position:0%
what model checking is good about for
 

00:03:58.040 --> 00:04:00.670 align:start position:0%
what model checking is good about for
instance<00:03:58.640><c> here</c><00:03:59.360><c> I'm</c><00:03:59.519><c> just</c><00:04:00.120><c> writing</c><00:04:00.519><c> an</c>

00:04:00.670 --> 00:04:00.680 align:start position:0%
instance here I'm just writing an
 

00:04:00.680 --> 00:04:02.470 align:start position:0%
instance here I'm just writing an
invariant<00:04:01.120><c> saying</c><00:04:01.480><c> there</c><00:04:01.599><c> are</c><00:04:01.799><c> no</c><00:04:02.079><c> two</c>

00:04:02.470 --> 00:04:02.480 align:start position:0%
invariant saying there are no two
 

00:04:02.480 --> 00:04:04.270 align:start position:0%
invariant saying there are no two
conflicting<00:04:03.000><c> blocks</c><00:04:03.439><c> basically</c><00:04:03.840><c> there</c><00:04:03.959><c> is</c><00:04:04.079><c> no</c>

00:04:04.270 --> 00:04:04.280 align:start position:0%
conflicting blocks basically there is no
 

00:04:04.280 --> 00:04:06.630 align:start position:0%
conflicting blocks basically there is no
fork<00:04:05.079><c> and</c><00:04:05.319><c> challenge</c><00:04:05.920><c> the</c><00:04:06.040><c> model</c><00:04:06.280><c> Checker</c>

00:04:06.630 --> 00:04:06.640 align:start position:0%
fork and challenge the model Checker
 

00:04:06.640 --> 00:04:08.789 align:start position:0%
fork and challenge the model Checker
with<00:04:06.760><c> this</c><00:04:06.959><c> false</c><00:04:07.280><c> invariant</c><00:04:08.239><c> then</c><00:04:08.439><c> the</c><00:04:08.560><c> model</c>

00:04:08.789 --> 00:04:08.799 align:start position:0%
with this false invariant then the model
 

00:04:08.799 --> 00:04:10.670 align:start position:0%
with this false invariant then the model
Checker<00:04:09.200><c> comes</c><00:04:09.480><c> back</c><00:04:09.680><c> in</c><00:04:09.840><c> several</c><00:04:10.200><c> minutes</c>

00:04:10.670 --> 00:04:10.680 align:start position:0%
Checker comes back in several minutes
 

00:04:10.680 --> 00:04:13.630 align:start position:0%
Checker comes back in several minutes
and<00:04:10.879><c> shows</c><00:04:11.239><c> me</c><00:04:11.799><c> an</c><00:04:12.000><c> example</c><00:04:12.680><c> so</c><00:04:13.319><c> actually</c>

00:04:13.630 --> 00:04:13.640 align:start position:0%
and shows me an example so actually
 

00:04:13.640 --> 00:04:15.830 align:start position:0%
and shows me an example so actually
these<00:04:13.840><c> tools</c><00:04:14.519><c> uh</c><00:04:14.680><c> work</c><00:04:15.280><c> uh</c><00:04:15.400><c> as</c><00:04:15.519><c> a</c><00:04:15.640><c> good</c>

00:04:15.830 --> 00:04:15.840 align:start position:0%
these tools uh work uh as a good
 

00:04:15.840 --> 00:04:17.590 align:start position:0%
these tools uh work uh as a good
communication<00:04:16.359><c> tool</c><00:04:16.600><c> for</c><00:04:16.799><c> protocol</c>

00:04:17.590 --> 00:04:17.600 align:start position:0%
communication tool for protocol
 

00:04:17.600 --> 00:04:20.270 align:start position:0%
communication tool for protocol
designers<00:04:18.600><c> he</c><00:04:18.759><c> is</c><00:04:18.880><c> an</c><00:04:19.079><c> example</c><00:04:19.680><c> of</c><00:04:19.880><c> such</c><00:04:20.040><c> an</c>

00:04:20.270 --> 00:04:20.280 align:start position:0%
designers he is an example of such an
 

00:04:20.280 --> 00:04:21.830 align:start position:0%
designers he is an example of such an
execution<00:04:20.759><c> you</c><00:04:20.840><c> don't</c><00:04:21.079><c> have</c><00:04:21.199><c> to</c><00:04:21.320><c> read</c><00:04:21.519><c> it</c><00:04:21.639><c> it's</c>

00:04:21.830 --> 00:04:21.840 align:start position:0%
execution you don't have to read it it's
 

00:04:21.840 --> 00:04:24.030 align:start position:0%
execution you don't have to read it it's
just<00:04:22.040><c> laan</c><00:04:22.479><c> but</c><00:04:22.600><c> it's</c><00:04:22.759><c> machine</c><00:04:23.120><c> readable</c><00:04:23.800><c> and</c>

00:04:24.030 --> 00:04:24.040 align:start position:0%
just laan but it's machine readable and
 

00:04:24.040 --> 00:04:27.070 align:start position:0%
just laan but it's machine readable and
it's<00:04:24.320><c> an</c><00:04:24.479><c> actual</c><00:04:25.040><c> execution</c><00:04:26.040><c> in</c><00:04:26.360><c> in</c><00:04:26.479><c> this</c>

00:04:27.070 --> 00:04:27.080 align:start position:0%
it's an actual execution in in this
 

00:04:27.080 --> 00:04:29.390 align:start position:0%
it's an actual execution in in this
specification<00:04:28.080><c> so</c><00:04:28.320><c> the</c><00:04:28.479><c> second</c><00:04:28.759><c> thing</c><00:04:29.120><c> where</c>

00:04:29.390 --> 00:04:29.400 align:start position:0%
specification so the second thing where
 

00:04:29.400 --> 00:04:31.629 align:start position:0%
specification so the second thing where
this<00:04:29.720><c> tools</c><00:04:29.960><c> can</c><00:04:30.160><c> help</c><00:04:30.400><c> you</c><00:04:30.720><c> is</c><00:04:30.880><c> to</c><00:04:31.039><c> show</c><00:04:31.360><c> some</c>

00:04:31.629 --> 00:04:31.639 align:start position:0%
this tools can help you is to show some
 

00:04:31.639 --> 00:04:34.550 align:start position:0%
this tools can help you is to show some
properties<00:04:32.639><c> uh</c><00:04:32.880><c> not</c><00:04:33.080><c> for</c><00:04:33.400><c> all</c><00:04:33.639><c> kinds</c><00:04:33.919><c> of</c><00:04:34.400><c> uh</c>

00:04:34.550 --> 00:04:34.560 align:start position:0%
properties uh not for all kinds of uh
 

00:04:34.560 --> 00:04:37.230 align:start position:0%
properties uh not for all kinds of uh
values<00:04:35.160><c> but</c><00:04:35.520><c> for</c><00:04:35.759><c> small</c><00:04:36.080><c> scopes</c><00:04:36.560><c> for</c><00:04:36.759><c> small</c>

00:04:37.230 --> 00:04:37.240 align:start position:0%
values but for small scopes for small
 

00:04:37.240 --> 00:04:39.629 align:start position:0%
values but for small scopes for small
parameters<00:04:38.240><c> for</c><00:04:38.440><c> instance</c><00:04:38.919><c> here</c><00:04:39.199><c> we</c><00:04:39.360><c> have</c>

00:04:39.629 --> 00:04:39.639 align:start position:0%
parameters for instance here we have
 

00:04:39.639 --> 00:04:41.430 align:start position:0%
parameters for instance here we have
experiments<00:04:40.120><c> for</c><00:04:40.440><c> five</c><00:04:40.680><c> blocks</c><00:04:41.080><c> seven</c>

00:04:41.430 --> 00:04:41.440 align:start position:0%
experiments for five blocks seven
 

00:04:41.440 --> 00:04:45.230 align:start position:0%
experiments for five blocks seven
checkpoints<00:04:42.440><c> 24</c><00:04:43.039><c> vots</c><00:04:44.000><c> and</c><00:04:44.240><c> as</c><00:04:44.360><c> you</c><00:04:44.479><c> can</c><00:04:44.680><c> see</c>

00:04:45.230 --> 00:04:45.240 align:start position:0%
checkpoints 24 vots and as you can see
 

00:04:45.240 --> 00:04:47.749 align:start position:0%
checkpoints 24 vots and as you can see
when<00:04:45.440><c> we</c><00:04:45.759><c> increase</c><00:04:46.240><c> the</c><00:04:46.400><c> parameter</c><00:04:46.960><c> space</c><00:04:47.639><c> the</c>

00:04:47.749 --> 00:04:47.759 align:start position:0%
when we increase the parameter space the
 

00:04:47.759 --> 00:04:49.670 align:start position:0%
when we increase the parameter space the
tools<00:04:48.400><c> uh</c><00:04:48.520><c> slow</c><00:04:48.880><c> down</c>

00:04:49.670 --> 00:04:49.680 align:start position:0%
tools uh slow down
 

00:04:49.680 --> 00:04:51.510 align:start position:0%
tools uh slow down
dramatically<00:04:50.680><c> however</c><00:04:50.919><c> we</c><00:04:51.120><c> have</c><00:04:51.280><c> some</c>

00:04:51.510 --> 00:04:51.520 align:start position:0%
dramatically however we have some
 

00:04:51.520 --> 00:04:53.430 align:start position:0%
dramatically however we have some
evidence<00:04:52.199><c> uh</c><00:04:52.320><c> that</c><00:04:52.520><c> these</c><00:04:52.720><c> properties</c><00:04:53.160><c> hold</c>

00:04:53.430 --> 00:04:53.440 align:start position:0%
evidence uh that these properties hold
 

00:04:53.440 --> 00:04:56.629 align:start position:0%
evidence uh that these properties hold
true<00:04:54.440><c> at</c><00:04:54.560><c> least</c><00:04:54.880><c> for</c><00:04:55.120><c> the</c><00:04:55.360><c> small</c><00:04:55.880><c> parameters</c>

00:04:56.629 --> 00:04:56.639 align:start position:0%
true at least for the small parameters
 

00:04:56.639 --> 00:04:58.790 align:start position:0%
true at least for the small parameters
and<00:04:56.800><c> that's</c><00:04:57.080><c> again</c><00:04:57.520><c> fast</c><00:04:57.800><c> feedback</c><00:04:58.560><c> that</c><00:04:58.680><c> you</c>

00:04:58.790 --> 00:04:58.800 align:start position:0%
and that's again fast feedback that you
 

00:04:58.800 --> 00:05:02.189 align:start position:0%
and that's again fast feedback that you
can<00:04:59.039><c> get</c><00:04:59.280><c> without</c><00:04:59.759><c> proven</c><00:05:00.160><c> things</c><00:05:00.639><c> in</c><00:05:01.199><c> heavy</c>

00:05:02.189 --> 00:05:02.199 align:start position:0%
can get without proven things in heavy
 

00:05:02.199 --> 00:05:05.670 align:start position:0%
can get without proven things in heavy
tools<00:05:03.199><c> so</c><00:05:04.000><c> to</c><00:05:04.199><c> come</c><00:05:04.479><c> to</c><00:05:04.639><c> the</c><00:05:04.759><c> summary</c><00:05:05.280><c> of</c><00:05:05.520><c> of</c>

00:05:05.670 --> 00:05:05.680 align:start position:0%
tools so to come to the summary of of
 

00:05:05.680 --> 00:05:07.510 align:start position:0%
tools so to come to the summary of of
our<00:05:05.880><c> work</c><00:05:06.479><c> we</c><00:05:06.600><c> believe</c><00:05:06.840><c> that</c><00:05:06.960><c> mche</c><00:05:07.400><c> can</c>

00:05:07.510 --> 00:05:07.520 align:start position:0%
our work we believe that mche can
 

00:05:07.520 --> 00:05:09.909 align:start position:0%
our work we believe that mche can
actually<00:05:07.919><c> helps</c><00:05:08.520><c> in</c><00:05:08.840><c> ensuring</c><00:05:09.400><c> correctness</c>

00:05:09.909 --> 00:05:09.919 align:start position:0%
actually helps in ensuring correctness
 

00:05:09.919 --> 00:05:12.830 align:start position:0%
actually helps in ensuring correctness
of<00:05:10.600><c> protocols</c><00:05:11.600><c> uh</c><00:05:11.840><c> we</c><00:05:12.000><c> still</c><00:05:12.160><c> need</c><00:05:12.400><c> humans</c><00:05:12.720><c> in</c>

00:05:12.830 --> 00:05:12.840 align:start position:0%
of protocols uh we still need humans in
 

00:05:12.840 --> 00:05:15.189 align:start position:0%
of protocols uh we still need humans in
the<00:05:12.960><c> loops</c><00:05:13.360><c> unfortunately</c><00:05:14.160><c> we</c><00:05:14.320><c> still</c><00:05:14.520><c> need</c><00:05:14.800><c> us</c>

00:05:15.189 --> 00:05:15.199 align:start position:0%
the loops unfortunately we still need us
 

00:05:15.199 --> 00:05:17.670 align:start position:0%
the loops unfortunately we still need us
basically<00:05:15.720><c> to</c><00:05:16.039><c> construct</c><00:05:16.520><c> this</c><00:05:17.080><c> abstractions</c>

00:05:17.670 --> 00:05:17.680 align:start position:0%
basically to construct this abstractions
 

00:05:17.680 --> 00:05:18.590 align:start position:0%
basically to construct this abstractions
and

00:05:18.590 --> 00:05:18.600 align:start position:0%
and
 

00:05:18.600 --> 00:05:20.390 align:start position:0%
and
specifications<00:05:19.600><c> uh</c><00:05:19.720><c> tune</c><00:05:19.960><c> in</c><00:05:20.120><c> for</c><00:05:20.280><c> the</c>

00:05:20.390 --> 00:05:20.400 align:start position:0%
specifications uh tune in for the
 

00:05:20.400 --> 00:05:21.870 align:start position:0%
specifications uh tune in for the
upcoming<00:05:20.800><c> technical</c><00:05:21.199><c> report</c><00:05:21.520><c> we</c><00:05:21.639><c> are</c><00:05:21.720><c> going</c>

00:05:21.870 --> 00:05:21.880 align:start position:0%
upcoming technical report we are going
 

00:05:21.880 --> 00:05:24.510 align:start position:0%
upcoming technical report we are going
to<00:05:22.080><c> publish</c><00:05:22.400><c> all</c><00:05:22.520><c> of</c><00:05:22.720><c> it</c><00:05:23.000><c> and</c><00:05:23.160><c> you'll</c><00:05:23.400><c> see</c><00:05:23.560><c> it</c>

00:05:24.510 --> 00:05:24.520 align:start position:0%
to publish all of it and you'll see it
 

00:05:24.520 --> 00:05:26.189 align:start position:0%
to publish all of it and you'll see it
and<00:05:24.680><c> thank</c><00:05:24.880><c> you</c><00:05:25.080><c> eum</c><00:05:25.479><c> foundation</c><00:05:25.800><c> for</c><00:05:26.000><c> giving</c>

00:05:26.189 --> 00:05:26.199 align:start position:0%
and thank you eum foundation for giving
 

00:05:26.199 --> 00:05:31.110 align:start position:0%
and thank you eum foundation for giving
us<00:05:26.280><c> a</c><00:05:26.440><c> grant</c><00:05:26.960><c> thanks</c><00:05:27.199><c> a</c><00:05:27.319><c> lot</c>

00:05:31.110 --> 00:05:31.120 align:start position:0%
 
 

00:05:31.120 --> 00:05:32.309 align:start position:0%
 
thank<00:05:31.280><c> you</c>

00:05:32.309 --> 00:05:32.319 align:start position:0%
thank you
 

00:05:32.319 --> 00:05:39.230 align:start position:0%
thank you
Igor<00:05:33.319><c> does</c><00:05:33.520><c> anybody</c><00:05:33.960><c> have</c><00:05:34.560><c> any</c>

00:05:39.230 --> 00:05:39.240 align:start position:0%
 
 

00:05:39.240 --> 00:05:50.790 align:start position:0%
 
question<00:05:40.240><c> okay</c>

00:05:50.790 --> 00:05:50.800 align:start position:0%
 
 

00:05:50.800 --> 00:05:53.950 align:start position:0%
 
okay<00:05:51.800><c> I</c><00:05:51.880><c> think</c><00:05:52.080><c> it</c><00:05:52.240><c> was</c><00:05:52.479><c> very</c><00:05:52.720><c> clear</c><00:05:53.520><c> nobody</c>

00:05:53.950 --> 00:05:53.960 align:start position:0%
okay I think it was very clear nobody
 

00:05:53.960 --> 00:06:03.189 align:start position:0%
okay I think it was very clear nobody
has<00:05:54.199><c> any</c><00:05:54.479><c> re</c>

00:06:03.189 --> 00:06:03.199 align:start position:0%
 
 

00:06:03.199 --> 00:06:07.469 align:start position:0%
 
you<00:06:03.520><c> have</c><00:06:03.720><c> to</c><00:06:04.080><c> quick</c><00:06:04.880><c> and</c><00:06:05.720><c> come</c><00:06:06.000><c> back</c><00:06:06.400><c> again</c>

00:06:07.469 --> 00:06:07.479 align:start position:0%
you have to quick and come back again
 

00:06:07.479 --> 00:06:10.270 align:start position:0%
you have to quick and come back again
at

00:06:10.270 --> 00:06:10.280 align:start position:0%
at
 

00:06:10.280 --> 00:06:13.670 align:start position:0%
at
okay<00:06:11.280><c> okay</c><00:06:11.599><c> if</c><00:06:11.880><c> there</c><00:06:12.000><c> are</c><00:06:12.199><c> no</c><00:06:12.400><c> more</c><00:06:12.680><c> questions</c>

00:06:13.670 --> 00:06:13.680 align:start position:0%
okay okay if there are no more questions
 

00:06:13.680 --> 00:06:18.230 align:start position:0%
okay okay if there are no more questions
just<00:06:14.000><c> thank</c><00:06:14.160><c> you</c><00:06:14.599><c> for</c><00:06:15.479><c> thank</c>

00:06:18.230 --> 00:06:18.240 align:start position:0%
 
 

00:06:18.240 --> 00:06:21.639 align:start position:0%
 
you<00:06:19.240><c> we</c><00:06:19.360><c> will</c>