Mastodon

SELab@HVLVideos from the RV’22 Conference on Runtime VerificationI was still sitting on a batch of video-recordings from Runtime Verification 2022 that Thao Dang and myself were running in a then slightly more peaceful Georgia.Most of the authors got the open links to the videos in our CMS at HVL, but I never got around to “officially” posting them somewhere. They are now also available on the conference web-site.<a href="https://selabhvl.github.io/science/2025/03/30/rv22-videos.html" rel="nofollow noopener" translate="no" target="_blank">https://selabhvl.github.io/science/2025/03/30/rv22-videos.html</a>^ <a href="https://mastodon.social/@fm_volker" class="u-url mention" rel="nofollow noopener" target="_blank">@fm_volker</a> <a href="https://fediscience.org/tags/runtimeVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#runtimeVerification</a> <a href="https://fediscience.org/tags/rv22" class="mention hashtag" rel="nofollow noopener" target="_blank">#rv22</a> <a href="https://fediscience.org/tags/formalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalMethods</a>

Cass AlexandruThe other thing that I really enjoyed in my industry job is to really think that, hey, the skills that we have as PL people and as formal methods, functional programming, these sorts of things, they are relevant. It’s like people say that when you get into industry, these things are not important. And I think that’s a total misconception. It’s a total lie because, of course, if you don’t know what you can do with a nice systematic approach, of course, you don’t end up doing it, and everything becomes just another hack. - <a href="https://haskell.foundation/podcast/63/" rel="nofollow noopener" target="_blank">Farhad Mehta – the Haskell Interlude Podcast</a> <a href="https://types.pl/tags/haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#haskell</a> <a href="https://types.pl/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://types.pl/tags/formalmethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalmethods</a>

Compsci WeeklyCoding isn't programming<a href="https://www.socallinuxexpo.org/scale/22x/presentations/closing-keynote-leslie-lamport" target="_blank" rel="nofollow noopener" translate="no">https://www.socallinuxexpo.org/scale/22x/presentations/closing-keynote-leslie-lamport</a>Discussions: <a href="https://discu.eu/q/https://www.socallinuxexpo.org/scale/22x/presentations/closing-keynote-leslie-lamport" target="_blank" rel="nofollow noopener" translate="no">https://discu.eu/q/https://www.socallinuxexpo.org/scale/22x/presentations/closing-keynote-leslie-lamport</a><a href="https://mastodon.social/tags/compsci" class="mention hashtag" rel="tag">#compsci</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/practices" class="mention hashtag" rel="tag">#practices</a> <a href="https://mastodon.social/tags/programming" class="mention hashtag" rel="tag">#programming</a>

LobstersSeL4 Summit 2024 Playlist <a href="https://lobste.rs/s/6omn3o" target="_blank" rel="nofollow noopener" translate="no">https://lobste.rs/s/6omn3o</a> <a href="https://mastodon.social/tags/video" class="mention hashtag" rel="tag">#video</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/security" class="mention hashtag" rel="tag">#security</a> <a href="http://www.youtube.com/playlist?list=PLtoQeavghzr0ZntMmRPwg1VA1yJd_T3y9" target="_blank" rel="nofollow noopener" translate="no">http://www.youtube.com/playlist?list=PLtoQeavghzr0ZntMmRPwg1VA1yJd_T3y9</a>

LobstersClosing Keynote with Leslie Lamport at SCALE 22x: Coding isn't programming <a href="https://lobste.rs/s/zz69lm" target="_blank" rel="nofollow noopener" translate="no">https://lobste.rs/s/zz69lm</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/practices" class="mention hashtag" rel="tag">#practices</a> <a href="https://www.socallinuxexpo.org/scale/22x/presentations/closing-keynote-leslie-lamport" target="_blank" rel="nofollow noopener" translate="no">https://www.socallinuxexpo.org/scale/22x/presentations/closing-keynote-leslie-lamport</a>

LobstersPeanoScript: TypeScript but it's a theorem prover <a href="https://lobste.rs/s/qnndyo" target="_blank" rel="nofollow noopener" translate="no">https://lobste.rs/s/qnndyo</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/javascript" class="mention hashtag" rel="tag">#javascript</a> <a href="https://peanoscript.mjgrzymek.com/tutorial" target="_blank" rel="nofollow noopener" translate="no">https://peanoscript.mjgrzymek.com/tutorial</a>

LobstersIntroducing GREASE: An Open-Source Tool for Uncovering Hidden Vulnerabilities in Binary Code <a href="https://lobste.rs/s/qykkq8" target="_blank" rel="nofollow noopener" translate="no">https://lobste.rs/s/qykkq8</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/release" class="mention hashtag" rel="tag">#release</a> <a href="https://mastodon.social/tags/reversing" class="mention hashtag" rel="tag">#reversing</a> <a href="https://mastodon.social/tags/security" class="mention hashtag" rel="tag">#security</a> <a href="https://www.galois.com/articles/introducing-grease" target="_blank" rel="nofollow noopener" translate="no">https://www.galois.com/articles/introducing-grease</a>

