# Analysing D Code with KLEE

Published

KLEE is symbolic execution engine that can rigorously verify or find bugs in software. It’s designed for C and C++, but it’s just an interpreter for LLVM bitcode combined with theorem prover backends, so it can work with bitcode generated by ldc2. One catch is that it needs a compatible bitcode port of the D runtime to run normal D code. I’m still interested in getting KLEE to work with normal D code, but for now I’ve done some experiments with -betterC D.

# Why Sorting is O(N log N)

Published

Any decent algorithms textbook will explain how fast sorting algorithms like quicksort and heapsort are, but it doesn’t take crazy maths to prove that they’re as asymptotically fast as you can possibly get.

# Counting Sudoku Solution Grids using Monte Carlo

Published

Tags: and

How many ways can you fill a 9x9 grid, obeying all the rules of the sudoku puzzle? The answer is too big to just calculate directly on a computer, so an exact answer takes careful analysis. But if an absolutely exact answer isn’t required, we can get a good statistical approximation using a Monte Carlo algorithm. As a bonus, the algorithm doesn’t need any application-specific analysis and works on many other problems, too. It’s a handy “stupid things that work” approach to solving problems.

# Compression, Complexity and Software System Design

Published

Information theory gives us a way to understand communication systems, by giving us a way to understand what happens to information as it’s transmitted or re-encoded.

We can also study what happens to complexity in a software system as components depend on or interface each other. Just like we can make rigorous arguments about how much information can be compressed, we can make arguments about how much complexity can be simplified, and use this to make better choices when designing software systems.