The worst-case execution time analyzer aiT originally developed by Saarland University and AbsInt GmbH computes safe and precise upper bounds for the WCETs of tasks. It relies on a pipeline model that usually has been handcrafted. We present some new approaches aiming at automatically obtaining a pipeline model as required by aiT from a formal processor description in VHDL or Verilog. The derivation of the total WCET from the basic-block WCETs requires knowledge about upper bounds on the number of loop iterations. We present a new method for loop bound detection using dataflow analysis to derive loop invariants. A task may contain infeasible paths caused by conditionals with logically related conditions. We present a static analysis that identifies and collects conditions from the executable, and relates these collections to detect infeasible paths. This new analysis uses the results of a novel generic slicer on the level of binary code.