-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathnews.html
108 lines (73 loc) · 2.9 KB
/
news.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
<!DOCTYPE html>
<HTML>
<!-- Mirrored from lamport.azurewebsites.net/tla/news.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:31:22 GMT -->
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<META NAME="GENERATOR" CONTENT="Mozilla/4.05 [en] (X11; I; OSF1 V4.0 alpha)
[Netscape]">
<!--
%&b&<b>#</b>&
%&c& <b>#</b> &
-->
<!-- The following loads the style sheet for the html files of
the tla web site -->
<link rel="stylesheet" type="text/css" href="tlaweb.css">
<script src="tlaweb.js"> </script>
<SCRIPT>
noLinkName = "News" ;
</SCRIPT>
</HEAD>
<BODY onload="initialize()">
<title>News</title>
<table id="main">
<tr>
<td id="main_leftcolumn" >
</td>
<td id="main_contentcolumn">
<table>
<tr >
<td style="vertical-alight:top">
<div id = "showleftcol" > </div>
<H1>News</H1>
<p style="margin-top:-8px; margin-bottom:-18px">
Leslie Lamport<p>
<font size=-1><I> Last modified on 23 August 2019</I></font>
</td>
<td style="vertical-alight:top;width:auto">
</td>
</tr>
</table>
<HR style="margin-bottom:-5px;margin-top:-11px">
<P style="margin-top:0px"> </P>
<h2>Videos of Paxos Lectures</h2>
Videos of two lectures describing the Paxos consensus algorithm
with TLA+ are available <a href="paxos-algorithm2ea2.html?back-link=news.html">here</a>.
In addition to explaining the algorithm, they provide a crash
course on TLA+.
<h2>TLA+ Conference at Strange Loop 2019</h2>
The conference will take place in St. Louis, Missouri, USA, on 15 September
2019.
See <a href="https://conf.tlapl.us/home/">
<!-- href="https://groups.google.com/forum/#!topic/tlaplus/89x3LCVCCBI"-->
this announcement</a>.
<h2><a>Checking Inductive Invariance with TLC</a></h2>
If you've written rigorous correctness proofs of concurrent algorithms
described in TLA+, then you know that the key to the proof is an
inductive invariant. Finding the right inductive invariant is
hard. It should be made easier by new features added to TLC for
checking that a formula is an inductive invariant. What an
inductive invariant is and how to use TLC to check if a formula is one
are described in <a href="inductive-invariant.pdf">this document</a>.
<h2>2018 TLA+ Community Meeting</h2>
A TLA+ community meeting was held in Oxford, England on 18 July 2018.
The program, containing links to papers or extended abstracts and slides
for the talks, can be found
<a href="http://tla2018.loria.fr/program.html">here</a>.
Videos of the talks are available
<a href="https://www.youtube.com/watch?v=ifFfxRCX_jw&list=PLWLcqZLzY8u_3mDg2cHmduA5wl4J6hNX2">here</a>.
</td>
</tr>
</table>
</BODY>
<!-- Mirrored from lamport.azurewebsites.net/tla/news.html by HTTrack Website Copier/3.x [XR&CO'2014], Thu, 26 Mar 2020 22:31:24 GMT -->
</HTML>