Three-Valued Automated Reasoning on Analog Properties

In: 17th ACM Great Lakes Symposium on VLSI (GLSVLSI '07). Stresa-Lago Maggiore, Italy. ACM Press, P. 485--488, March, 2007

Authors

• Raffaella Gentilini
• Klaus Schneider
• Alexander Dreyer

Abstract

"We deal with the problem of designing suitable languages for the modeling and the automatic verification of properties over analog circuits. To this purpose, we suitably enrich classical temporal logics with basic formulae allowing to model arbitrary functions relating analog variables. We show how to automatically check the resulting CTLf formulae 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.

© ACM, (2007). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 17th Great Lakes Symposium, (2007) http://doi.acm.org/10.1145/1228784.1228899 ."

Full Text

• Publication: GentiliniSchneiderDreyerGLSVLSI07-author.pdf

BibTeX

 
@InProceedings{  GentilinSchneiderDreyerGLS07, 
   title = { Three-Valued Automated Reasoning on Analog Properties }, 
   author = { Raffaella Gentilini and Klaus Schneider and Alexander Dreyer },   
   booktitle = { 17th ACM Great Lakes Symposium on VLSI  (GLSVLSI '07).  Stresa-Lago Maggiore, Italy },        
   publisher = { ACM Press },   
   pages = { 485--488 },  
   month = mar, 
   year = 2007, 
} 

---

This publication belongs to the project VerSiS.