While browsing information about compilers I found it difficult to find a formal definition of SSA form (Static Single Assignment). For whatever reason, it's often under-specified or simplifed. So anyway, if you are like me and like formal definitions, here it is.

A program is in SSA form when:

The concept of domination is from graph theory: an instruction A dominates another B when all the paths from the entry point of the program to B go through A.

Please let me know if the definition above looks wrong to you. Finally, if you want informal examples, the Wikipedia page has plenty!