Andrzej Wąsowski ☑️ 🟥<a href="https://mastodon.world/@SuneAuken" class="u-url mention" rel="nofollow noopener" target="_blank">@SuneAuken</a>, <a href="https://mastodon.social/@UlrikNyman" class="u-url mention" rel="nofollow noopener" target="_blank">@UlrikNyman</a> bio:Head of Studies, Deputy Head of Department at Computer Science, Aalborg University <a href="http://ulrik.blog.aau.dk" rel="nofollow noopener" translate="no" target="_blank">http://ulrik.blog.aau.dk</a> Associate Professor, PhD.<a href="https://social.itu.dk/tags/compsci" class="mention hashtag" rel="nofollow noopener" target="_blank">#compsci</a> <a href="https://social.itu.dk/tags/formalmethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalmethods</a>

LobstersProof Assistants At the Hardware-Software Interface (2020) <a href="https://lobste.rs/s/kzqk9g" target="_blank" rel="nofollow noopener" translate="no">https://lobste.rs/s/kzqk9g</a> <a href="https://mastodon.social/tags/video" class="mention hashtag" rel="tag">#video</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/hardware" class="mention hashtag" rel="tag">#hardware</a> <a href="https://www.youtube.com/watch?v=GXXOyXeyKeY" target="_blank" rel="nofollow noopener" translate="no">https://www.youtube.com/watch?v=GXXOyXeyKeY</a>

screwlisp<a href="https://mastodon.sdf.org/tags/formalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalMethods</a> <a href="https://mastodon.sdf.org/tags/gamedev" class="mention hashtag" rel="nofollow noopener" target="_blank">#gamedev</a> <a href="https://mastodon.sdf.org/tags/programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#programming</a> <a href="https://mastodon.sdf.org/tags/commonLisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#commonLisp</a> <a href="https://mastodon.sdf.org/tags/acl2" class="mention hashtag" rel="nofollow noopener" target="_blank">#acl2</a> <a href="https://mastodon.sdf.org/tags/itch" class="mention hashtag" rel="nofollow noopener" target="_blank">#itch</a> <a href="https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic" rel="nofollow noopener" target="_blank">https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic</a>Since yesterday I advocated strong use of defgeneric, defmethod and McCLIM's define-command, here I present just giving lisp's defun to acl2's first order <a href="https://mastodon.sdf.org/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#logic</a>.I present a batch processing style for using acl2 both in <a href="https://mastodon.sdf.org/tags/shell" class="mention hashtag" rel="nofollow noopener" target="_blank">#shell</a> and in <a href="https://mastodon.sdf.org/tags/lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#lisp</a> with a worked example.Thoughts and opinions, gamedevs and logical types?

Compsci Weeklycoq-of-rust: Formal verification tool for Rust<a href="https://github.com/formal-land/coq-of-rust" target="_blank" rel="nofollow noopener" translate="no">https://github.com/formal-land/coq-of-rust</a>Discussions: <a href="https://discu.eu/q/https://github.com/formal-land/coq-of-rust" target="_blank" rel="nofollow noopener" translate="no">https://discu.eu/q/https://github.com/formal-land/coq-of-rust</a><a href="https://mastodon.social/tags/compsci" class="mention hashtag" rel="tag">#compsci</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/programming" class="mention hashtag" rel="tag">#programming</a> <a href="https://mastodon.social/tags/rustlang" class="mention hashtag" rel="tag">#rustlang</a>

Lobsterscoq-of-rust: Formal verification tool for Rust <a href="https://lobste.rs/s/lomwgf" target="_blank" rel="nofollow noopener" translate="no">https://lobste.rs/s/lomwgf</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/rust" class="mention hashtag" rel="tag">#rust</a> <a href="https://github.com/formal-land/coq-of-rust" target="_blank" rel="nofollow noopener" translate="no">https://github.com/formal-land/coq-of-rust</a>

LobstersTypestate Programming <a href="https://lobste.rs/s/lkdgd4" target="_blank" rel="nofollow noopener" translate="no">https://lobste.rs/s/lkdgd4</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/hardware" class="mention hashtag" rel="tag">#hardware</a> <a href="https://mastodon.social/tags/plt" class="mention hashtag" rel="tag">#plt</a> <a href="https://mastodon.social/tags/rust" class="mention hashtag" rel="tag">#rust</a> <a href="https://docs.rust-embedded.org/book/static-guarantees/typestate-programming.html" target="_blank" rel="nofollow noopener" translate="no">https://docs.rust-embedded.org/book/static-guarantees/typestate-programming.html</a>

Lobstersowi: Cross-language Bugfinder <a href="https://lobste.rs/s/qsmfvf" target="_blank" rel="nofollow noopener" translate="no">https://lobste.rs/s/qsmfvf</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/ml" class="mention hashtag" rel="tag">#ml</a> <a href="https://github.com/OCamlPro/owi" target="_blank" rel="nofollow noopener" translate="no">https://github.com/OCamlPro/owi</a>

