Dr Martin Nyx Brain

Our ability to build complex computer systems vastly exceeds our ability to understand them. Security vulnerabilities and bugs are examples of unintended and unanticipated consequences of seemingly simple and understood systems.

I want a tool that takes a piece of software and finds all of the bugs in it. I can’t find one that does the job so I am trying to make one. My paper with Elizabeth Polgreen, A Pyramid Of (Formal) Software Verification, explains how I view the problem and how it breaks into two parts:

1. Tools that turns real software into logical formulae. For this, I work on CBMC and care about (bounded) model checking, abstract interpretation, deductive verification and other forms of static analysis.
2. Tools that check if the formulae are true or false. For this, I work on cvc5 (link 1 and link 2) and care about automated reasoning, satisfiability modulo theories, decision procedures, computational algebraic geometry, expression synthesis, numerical computation and abstract algebra.

Contact details:

• Email: martin.brain@citystgeorges.ac.uk
• Full profile