1. 6

Abstract: “Most current approaches to software verification are one-sided – a safety prover will try to prove that a program is safe, while a bug-finding tool will try to find bugs… The result of taking a one-sided approach to verification is false alarms: safety provers will often claim that safe programs have errors, while bug-finders will often be unable to find errors in unsafe programs. In this thesis we will show that it is possible to analyse C programs without generating false alarms, even if they contain unbounded loops, use non-linear arithmetic and have integer overflows.”

  1.  

  2. 7

    I found this digging through blog comments. In particular, author posted this sad comment that mirrors what many academics have said:

    https://lcamtuf.blogspot.com/2015/02/symbolic-execution-in-vuln-research.html?showComment=1423739841139#c809183368713494449

    “As an academic you are actively disincentivised from building robust tools. This is because you are evaluated only on the number of papers you write. If I spend 6 months productionising one of my research tools, that’s at least one paper I haven’t written. The productionising work is completely invisible to the system evaluating me and so to all intents and purposes I’ve done nothing for 6 months. These tools are very complex and most academics are very bad engineers, so it is unsurprising that our tools rarely work robustly. As a result, most people will refuse to let others even see their code out of embarrassment.”

    Beyond sad. There’s so much capability trapped in CompSci that can’t get out due to academic systems that punish implementors. Antti Kantee who did the Rump Kernel work told me same thing happened to him where they didn’t care he actually built the thing for people to use. We need strong focus by entrepreneurs, activists, and FOSS on helping get some of the better results implemented and/or productized. Much like tech transfer to companies, I would like to see FOSS-oriented companies or nonprofits constantly implementing stuff in reusable form that they incorporate in products they sell to generate funding. On top of donations, grants, or industry collaborations.

    1. 3

      I think it’s true that it isn’t incentivized enough, but it’s not entirely unincentivized. You get “paid” for releasing robust software other people use in the form of citations, which in CS at least are increasingly valuable currency (people care about Google Scholar h-indexes more than they care about journal impact factors). It’s not always a net win over writing more papers, but releasing a system other people use does tend to increase citations. For example the Stanford CoreNLP Toolkit paper has 1300 citations, the WordNet system’s paper has 9000 citations, the WEKA data-mining toolkit’s paper has 14,000 citations, etc. In machine learning, the relatively new Journal of Machine Learning Open Source Software aims to explicitly encourge that by providing a venue to publish a paper just on the software.

      Academics not being good software engineers is a problem though. Plenty of people are just not really good at making a robust implementation even if they wanted to spend 6 months on it, and don’t have funding that is earmarked in a way that would let them hire a programmer to do it. Some exceptions, e.g. German grant agencies explicitly fund software work, which is what’s paid for Potassco to be released and maintained.

      1. 1

        “I think it’s true that it isn’t incentivized enough, but it’s not entirely unincentivized. You get “paid” for releasing robust software other people use in the form of citations, which in CS at least are increasingly valuable currency”

        That’s not generally correct. The citations are important but they’re paid to publish papers. The implementation or its distribution is optional unless funder demands it. The papers themselves can be paywalled with many good ones otherwise unavailable for free. The methods are sometimes patented. The software might be closed + paid, closed + free, restricted + free, open + paid, or open + free. It’s all over the place with all kinds of tools either not open or encumbered with high fees.

        On top of this, many places reward only papers being published with quantity over quality. Interacts with other problems as vicious circle.

        1. 3

          It’s correct in the parts of CS academia I’ve spent the past 15 years in. After the first few years of your career, publishing papers just to publish more papers is fairly useless; another 5 conference papers when you have 50 or 100 is noise as far as your CV goes. What you really need to make the next step are either very high-profile papers (Nature type stuff) or very highly cited papers, not just more papers. Getting press also counts; when I was at Georgia Tech, for promotion to full Professor you basically had to develop a public profile with things like media appearances. There are various strategies for racking up highly cited papers and media appearances, and increasingly, releasing software is one of the methods, though there are others. Does vary a lot by sub-area, though. In my area (AI), lots of people publish open-source software, and the incentives tend to encourage it.

          As for paywalls, I don’t love them, but for new research, these days I honestly rarely find one. Who in CS doesn’t put their publications on their academic webpage and/or on arXiv? Heck, most papers in AI, at least, are published first on arXiv, only later in conferences or journals.

          1. 1

            Your points are definitely true for AI. I’ve seen plenty of papers and software for it. For the rest, it seems to vary by school and research group. Might be worthwhile to mske a list of all the groups regularly FOSSing work. Then, start sending people emails asking if they’re interested in project ideas or related work/tooling in their interest area that might be built into great tools or ecosystem over time. Probably cite LLVM, Haskell, or Coq as examples of intended effect where many contributors snowball the overall tool into something immensely practical.

            What you think?