Blog
-
Encoding Symbolic Expressions as Efficient Solver Queries
This post was originally published on the blog of Dependable Systems Lab at EPFL.
Constraint solving constitutes a major bottleneck in symbolic execution. It is therefore important to maximize solver performance, which in turn can improve path throughput, code coverage, and the number of bugs discovered. In this post, we show that the encoding of symbolic expressions as solver queries significantly impacts the solver performance. By exploring a few points in the design space of query encodings, we discovered performance differences spanning over two orders of magnitude. On a Chef symbolic execution workload, the Z3 constraint solver achieved the best performance when running in a portfolio of incremental and non-incremental configurations, by encoding memory accesses as operations over the array theory and using assertions to initialize constant arrays.
-
The Poor State of Software Testing Today
This post was originally published on the blog of Dependable Systems Lab at EPFL.
Today, software quality assurance is largely synonymous to software testing. Broadly speaking, testing means developers think hard of all relevant inputs that a program (or subcomponent) can receive and write code that executes the program with those inputs, while checking that the program behaves correctly.
subscribe via RSS