Functional SCJoin us TUE Mar 11th for "LEAN - Interactive LLMs" hosted by <a href="https://mathstodon.xyz/@jaredc" class="u-url mention" rel="nofollow noopener" target="_blank">@jaredc</a> First we'll explore using LLMs for proofs in Lean. Then, we'll work together to tackle math theorems together. Don’t miss this hands-on session!<a href="https://functional.cafe/tags/lean" class="mention hashtag" rel="nofollow noopener" target="_blank">#lean</a> <a href="https://functional.cafe/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://functional.cafe/tags/formalmethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalmethods</a> <a href="https://functional.cafe/@leanprover" class="u-url mention" rel="nofollow noopener" target="_blank">@leanprover</a> <a href="https://functional.cafe/tags/chstech" class="mention hashtag" rel="nofollow noopener" target="_blank">#chstech</a> <a href="https://www.charlestonlc.org/classes/charleston-lean-proof-assistant-meetup/" rel="nofollow noopener" translate="no" target="_blank">https://www.charlestonlc.org/classes/charleston-lean-proof-assistant-meetup/</a>

Formal Methods EuropeThe invited talks from <a href="https://mastodon.acm.org/tags/FMAS2024" class="mention hashtag" rel="nofollow noopener" target="_blank">#FMAS2024</a> are captured on our YouTube channel: <a href="https://buff.ly/3QFxNhE" rel="nofollow noopener" translate="no" target="_blank">https://buff.ly/3QFxNhE</a> You can (re)watch "Proof for Industrial Systems using Neural Certificates" by Daniel Kröning (joint with <a href="https://mastodon.acm.org/tags/iFM2024" class="mention hashtag" rel="nofollow noopener" target="_blank">#iFM2024</a>) and "Self-Adaptation in Autonomous Systems" by Lizeth Tarifa <a href="https://mastodon.acm.org/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalMethods</a> <a href="https://mastodon.acm.org/@FMASWorkshop" class="u-url mention" rel="nofollow noopener" target="_blank">@FMASWorkshop</a>

Formal Methods EuropeCan't remeber something important from the <a href="https://mastodon.acm.org/tags/FM2023" class="mention hashtag" rel="nofollow noopener" target="_blank">#FM2023</a> invited talks?Yes you can.Watch them again on our YouTube channel: <a href="https://buff.ly/41khRXh" rel="nofollow noopener" translate="no" target="_blank">https://buff.ly/41khRXh</a> We collect the invited talks for FM, FormaliSE, and many other <a href="https://mastodon.acm.org/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalMethods</a> events

LobstersSystems Correctness Practices at AWS: Leveraging Formal and Semi-formal Methods via <a href="https://discuss.systems/@ahelwer" class="u-url mention">@ahelwer</a> <a href="https://lobste.rs/s/pjbdph" target="_blank" rel="nofollow noopener" translate="no">https://lobste.rs/s/pjbdph</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://dl.acm.org/doi/10.1145/3712057" target="_blank" rel="nofollow noopener" translate="no">https://dl.acm.org/doi/10.1145/3712057</a>

Andrew HelwerReading the new experience report paper "System Correctness Practices at AWS" by <a href="https://fediscience.org/@marcbrooker" class="u-url mention" rel="nofollow noopener" target="_blank">@marcbrooker</a> & Ankush Desai, a successor to 2015 paper "How Amazon Web Services Uses Formal Methods". Documents a whole buffet of industrial formal methods use: P (including new tool PObserve for runtime trace validation), deterministic simulation testing in Rust with the open-sourced Shuttle and Turmoil tools, Dafny, HOL Light, and the open-sourced Kani model-checker for Rust.While TLA⁺ was the most prominent featured tool in the 2015 paper, it's been lost in the crowd here as part of a clear shift toward verifying & testing the actual running code. I think TLA⁺ must carve out a niche for itself in a world where deterministic simulation testing becomes a commodity technology, or it risks losing relevance same as other design-level tools like UML. There are existing case studies on using TLA⁺ for trace validation and model-driven testing, but a lot of effort needs to go into tooling for making such integrations as smooth as possible instead of bespoke one-off projects.<a href="https://dl.acm.org/doi/10.1145/3712057" rel="nofollow noopener" translate="no" target="_blank">https://dl.acm.org/doi/10.1145/3712057</a><a href="https://discuss.systems/tags/TLAplus" class="mention hashtag" rel="nofollow noopener" target="_blank">#TLAplus</a> <a href="https://discuss.systems/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalMethods</a>

LobstersLean 4, release v4.17.0 <a href="https://lobste.rs/s/cbytov" target="_blank" rel="nofollow noopener" translate="no">https://lobste.rs/s/cbytov</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="tag">#formalmethods</a> <a href="https://mastodon.social/tags/release" class="mention hashtag" rel="tag">#release</a> <a href="https://github.com/leanprover/lean4/releases/tag/v4.17.0" target="_blank" rel="nofollow noopener" translate="no">https://github.com/leanprover/lean4/releases/tag/v4.17.0</a>

Recent searches

Search options

Administered by:

Server stats:

#formalmethods