SMT Solvers in Software Security (2012)
usenix.orgIf for verification, I'll add this trifecta some of us independently arrived at:
1. Formal specs drive spec/property-based testing for quick verification.
2. If that passes, try to get automated proof with the solver.
3. Use formal specs as runtime checks or traces that get checked with the input being from fuzzers or other test generatore. Failures take you right to the property that failed.
4. Optionally, leave runtime check in for any specification property that is unproven or lacking resources to prove.
Also, static analyzers that quickly catch certain kinds of problems. If available, I'd run them in parallel to the property-based testing before the proof attempt. All this together keeps time/effort minimized with productivity on verified code maximized.
I found it funny that your "trifecta" has four clauses :)
So I looked up the meaning of the word to make sure I knew what it means- and, it turns out, it has nothing to do with a Roman Triumvirate (as I had somehow convinced myself it did).
It turns out it comes from betting on the horses. It means a kind of bet where you put your money on which three horses will come first, second and third in the race- in the exact order you bet on.
Apparently, the word itself is a kind of fragmented portmanteau, from "tri-" and the syllable "fecta" in "perfecta", from the American Spanish for a perfect bet: "quiniela perfecta". This post has got the works: [2].
... and I still haven't read the article I navigated here to read :)
_______________
[1] https://en.wikipedia.org/wiki/Trifecta
[2] https://www.dailywritingtips.com/trifecta-not-always-appropr...
Oh yeah, I editted in the fourth one after I wrote that. Glad you got some fun out of it. :)
We’ve been using Certora for smart contract code verification. For me, it’s really amazing to see effective code verification can be (on small and important code routines). Over time, I expect code verification to overtake unit testing for core (pure) code modules.
Aside: Should have a 2012 in the title. I recognized Julien’s work because he came to Bloomberg almost immediately after this :)