Automated generation of BSP automata BulkSynchronous Parallel (BSP) is a bridging model between abstract execution and concrete parallel architecture. In order to model BSP program  executions Hains adapted the finite automata theory to the BSP paradigm by introducing BSP automata theory.  Benefit provided by BSP automata is twofold: modeling BSP program control and parallelizing finite state automata.  The lack of generation algorithm of BSP automata and the illusory lack of application of this theory has been preventing this theory from being used.  We propose in this paper an algorithm that generates a BSP automaton recognizing a defined BSP language.  In order to demonstrate the usefulness of BSP automata and help to design its use, two applications of the BSP automata theory are provided. The parallel recognition of an expression and debugging of a BSP program.

Benchmarking Symbolic Execution Using Constraint Problems  Initial Results. Symbolic execution is a powerful technique for bug finding and program testing. It is successful in finding bugs in realworld code. The core reasoning techniques use constraint solving, path exploration, and search, which are also the same techniques used in solving combinatorial problems, e.g., finitedomain constraint satisfaction problems (CSPs). We propose CSP instances as more challenging benchmarks to evaluate the effectiveness of the core techniques in symbolic execution. We transform CSP benchmarks into C programs suitable for testing the reasoning capabilities of symbolic execution tools. From a single CSP P, we transform P depending on transformation choice into different C programs. Preliminary testing with the KLEE, TracerX, and LLBMC tools show substantial runtime differences from transformation and solver choice. Our C benchmarks are effective in showing the limitations of existing symbolic execution tools. The motivation for this work is we believe that benchmarks of this form can spur the development and engineering of improved core reasoning in symbolic execution engines.