Strange Loop

Next: September 12-14 2019


Stifel Theatre


St. Louis, MO

Register for 2019!

Finding bugs without running or even looking at code

What if you could find complex bugs in systems without ever having looked at any of the code, without running the code, without cloning the code, or even knowing what language the code is written in or where its git repo lives? What if you could validate the correctness of an architectural proposal before writing code?

While this might sound impossible, it's in fact quite doable, and happening every day!

Tools called "model checkers" can be used to model and analyze the architecture/design of a system. Model checkers can simulate every possible sequence of operations your system might ever encounter, and check if desired properties always hold. And if a property doesn't hold, the model checker will show you an exact sequences of operations that violates it.

Benefit can be had both in the early design stages of a project, or if you're a newcomer trying to get up-to-speed on an existing system. Examples of both will be shown.

This talk will describe the model checker Alloy ( I'll show how we used it to invalidate a large amount of work by one group (before multiple teams started to try integrating with that work). I'll also show how we employed it to find a highly subtle security flaw in another group's project, without ever looking at a single line of code from either group. In both cases, we did this simply by talking to teams about the architecture of their systems, and translating those designs into formal specifications.

Jay Parlar

Jay Parlar


Jay Parlar has been at Rackspace since early 2014, working on both internal tooling and customer-facing applications. He has a Ph.D. in Software Engineering, and is currently focusing on the application of formal methods (TLA+, Alloy) to Rackspace systems. Jay is one of three employees of Rackspace Canada. Despite working mostly in JavaScript while at Rackspace, he considers himself to be a "Python guy", having made Python his language of choice all the way back in 2001.