  Datalog has become a popular language for writing static analyses. Because
Datalog is very limited, some implementations of Datalog for static analysis
have extended it with new language features. However, even with these features
it is hard or impossible to express a large class of analyses because they use
logical formulae to represent program state. FormuLog fills this gap by
extending Datalog to represent, manipulate, and reason about logical formulae.
We have used FormuLog to implement declarative versions of symbolic execution
and abstract model checking, analyses previously out of the scope of
Datalog-based languages. While this paper focuses on the design of FormuLog and
one of the analyses we have implemented in it, it also touches on a prototype
implementation of the language and identifies performance optimizations that we
believe will be necessary to scale FormuLog to real-world static analysis
problems.
