Tux Machines
Posted by Roy Schestowitz on Apr 18, 2023
=> Security: Reproducible Builds, FUD, and more | Red Hat Leftovers
=> ↺ Breaking the limits of TLA+ model checking
I haven’t written much about TLA+ on the blog since the new learntla went up. Any examples or special topics I think of go there instead. But I recently thought of a cool demo that doesn’t quite fit the theme of that book: there are some things you can’t easily check with the model checker but can check if you work with the state space as a directed graph.
Hi everyone,
I wrote a new blog post, Breaking the Limits of TLA+ Model Checking. It’s the first (non-learntla) TLA+-related content I’ve put out in what, almost two years? It also comes with a GitHub project with all the software artifacts: the spec, the graphing software, the scripts, etc. It’s about how to test the things that TLA+ can’t natively check, like hyperproperties and probabilistic properties.
=> ↺ Breaking the Limits of TLA+ Model Checking | ↺ GitHub project
So what do I mean by “things that TLA+ can’t check?” I spent ten minutes writing and rewriting two paragraphs carefully defining the differences between the language and the model checker before giving up and saying “this is a newsletter, nobody wants to read this.” So here’s the oversimplification. In TLA+ we have a spec that has multiple behaviors, or traces. Properties in TLA+ are things that are true for every behavior. Some such properties: [...]
=> ↺ Breaking the Limits of TLA+ Model Checking | ↺ GitHub project
=> ↺ Frederik Braun: Examine Firefox Inter-Process Communication using JavaScript in 2023
This is my update to the 2021 JavaScript IPC blog post from the Firefox Attack & Defense blog.
=> ↺ blog post
=> ↺ blog post
=> ↺ Support.Mozilla.Org: What’s up with SUMO – Q1 2023
Hi everybody,
I know some of you have been asking about the monthly blog post since January. We’re back today, with a summary of what happened in the past 3 months. This will be our new cadence for this kind of post. So please look out for our next edition by early July.
I hope the past 3 months have treated you well. Time surely flies so fast. We’ve done a lot of internal research for the past 3 months, but in Q2, I promise you will see more of me all around our various community channels.
If you're a programming student, you can win a free ticket to TPRC in Toronto (11-13 July) by taking part in the contest! Meanwhile, a preliminary schedule is available! Anton's Corner Anton Antonov has been busy again this week: a new module (WWW::MermaidInk) and an associated blog post with an introduction and examples!
=> gemini.tuxmachines.org This content has been proxied by September (ba2dc).Proxy Information
text/gemini;lang=en-GB