Three-valued automated reasoning . . .

We deal with the problem of designing suitable languages for the modeling and the automatic verification of proper-ties over analog circuits. To this purpose, we suitably en-rich classical temporal logics with basic formulæ allowing to model arbitrary functions relating analog variables. We show how to automatically check the resulting CTLf for-mulæ on analog circuits. In particular, we rely on interval arithmetic methods and we extend to the analog context a number of techniques for the abstraction and the verification of digital systems, based on three-valued temporal logics