"LLM-Verifier systems get a boost with 4/$\delta$ Bound theorem! #FormalVerification #LLM #SoftwareVerification"

The introduction of Formal Verification tools with large language models (LLMs) has revolutionized software verification, but current methods lack reliability due to the absence of a solid theoretical foundation. This research addresses this gap by developing an LLM-Verifier Convergence...

#FormalVerification #LargeLanguageModels #LLM-VerifierSystems #SoftwareVerification

Third up: the experience report "Teaching Software Specification" by Cameron Moy and Daniel Patterson. This paper makes the provocative but very good point that (at least) some courses on software verification could actually benefit by teaching formal *specification* instead. I found section 7 (interviews with students who took two very different versions of their course) particularly interesting. I just might have to make some changes to my FP course based on this.

(Also I was glad to see the work of @sarantja on teaching theorem provers getting a mention here!)

dl.acm.org/doi/10.1145/3747533

#SoftwareVerification #SoftwareSpecification #Education

I cannot get enough of our shared Vulgar Technobabble that we #ComputerScientists speak. Even #ACM #TuringAward winning blokes speak this way.🤣

Interviewer—What is a good way to understand what #ModelChecking is and what it does?

#AllenEmerson—[staring intently at his toes] Well, uh, in "layman's terms", model checking is an algorithmic method of verifying correctness of nominally finite state systems, uh, against a specification that's typically given in temporal logic. Uh, if the model checker, the model checking tool that's been implemented, uh, returns "yes", then the system is correct. If it, uh, returns "no", the specification is violated, and a counterexample is produced.

Sure, we get it; it is but #SoftwareVerification in so many words. But does a "layman" get it?

https://youtu.be/sUwxA8px7O8?si=O4MVOVDT2rkIToNd

#VulgarLatin https://en.wikipedia.org/wiki/Vulgar_Latin

Emerson on the introduction of model checking for hardware and software verification.

YouTube

SwiftCraft 2024 TUTORIAL PREVIEW: Shifting (UI) Tests to the Far Left by Georgios Sotiropoulos

https://swiftcraft.uk/session/shifting-ui-tests-to-the-far-left

Register now at https://swiftcraft.uk/tickets

#UItests #specifications #softwareverification

Swift Craft

SwiftCraft 2024 TUTORIAL PREVIEW: Shifting (UI) Tests to the Far Left by Georgios Sotiropoulos

https://swiftcraft.uk/session/shifting-ui-tests-to-the-far-left

Register now at https://swiftcraft.uk/tickets

#UItests #specifications #softwareverification

Swift Craft

SwiftCraft 2024 TUTORIAL ANNOUNCEMENT: Shifting (UI) Tests to the Far Left by Georgios Sotiropoulos

https://swiftcraft.uk/session/shifting-ui-tests-to-the-far-left

Register now at https://swiftcraft.uk/tickets

#UItests #specifications #softwareverification

Swift Craft

Creating a new #introduction, since life changes. For 12 years I was a #SoftwareEngineer at Google, working predominantly on #EngineeringProductivity. Now I’m at smaller startup doing smaller-startup things. My Ph.D. is in #SoftwareVerification.

I stopped really posting on Twitter eight years before moving to Mastodon, so I’m a little rusty and tend to fall out of it from time to time.

I continue to forecast that my posts will soon be all #beagle, all the time.

@modulux Based on our conversation above, you might be interested in this:

https://takolang.dev/

An experimental programming language for ergonomic software verification

#ProgrammingLanguage #SoftwareVerification #Verification

Coming soon…

An experimental programming language for ergonomic software verification

tako

RT @[email protected]

Download this free book to learn about #SPARKAda, a programming language & toolsuite that brings mathmatics-based confidence to #softwareverification. The book presents SPARK Ada from a #MISRAC developer's perspective. #formalmethods #Adaprogramming
https://www.adacore.com/books/spark-ada-for-misra-c-developer

🐦🔗: https://twitter.com/AdaCoreCompany/status/1298598432748208128

SPARK Ada for the MISRA C Developer

Take a look at the SPARK subset of Ada and its supporting tools through an example-driven comparison with the rules in the widely known MISRA C subset.