SMT solvers write the weirdest programs. Wanna Jump? Simple: Just set the interrupt vector and then execute an illegal instruction.
-
-
Replying to @oe1cxw @whitequark
I understand what an SMT solver is, but in what context do they generate code?
2 replies 0 retweets 1 like -
in this case I believe it's formal verification of a CPU core
1 reply 0 retweets 6 likes -
Replying to @whitequark
do you have insider information? if you don't and this is a guess, please register me as betting on “superoptimizer” please
2 replies 0 retweets 1 like -
Replying to @rep_stosq_void @whitequark
In this case it was riscv-formal. But superoptimizers and program synthesis are generally are good guesses for SMT solvers writing programs.
1 reply 0 retweets 2 likes -
Replying to @oe1cxw @whitequark
Can you tell me how SMT is used in this case?
1 reply 0 retweets 1 like
Replying to @PLT_cheater @whitequark
Bounded model check. https://github.com/cliffordwolf/riscv-formal … http://symbiyosys.readthedocs.io/
1 reply
0 retweets
3 likes
-
-
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.