31–40 of 43 posts
My team similarly used Z3 to reverse-generate data from SQL queries so that erroneous mutations of the queries get detected early on: http://www.cse.iitb.ac.in/infolab/xdata/
Earlier quoted context omitted.
Google's one step ahead of you there :) https://github.com/google/souper
Not exactly what I'm talking about. My scheme would really be a cheap way of getting some symbolic optimisations for free during the early days of a compiler, I don't think it's a realistic strategy for all compilation.
Lean 4 is a functional programming language and theorem prover that compiles to C. A lot of research went into making Lean 4 blazingly fast https://leanprover.github.io/publications/
Galois inc reproduced benchmarks by the Lean 4 devs that show that Lean 4 regularly outperforms the C++ stdlib.
This is an awesome mix of raw speed, functional programming, and formal software verification.
Earlier quoted context omitted.
Let me ask another question, how do we evaluate the accuracy of a model? Thank you for your time.
Evaluating the accuracy of a model is an unsolved problem with both formal and informal approaches. 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 t…
Earlier quoted context omitted.
Evaluating the accuracy of a model is an unsolved problem with both formal and informal approaches. 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 t…
Thank you. Is there any way to statistically evaluate a model? Something like testing a model.
The author of Z3, Leo de Moura, released Lean 4 milestone 1 about 3 weeks ago: https://github.com/leanprover/lean4 Lean 4 is a functional programming language and theorem prover that compiles to C. A lot of research went into making Lean 4 blazingly fast https://leanprover.github.io/publications/ Galois inc reproduced benchmarks by the Lean 4 devs that show that Lean 4 regularly outperforms the C++ stdlib. This is an…
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.
Z3 is intended as more of a backend for higher-level languages, like TLA+, to use in model checking. I would be surprised if anyone were writing specs in the input language directly.
- Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-lan...
- Coral: https://www.microsoft.com/en-us/research/project/q-program-v...
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…
It sounds nice for optimization in theory but in practice production compilers already have well oiled optimization pipelines that have mostly "flat" performance characteristics (i.e. all the low hanging fruit is gone), and the algorithms are all very well understood because most of the fundamentals really haven't changed in ~20 years or more. The 80/20 rule mostly still applies. TBF this isn't always true. Unison[1]…
I'm not sure that's true. Apparently some low-level optimisations are barely worth implementing if you're targeting a modern CPU.
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.
Z3 is intended as more of a backend for higher-level languages, like TLA+, to use in model checking. I would be surprised if anyone were writing specs in the input language directly.