Blog

SmartBugs is a new execution framework that simplifies the execution of automated analysis tools on datasets of Solidity smart contracts. SmartBugs currently supports 10 tools. It has a simple plugin system to easily add new analysis tools, based on Docker images. It supports parallel execution of the tools to speed up the execution time. It also normalizes the output that tools produce to facilitate experiments. SmartBugs was developed in the context of an empirical review of automated analysis tools on 47,587 Ethereum smart contracts.

In 2009, I posted a calculational proof of the handshaking lemma, a well-known elementary result on undirected graphs. I was very pleased about my proof because the amount of guessing involved was very small (especially when compared with conventional proofs). However, one of the steps was too complicated and I did not know how to improve it. In June, Jeremy Weissmann read my proof and he proposed a different development. His argument was well structured, but it wasn’t as goal-oriented as I’d hoped for.

I am currently in Salamanca (Spain), attending the conference Tools for Teaching Logic III. My talk was on teaching logic through algorithmic problem solving and it went quite well, I think. In particular, it seems that the audience enjoyed the examples that I have used and the teaching scenarios that I have shown. As a result, I have promised that I would upload my PhD thesis into this website. Since the thesis can also be useful for other people, I have decided to write a new blog post.

Suppose you write a program and you send the source code to two of your friends, $\mathcal{A}$ and $\mathcal{B}$. Your two friends read the code and when they finish, $A$ errors are detected by $\mathcal{A}$, $B$ errors are detected by $\mathcal{B}$, and $C$ errors are detected by both. So, in total, $A+B-C$ errors are detected and can now be eliminated. We wish to estimate the number of errors that remain unnoticed and uncorrected.

I found the following problem on K. Rustan M. Leino’s puzzles page: [Carroll Morgan told me this puzzle.] Prove that for any positive K, every Kth number in the Fibonacci sequence is a multiple of the Kth number in the Fibonacci sequence. More formally, for any natural number n, let F(n) denote Fibonacci number n. That is, F(0) = 0, F(1) = 1, and F(n+2) = F(n+1) + F(n).

The other day I went to my pigeon-hole to collect my snail mail, and I had a letter from Donald E. Knuth, Professor Emeritus of the Art of Computer Programming! Inside, there was a check for a correction I sent him some months ago. In fact, it was not really a correction; it was more like a comment. And it was so obvious (he even said that) that he just sent $0.