-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
2351551
commit 19670f4
Showing
1 changed file
with
59 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,59 @@ | ||
| +++ | ||
| title = "2025 - TLA+ Community Event" | ||
| weight = 65 | ||
| +++ | ||
|
|
||
| <div align="right"> | ||
| <h4> | ||
|
|
||
| TLA<sup>+</sup> Community Event 2025<br> | ||
| Sunday, May 4, 2025<br> | ||
| Hamilton, Canada<br> | ||
| </h4> | ||
| </div> | ||
|
|
||
| # TLA+ Community Event 2025 | ||
|
|
||
|
|
||
|
|
||
| ### Co-located with [ETAPS 2025](https://etaps.org/2025/) in Hamilton, Ontario (Canada), on May 4, 2025. | ||
|
|
||
| [TLA+](https://lamport.azurewebsites.net/tla/tla.html) is a language that | ||
| is used in academia and industry for formally specifying systems. It is | ||
| supported by [verification tools](https://lamport.azurewebsites.net/tla/tools.html), including the TLC and Apalache model checkers and the TLAPS proof system. | ||
| PlusCal serves as a frontend for generating TLA+ specifications from an | ||
| algorithmic language with an imperative flavor. | ||
|
|
||
| The TLA+ Community Event serves as a forum where practitioners and | ||
| researchers interested in the use and further development of the | ||
| TLA+ specification language and its tools meet and discuss. | ||
|
|
||
| Proposals for contributed talks are sollicited that present work of | ||
| interest to users of TLA+ or PlusCal, such as: | ||
|
|
||
| * industrial or academic case studies, | ||
| * new tools for TLA+ or add-ons to existing tools, | ||
| * innovative use of existing tools or reports on their shortcomings, | ||
| * use of TLA+ in education. | ||
|
|
||
| Proposals for presentations, with a short (2 page) abstract summarizing | ||
| the content, should be sent to [[email protected]](mailto:[email protected]) | ||
| by February 7, 2025. Please indicate if you want to give a short or long | ||
| presentation (25 or 40 minutes, including discussion). Notification will | ||
| be given by February 17, 2025. | ||
|
|
||
| There will not be formal proceedings, but the abstracts and presentations | ||
| will be made available on the Web. | ||
|
|
||
| Participants will be required to | ||
| register | ||
| to ETAPS 2025. | ||
|
|
||
| ### Organizers | ||
| * Igor Konnov, researcher in security and formal methods and TU Wien | ||
| * Markus Kuppe, Microsoft | ||
| * [Stephan Merz](https://members.loria.fr/SMerz/), Inria Nancy | ||
|
|
||
| ### Program committee | ||
|
|
||
| TBA |