"We developed a Quantifier-Elimination (QE) based compositional verification technique for systems with time-dependent contracts and extended our Redlog based tool to be able to compose time-dependent properties. (Note Redlog is a public domain tool that can perform quantifier elimination.) We begin by showing how quantifier elimination is applicable to Assume-Guarantee style contracts composition. In compositional verification, the goal is to prove/disprove a system level contract from the given component level contracts. The state-of-the-art verification tool AGREE tries to sequentially prove that each component assumption is satisfied by the system assumption and its upstream components’ guarantees, following which the conjunction of all component contracts and system assumption is used to verify the system guarantee. In contrast, in our QE-based approach, we derive, in a single step, the strongest system contract given the component contracts---the formalism was developed in our earlier work. For time-independent contracts (described by predicates over inputs and outputs), any postulated system contract can be verified by performing a simple implication verification from the inferred strongest system contract. For time-dependent contracts, the composition to infer the strongest system-level contract requires additional work, namely, replicating the given contracts by shifting those along time so the entire time-horizon of interest is captured, where time-horizon (or order) of a system contract is simply the sum of the time-horizons (or orders) of the contracts. Next the initial conditions of components are also composed to obtain the system level initial condition, which is used alongside the inferred strongest system property, to verify postulated system property through induction. We implemented a new prototype tool called RELIQE (REduced Logic Inference using Quantifier Elimination) and demonstrated it through a composition of a vehicle model."