Provide (as background material) a description of the semantic analysis capabilities in JPL's CAESAR tool set.