11–20 of 43 posts
Is there any introductory course for these kind of stuff?
The most useful and accessible symbolic execution package I’ve found so far is KLEE https://klee.github.io/
If anyone else has recommendations for tools or beginner material I’m all ears!
I'm not sure exactly what data structures LLVM uses to track knowledge about the program it's optimising, but with SMT you can ask the solver very non-trivial questions about the code and either eliminate subtle dead code or generate exploitable invariants (for "free")
Earlier quoted context omitted.
That's not a dumb question! The accuracy of one's underlying models is an outstanding problem in verification.
Let me ask another question, how do we evaluate the accuracy of a model? Thank you for your time.
Formally: we could ask multiple separate model/proof assistants to generate separate models from the same underlying specification, and then attempt to find discrepancies between their predicted results. This really just punts the responsibility: now we're relying on the accuracy of the abstract specification, rather than the model(s) automatically or manually produced from it. It's also not sound; it just allows us to feel more confident.
Informally: we can have a lot of different people look at the model very closely, and produce test vectors for the model based on human predictions of behavior.
This may be a dumb question, but how do I know that the model is accurate?
Is there any introductory course for these kind of stuff?
https://rise4fun.com/ for all sorts of examples of what these sorts of algorithms can solve.
https://www.coursera.org/learn/discrete-optimization is a good introduction to constraint optimization, local search, linear programming, and mixed integer programming.
It has a pretty large cost for small amounts of work, but Z3 seems like a good dependency for an optimizing compiler - asking it to do nothing from C++ seems to cost about 4ms, which isn't cheap but you can batch these things. I'm not sure exactly what data structures LLVM uses to track knowledge about the program it's optimising, but with SMT you can ask the solver very non-trivial questions about the code and eithe…
This may be a dumb question, but how do I know that the model is accurate?
Is it possible to check at runtime that the model is accurate?
Do you have a sensible thing to do if the model isn't accurate (e.g., fallback into "failsafe" mode, let an on-call engineer know that an assumption was violated, etc.)?
If yes & yes, well, there's your answer :)
It has a pretty large cost for small amounts of work, but Z3 seems like a good dependency for an optimizing compiler - asking it to do nothing from C++ seems to cost about 4ms, which isn't cheap but you can batch these things. I'm not sure exactly what data structures LLVM uses to track knowledge about the program it's optimising, but with SMT you can ask the solver very non-trivial questions about the code and eithe…
Google's one step ahead of you there :) https://github.com/google/souper
First time I see Z3 in the wild. Bonus points for the CLI friendly model checker, but lisp syntax... is less legible than TLA+ imho. Gotta give it a try someday to see for myself if the experience of creating the spec is better.
Is there any introductory course for these kind of stuff?
I’m just starting to investigate using formal analysis in practice and I think a much more practical topic is the symbolic execution frameworks which can analyze programs and feed them to theorem solvers like Z3. The most useful and accessible symbolic execution package I’ve found so far is KLEE https://klee.github.io/ If anyone else has recommendations for tools or beginner material I’m all ears!
Nielson & Nielson have the standard textbook in static program analysis that is used everywhere. But it's quite unfriendly as it's written using abstract algebra. They've recently released two textbooks that are much gentler. Actually, I'd say they are easy going and fun but still retain all the mathematical rigor.
They use program graphs, which are a bit less general but a lot easier to digest. They cover all major techniques, including theorem proving, static analysis, model checking, abstract interpretation, type and effect systems, etc:
- Formal Methods: An Appetizer https://www.springer.com/gp/book/9783030051556
- Program Analysis: An Appetizer https://arxiv.org/abs/2012.10086
There's also a companion website with some F# code. The second book, which seems still unfinished discusses how to implement program analyses using datalog. This speeds up development quite a lot. Otherwise, developing your own static analyzer is a lot of work.
My dream is to implement some kind of framework that enables quick DSL creation along with lightweight formal methods support to verify programs written in each DSL. I think restricted semantics is the key to make formal methods practical. Quoting Alan Perlis, "Beware of the Turing tar-pit in which everything is possible but nothing of interest is easy."