A crucial problem in software security is the detection of sidechannels. Information gained by observing non-functional properties ofprogram executions (such as execution time or memory usage) can enableattackers to infer secret information (such as a password). In this talk,I will discuss how symbolic execution, combined with a model countingconstraint solver, can be used for quantifying side-channel leakage inJava programs. In addition to computing information leakage for a singlerun of a program, I will also discuss computation of information leakagefor multiple runs for a type of side channels called segmented oracles. Insegmented oracles, the attacker is able to explore each segment of a secret(for example each character of a password) independently. For segmentedoracles, it is possible to compute information leakage for multiple runsusing only the path constraints generated from a single run symbolicexecution. These results have been implemented as an extension to thesymbolic execution tool Symbolic Path Finder (SPF) using the SMT solverZ3 and two model counting constraint solvers LattE and ABC.This is joint work with Lucas Bang and Abdulbaki Aydin from UCSB and CorinaPasareanu and Quoc-Sang Phan from CMU.