SMT Solvers in Software Security (2012)(usenix.org) |
SMT Solvers in Software Security (2012)(usenix.org) |
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.
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...