A post-doctoral scholar position and PhD positions focusing on symbolic verification techniques for cyber-security are available at the Verification Laboratory (VLab) of the Computer Science Department at the University of California, Santa Barbara (UCSB). The research project titled "Integrated Symbolic execution for Space-Time Analysis of Code (ISSTAC)" involves symbolic execution of Java Bytecode for automatically identifying (1) denial of service attacks (by determining worst case complexity of a program in terms of both time and space usage) and (2) side channel attacks (by determining if observations about the execution time or memory usage of a program can leak secret information). This is a multi-year collaborative effort with researchers from the the Carnegie Mellon University, the Vanderbilt University and the Queen Mary University of London. There are many exciting research directions within the scope of this project, including novel constraint solving techniques, heuristics for scalable symbolic program analysis, automated worst-case behavior analysis, quantitative information flow using symbolic execution, etc.
The positions are available now and will be open until filled.
You can find more information about VLab here and the ISSTAC project here.