Blog

SmartBugs: An Execution Framework for Automated Analysis of Smart Contracts

SmartBugs is a new execution framework that simplifies the execution of automated analysis tools on datasets of Solidity smart …

An Improved Proof of the Handshaking Lemma

In 2009, I posted a calculational proof of the handshaking lemma, a well-known elementary result on undirected graphs. I was very …

Principles and Applications of APS

I am currently in Salamanca (Spain), attending the conference Tools for Teaching Logic III. My talk was on teaching logic through …

Probabilities in Proofreading

Suppose you write a program and you send the source code to two of your friends, ${\cal A}$ and ${\cal B}$. Your two friends read the …

Multiples in the Fibonacci Series

I found the following problem on K. Rustan M. Leino’s puzzles page: [Carroll Morgan told me this puzzle.] Prove that for any …

A Reward Check From Donald Knuth

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 …

A Square Grid Path Problem

Last November I solved Problem 15 of Project Euler (a counting problem involving paths in square grids), and, although the problem …