Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
dmv.community is one of the many independent Mastodon servers you can use to participate in the fediverse.
A small regional Mastodon instance for those in the DC, Maryland, and Virginia areas. Local news, commentary, and conversation.

Administered by:

Server stats:

175
active users

dmv.community: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.4

#formalverification

1 post1 participant0 posts today
Jan :rust: :ferris:<p>Iris Project | A Higher-Order Concurrent Separation Logic Framework,<br>implemented and verified in the Rocq Prover</p><p><a href="https://iris-project.org/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">iris-project.org/</span><span class="invisible"></span></a></p><p><a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://floss.social/tags/Iris" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Iris</span></a> <a href="https://floss.social/tags/ConcurrentSeparationLogic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ConcurrentSeparationLogic</span></a> <a href="https://floss.social/tags/Proof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Proof</span></a></p>
José A. Alonso<p>Readings shared March 19, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/19-readings_shared_03-19-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/03/19-readings_shared_03-19-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CompSci</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Programaci%C3%B3nFuncional" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgramaciónFuncional</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a></p>
José A. Alonso<p>Can LLMs enable verification in mainstream programming? ~ Aleksandr Shefer et als. <a href="https://arxiv.org/abs/2503.14183" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2503.14183</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a></p>
LavX News<p>AI and the Future of Mathematical Proofs: A New Era of Collaboration and Innovation</p><p>As AI continues to evolve, the intersection of mathematics and machine learning is poised to revolutionize how proofs are generated and verified. With the advent of interactive theorem provers and adv...</p><p><a href="https://news.lavx.hu/article/ai-and-the-future-of-mathematical-proofs-a-new-era-of-collaboration-and-innovation" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">https://</span><span class="ellipsis">news.lavx.hu/article/ai-and-th</span><span class="invisible">e-future-of-mathematical-proofs-a-new-era-of-collaboration-and-innovation</span></a></p><p><a href="https://mastodon.cloud/tags/news" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>news</span></a> <a href="https://mastodon.cloud/tags/tech" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>tech</span></a> <a href="https://mastodon.cloud/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://mastodon.cloud/tags/InteractiveTheoremProvers" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>InteractiveTheoremProvers</span></a> <a href="https://mastodon.cloud/tags/AlphaProof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AlphaProof</span></a></p>
Rob Sison<p>There's now a video up of the talk I gave at this year's seL4 Summit, on the status of UNSW's projects to verify Time Protection and Microkit-based userland OS services for the seL4 microkernel:</p><p><a href="https://youtu.be/7wcFx6OTEL4" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/7wcFx6OTEL4</span><span class="invisible"></span></a></p><p><a href="https://aus.social/tags/sel4summit" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>sel4summit</span></a> <a href="https://aus.social/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a> <a href="https://aus.social/tags/verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>verification</span></a> <a href="https://aus.social/tags/operatingsystems" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>operatingsystems</span></a> <a href="https://aus.social/tags/microkernel" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>microkernel</span></a> <a href="https://aus.social/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://aus.social/tags/HOL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HOL4</span></a> <a href="https://aus.social/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://aus.social/tags/modelchecking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>modelchecking</span></a> <a href="https://aus.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://aus.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalverification</span></a> <a href="https://aus.social/tags/formal_methods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formal_methods</span></a> <a href="https://aus.social/tags/formal_verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formal_verification</span></a></p>
Kensan<p>New article up on ACM on Ada/SPARK title "Co-Developing Programs and Their Proof of Correctness". PDF is also available for download.</p><p><a href="https://cacm.acm.org/magazines/2024/3/280078-co-developing-programs-and-their-proof-of-correctness/fulltext" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">cacm.acm.org/magazines/2024/3/</span><span class="invisible">280078-co-developing-programs-and-their-proof-of-correctness/fulltext</span></a></p><p><a href="https://mastodon.social/tags/ada" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ada</span></a> <a href="https://mastodon.social/tags/spark" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>spark</span></a> <a href="https://mastodon.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalverification</span></a></p>
Steve Easterbrook<p>A fuller <a href="https://fediscience.org/tags/introduction" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>introduction</span></a>.</p><p>My PhD was in software systems analysis: how to handle poorly understood, conflicting system requirements (<a href="https://fediscience.org/tags/RequirementsEngineering" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>RequirementsEngineering</span></a>)</p><p>This led me to explore socio-cognitive processes of large teams (<a href="https://fediscience.org/tags/DistributedCognition" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DistributedCognition</span></a>, <a href="https://fediscience.org/tags/STS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>STS</span></a>, <a href="https://fediscience.org/tags/Ethnography" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Ethnography</span></a>)</p><p>I have worked for NASA studying software safety for spacecraft (<a href="https://fediscience.org/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a>, <a href="https://fediscience.org/tags/OrganizationalBehaviour" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>OrganizationalBehaviour</span></a>)</p><p>Now I study <a href="https://fediscience.org/tags/ClimateModels" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ClimateModels</span></a> + do <a href="https://fediscience.org/tags/ClimateData" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ClimateData</span></a> analytics, using all the above, plus <a href="https://fediscience.org/tags/SystemsThinking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SystemsThinking</span></a>, <a href="https://fediscience.org/tags/DataScience" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DataScience</span></a>, &amp; <a href="https://fediscience.org/tags/ML" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ML</span></a></p>
theruran 💻 🌐 :cereal_killer:<p>worth posting this again, for those programmers who are having wicked thoughts of writing security-critical software in C or C++</p><p>Source: "Exploitation in the era of <a href="https://hackers.town/tags/formalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalVerification</span></a>: A peek at a new frontier with <a href="https://hackers.town/tags/Ada" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Ada</span></a> / <a href="https://hackers.town/tags/SPARK" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SPARK</span></a>" by Adam Zabrocki and Alex Tereshkin, <a href="https://hackers.town/tags/DEFCON30" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DEFCON30</span></a>, 2022</p><p><a href="https://hackers.town/tags/infosec" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>infosec</span></a> <a href="https://hackers.town/tags/DEFCON" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DEFCON</span></a></p>
ExploreLive feeds
About