First, some background: I’ve been busy working on CrossHair lately. It uses symbolic execution to check properties of Python programs. Z3 is a popular SMT solver (kind of theorem prover) that CrossHair uses.

As of the last week or so, CrossHair can check properties of Python programs using regular expressions. You can fiddle with an example in the CrossHair playground, here. Below, I ramble about my adventure in making this work.

Z3 has some native support for regular expressions. Initially, I thought this would work to model regular expressions in Python. …

Phillip Schanely

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store