My naive thoughts on Formal Verification (FV) and LLM:
We could leverage existing FV tools for a given programming language by using an LLM to generate a translator that maps the language to the FV tool's input format. This would essentially require a finite number of "abstract interpretation" functions—one for each language construct. While the total number of constructs might be large (e.g., around 500), each function would be independent. A function would only need to reason about the abstract semantics of a single construct, assuming the others adhere to their respective semantics. We could then distribute these LLM-generated functions among a group of experts (e.g., 100 reviewers). Thanks to the modularity of the functions, reviewers could evaluate their assigned subset in parallel without bottlenecks. The end result would be a working FV tool for the target language.
The usual sorts of fuzzing and static analyses, using AddressSanitizer and ThreadSanitizer. Also, with a bug bounty program to try to encourage external researchers to report issues. (I work on Firefox security; also I fixed 2 of the bugs linked in the blog post.)
How many of those are false positives though? Probably just over 5000?
You get bug bounties if you report the kind of bugs Mythos identified. There's a reason no-one collected bounties from the "5000 defects" Coverity identified.
The Mythos reports have several examples of chaining a whole bunch of logic in different parts of the program together to exploit something very subtle. The Coverity reports aren't anything like that. These tools aren't remotely in the same league or even universe.
It's hard to convince managers to spend money on static analysis tools (or any development tool).
Unless your company just got bad publicity for a bug and your devs come to you and demonstrate that a certain static analysis tool would have flagged that particular piece of code, most managers would let the beancounter-facet dominate the decision making process.
The best general purpose one, anyway. Specialty tools can be much better for their niches. Heck, compiler warnings are one such niche tool, and some of them are quite good.
Firefox developers do fix issues found by Coverity. I haven't looked at the results in over a decade, but the last time I did there were a few code patterns we used in a lot of places which Coverity didn't like (but were actually okay the way we were doing them) which resulted in a colossal number of false positives.
That's a good post but we don't even need this post to tell of her incredible power of smashing great things. I wish to see her in the next Shehulk movie.
There is no undebatably best consumer laptop for the simple reason that different users have different requirements and priorities.
And for some, things that Apple do are a no go. Like glued parts, limited Linux support, no OLED screens, no post buy upgradability, overpriced RAM upgrades, limited and finicky multimonitor support for most models.
So clearly it is debatable and depends on who you ask.
Yep, everyone has different requirements and things they'll put up with. Personally, the touchpad on my Dell laptop is absolutely terrible, but it's not hard to get a wireless (or wired) mouse and plug that in, so I can have a reasonably-priced laptop that works well with Linux.
> limited and finicky multimonitor support for most models.
I’ve never had an issue, and I regularly plug in one or two at a time. Even two that lie and say they are the same monitor with same serial and it still just works. Although, only after m1 and beyond.
How about I name a company that sold us a laptop that required 7 motherboard replacements, and after the 8th time it crapped out they told us it would cost $1200 to fix it from then on out. We signed up on a class action lawsuit along with tons of other people having the same exact dead motherboard problem, and we won.
Because the reason Apple really dislikes nvidia was because nvidia sort of lied about the thermal spec (much like intel does, except intel could downclock); and it caused a lot of GPUs to kill their motherboards: https://blog.greggant.com/posts/2021/10/13/apple-vs-nvidia-w...
We’ve had our share of Dell lemons, too. Bad batches and problematic models happen, that’s life. If we have to go back 10 years to find an example of widespread problem, it’s not that bad.
Obviously, openAI is a cheaper and better option for Apple to use AI in their devices for the time being. Once they have their own AI, or the AI hype subsides, they'll kick openAI.
We could leverage existing FV tools for a given programming language by using an LLM to generate a translator that maps the language to the FV tool's input format. This would essentially require a finite number of "abstract interpretation" functions—one for each language construct. While the total number of constructs might be large (e.g., around 500), each function would be independent. A function would only need to reason about the abstract semantics of a single construct, assuming the others adhere to their respective semantics. We could then distribute these LLM-generated functions among a group of experts (e.g., 100 reviewers). Thanks to the modularity of the functions, reviewers could evaluate their assigned subset in parallel without bottlenecks. The end result would be a working FV tool for the target language.