Higher-Order Symbolic Execution(arxiv.org)

76 pointsby akakievichvor 10 Jahren10 comments

http://arxiv.org/abs/1507.04817

11 comments

On page 3, I see this:

    (define/contract (f x)
    (positive? . âĘŠ . negative?) ; contract
    (* x -1))

Am I missing fonts or does âĘŠ actually mean something?

groovy2shoesvor 10 Jahren

I see the same thing, but I think it's supposed to be a rightward arrow, as in a function from positive numbers to negative numbers. At least, that's how it usually appears in the Racket documentation.

geographomicsvor 10 Jahren

It does appear to be some encoding issue relating to the Unicode "→" (U+2192). Encoded with UTF-8, this is represented by the three bytes 0xE2 0x86 0x92. In the TeX EC encoding, these correspond to "âĘŠ".

(See https://www.tug.org/TUGboat/Articles/tb11-4/tb30ferguson.pdf, also section 2.3 of http://mirrors.ctan.org/macros/latex/doc/encguide.pdf)

dvh_umdvor 10 Jahren

I've submitted a replacement to arxiv that fixes the encoding issues (arxiv unfortunately does not support xelatex, which I use extensively). That will appear Tue 0:00 GMT.

In the meantime, I've made a version available at https://www.cs.umd.edu/~dvanhorn/jfp-draft-2016.pdf

[deleted]vor 10 Jahren

samthvor 10 Jahren

This is now fixed.

spdegabriellevor 10 Jahren

"it can form the basis of automated verification and bug-finding tools for higher-order programs. "

Does this mean I can verify C++, Haskell, Python, JavaScript & Common Lisp code that uses Higher Order Functions?

samthvor 10 Jahren

That's the idea. We've only done it for Racket so far.

quietplatypusvor 10 Jahren

How is this different from defunctionalizing and converting to smt backend or prolog engine without higher-order capabilities?

samthvor 10 Jahren

Other people have taken that approach, for example the HALO project in Haskell. But the imprecision of the defunctionalizaton often makes it hard to prove the properties you want, especially without static types.

jslivor 10 Jahren

I am looking for papers about converting to prolog backend. Could you name one for me? Thanks.