TechHub

LobstersAdvent of Code in Coq (2021) <a href="https://lobste.rs/s/jghuoa" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/jghuoa</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://github.com/Lysxia/advent-of-coq-2021" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/Lysxia/advent-of-coq-2021</a>

Hacker NewsSystems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods<a href="https://queue.acm.org/detail.cfm?id=3712057" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://queue.acm.org/detail.cfm?id=3712057</a><a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#HackerNews</a> <a href="https://mastodon.social/tags/SystemsCorrectness" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SystemsCorrectness</a> <a href="https://mastodon.social/tags/AWS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AWS</a> <a href="https://mastodon.social/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalMethods</a> <a href="https://mastodon.social/tags/SoftwareEngineering" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SoftwareEngineering</a> <a href="https://mastodon.social/tags/TechTrends" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TechTrends</a> <a href="https://mastodon.social/tags/CloudComputing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CloudComputing</a>

Lobsters3110 Coq Tactics Cheatsheet <a href="https://lobste.rs/s/sjnbsz" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/sjnbsz</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html</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 noreferrer" target="_blank">Farhad Mehta – the Haskell Interlude Podcast</a> <a href="https://types.pl/tags/haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#haskell</a> <a href="https://types.pl/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FunctionalProgramming</a> <a href="https://types.pl/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a>

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

LobstersSeL4 Summit 2024 Playlist <a href="https://lobste.rs/s/6omn3o" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/6omn3o</a> <a href="https://mastodon.social/tags/video" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#video</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/security" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#security</a> <a href="http://www.youtube.com/playlist?list=PLtoQeavghzr0ZntMmRPwg1VA1yJd_T3y9" rel="nofollow noopener noreferrer" translate="no" target="_blank">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" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/zz69lm</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/practices" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#practices</a> <a href="https://www.socallinuxexpo.org/scale/22x/presentations/closing-keynote-leslie-lamport" rel="nofollow noopener noreferrer" translate="no" target="_blank">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" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/qnndyo</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/javascript" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#javascript</a> <a href="https://peanoscript.mjgrzymek.com/tutorial" rel="nofollow noopener noreferrer" translate="no" target="_blank">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" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/qykkq8</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/release" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#release</a> <a href="https://mastodon.social/tags/reversing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#reversing</a> <a href="https://mastodon.social/tags/security" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#security</a> <a href="https://www.galois.com/articles/introducing-grease" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.galois.com/articles/introducing-grease</a>

Andrzej Wąsowski ☑️ 🟥<a href="https://mastodon.world/@SuneAuken" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@SuneAuken</a>, <a href="https://mastodon.social/@UlrikNyman" class="u-url mention" rel="nofollow noopener noreferrer" 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 noreferrer" 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 noreferrer" target="_blank">#compsci</a> <a href="https://social.itu.dk/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a>

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

screwlisp<a href="https://mastodon.sdf.org/tags/formalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalMethods</a> <a href="https://mastodon.sdf.org/tags/gamedev" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#gamedev</a> <a href="https://mastodon.sdf.org/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programming</a> <a href="https://mastodon.sdf.org/tags/commonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#commonLisp</a> <a href="https://mastodon.sdf.org/tags/acl2" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#acl2</a> <a href="https://mastodon.sdf.org/tags/itch" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#itch</a> <a href="https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic" rel="nofollow noopener noreferrer" 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 noreferrer" 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 noreferrer" target="_blank">#shell</a> and in <a href="https://mastodon.sdf.org/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" 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" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/formal-land/coq-of-rust</a>Discussions: <a href="https://discu.eu/q/https://github.com/formal-land/coq-of-rust" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://discu.eu/q/https://github.com/formal-land/coq-of-rust</a><a href="https://mastodon.social/tags/compsci" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#compsci</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programming</a> <a href="https://mastodon.social/tags/rustlang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#rustlang</a>

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

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

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

Formal Methods EuropeThe invited talks from <a href="https://mastodon.acm.org/tags/FMAS2024" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FMAS2024</a> are captured on our YouTube channel: <a href="https://buff.ly/3QFxNhE" rel="nofollow noopener noreferrer" 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 noreferrer" 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 noreferrer" target="_blank">#FormalMethods</a> <a href="https://mastodon.acm.org/@FMASWorkshop" class="u-url mention" rel="nofollow noopener noreferrer" 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 noreferrer" 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 noreferrer" 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 noreferrer" 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" rel="nofollow noopener noreferrer" target="_blank">@ahelwer</a> <a href="https://lobste.rs/s/pjbdph" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/pjbdph</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://dl.acm.org/doi/10.1145/3712057" rel="nofollow noopener noreferrer" translate="no" target="_blank">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 noreferrer" 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 noreferrer" 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 noreferrer" target="_blank">#TLAplus</a> <a href="https://discuss.systems/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalMethods</a>

Recent searches

Search options

Administered by:

Server stats:

#formalmethods