Quick introduction to SAT/SMT solvers and symbolic execution [pdf]

[jaybosamiya]

http://yurichev.com/tmp/SAT_SMT_DRAFT.pdf

[rurban]

Oh, 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.

[baby]

How can someone call an 85 pages document a "quick" introduction?

[nickpsecurity → baby]

Because 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 → baby]

Well most graduate level math textbooks are called "An Introduction to..." and run to 500+ pages.

[GFK_of_xmaspast → baby]

Might as well read Knuth vol4 fascicle 6 instead: http://www-cs-faculty.stanford.edu/~uno/news.html

[bjornsing]

I'm getting ERR_NAME_NOT_RESOLVED... :(

[KhalilK → bjornsing]

https://web.archive.org/web/20160228093915/http://yurichev.c...

[bjornsing → KhalilK]

Thanks! :)

[jo909 → bjornsing]

Worked fine for me.

[bjornsing → jo909]

I 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

[sriram_malhar]

Lovely writeup!