@inproceedings{afde6e1aa3e0481e970b9907e58a7fd8,
title = "Verifying analog oscillator circuits using forward/backward abstraction refinement",
abstract = "Properties of analog circuits can be verified formally by partitioning the continuous state space and applying hybrid system verification techniques to the resulting abstraction. To verify properties of oscillator circuits, cyclic invariants need to be computed. Methods based on forward reachability have proven to be inefficient and in some cases inadequate in constructing these invariant sets. In this paper we propose a novel approach combining forward- and backward-reachability while iteratively refining partitions at each step. The technique can yield dramatic memory and runtime reductions. We illustrate the effectiveness by verifying, for the first time, the limit cycle oscillation behavior of a third-order model of a differential VCO circuit.",
author = "Goran Frehse and Krogh, {Bruce H.} and Rutenbar, {Rob A.}",
year = "2006",
doi = "10.1109/date.2006.244113",
language = "English (US)",
isbn = "3981080114",
series = "Proceedings -Design, Automation and Test in Europe, DATE",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
booktitle = "Proceedings - Design, Automation and Test in Europe, DATE'06",
address = "United States",
note = "Design, Automation and Test in Europe, DATE'06 ; Conference date: 06-03-2006 Through 10-03-2006",
}