5 ms·
Quick introduction to SAT/SMT solvers and symbolic execution [pdf]
- bjornsing 11y agoI'm getting ERR_NAME_NOT_RESOLVED... :(
- jo909 11y agoWorked fine for me.
- bjornsing 11y agoI can resolve it (as 78.46.87.164) with Google's DNS, but then I'm getting ERR_ADDRESS_UNREACHABLE instead... Somewhere on the interwebs there must be some mighty strange routing: $ traceroute 78.46.87.164 traceroute to 78.46.87.164 (78.46.87.164), 64 hops max, 52 byte packets 1 192.168.1.1 (192.168.1.1) 1.238 ms 1.078 ms 1.066 ms 2 46-236-104-1.customer.t3.se (46.236.104.1) 3.896 ms 1.577 ms 1.317 ms 3 46.236.64.69 (46.236.64.69) 5.090 ms 5.281 ms 2.261 ms 4 46.236.64.69 (46.236.64.69) 1.560 ms !H * 3.568 ms !H
- KhalilK 11y agohttps://web.archive.org/web/20160228093915/http://yurichev.com/tmp/SAT_SMT_DRAFT.pdf https://web.archive.org/web/20160228093915/http://yurichev.c...
- bjornsing 11y agoThanks! :)
- baby 11y agoHow can someone call an 85 pages document a "quick" introduction?
- GFK_of_xmaspast 11y agoMight as well read Knuth vol4 fascicle 6 instead: http://www-cs-faculty.stanford.edu/~uno/news.html http://www-cs-faculty.stanford.edu/~uno/news.html
- nickpsecurity 11y agoBecause it's (a) shorter than full texts on the subject and (b) most of that is the examples. For (b), you can choose how much you want to read.
- greydius 11y agoWell most graduate level math textbooks are called "An Introduction to..." and run to 500+ pages.
- sriram_malhar 11y agoLovely writeup!
- rurban 11y agoOh, it's still missing cbmc or Saturn, which are IMHO the easiest way to translate C problems to SMT problems, because it translates the symbolic C problem automatically. klee still has weird installation issues and a weird syntax, and with z3, coq, akka, agda, HOL, Isabelle and the other prover frameworks you have do it manually. I'd rather use the decade old lisp tools than learning ML or their odd syntax.