verification practitioner: undecidable is fast, decidable is slow
-
-
-
Yeah, I'm being somewhat glib, but sometimes restriction to decidable theories makes it harder to add domain-specific reasoning. Domain knowledge can often be most easily described in expressive logics, and significantly speed up reasoning.
- Još 3 druga odgovora
Novi razgovor -
-
-
I once saw a FM paper that said "the complexity of our algorithm is merely exponential". It was when I was just starting out, so it gave me a good orientation of what I'm getting into.
-
Can you imagine my shock when I accidentally attended a talk about designing fast memory allocators, and the speaker said: "Obviously we can't use integer *division*, it's too slow"

- Još 8 drugih odgovora
Novi razgovor -
-
-
systems researcher: fast is fast, slow is slow
-
Oh I thought it's: slow is slow, fast is also slow
- Još 1 odgovor
Novi razgovor -
-
-
When dealing with real-time temporal logic verification, sometimes I even thought: decidable is fast, semidecidable is still OK, I'll start to worry when I hit \Sigma_1^1
-
Totally true in synthesis too. No alternating quantifiers, no problem
Kraj razgovora
Novi razgovor -
-
-
In verification don't you say things like O(n^2) SAT calls is fast
-
I suppose we do say "the size of this SMT encoding is quadratic in the size of the problem". But then we say: "Hey, but there's no alternating quantifiers, it's gonna FLY!"
Kraj razgovora
Novi razgovor -
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.