@BOOK{Dolev00, author = {S. Dolev}, title = {Self-Stabilization}, publisher = {The MIT Press}, year = {200} } @ARTICLE{Dijkstra74, author = {E. W. Dijkstra}, title = {Self-Stabilization Systems in spite of Distributed Control}, journal = {Communication of the ACM}, year = {1974}, volume = {17}, pages = {643--644} } @ARTICLE{BEL99, author = {E. Birnbaum and E. L. Lozinskii}, title = {The Good Old {D}avis-{P}utnam Procedure Helps Counting Models}, journal = {Journal of Artificial Intelligence Research}, year = {1999}, volume = {10}, pages = {457--477} } @ARTICLE{Cla86, AUTHOR = {E. M. Clarke and E. A. Emerson and A. P. Sistla}, TITLE = {Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications}, JOURNAL = {ACM Transactions on Programming Languages and Systems}, YEAR = {1986}, volume = {8}, number = {2}, pages = {244--263} } @INPROCEEDINGS{Yo96, author = {W. D. Young}, title = {Comparing Verification Systems: Interactive Consistency in {ACL2}}, booktitle = {Proc. 11th Annual Conference on Computer Assurance}, year = {1996}, pages = {17--21} } @inproceedings{Church57, address = {Princeton}, author = {A. Church}, booktitle = {Summaries of talks presented at the Summer Institute for Symbolic Logic}, organization = {Communications Research Division, Institute for Defense Analyses}, pages = {3--50}, title = {Application of Recursive Arithmetic to the Problem of Circuit Synthesis}, year = 1957, } @INPROCEEDINGS{OB09, author = {F. Ouchet and D. Borrione and K. Morin-Allory and L. Pierre}, title = {High-level Symbolic Simulation for Automatic Model Extraction}, booktitle = {Proc. IEEE Symposium on Design and Diagnostics of Electronic Systems}, year = {2009} } @inproceedings{BaarirBCEILMPP09, author = {S. Baarir and C. Braunstein and R. Clavel and E. Encrenaz and J.-M. Ili{\'e} and R. Leveugle and I. Mounier and L. Pierre and D. Poitrenaud}, title = {Complementary Formal Approaches for Dependability Analysis}, booktitle = {Proc. International Symposium on Defect and Fault Tolerance in VLSI Systems}, publisher = {IEEE Computer Society}, year = {2009}, pages = {331--339}, ee = {http://doi.ieeecomputersociety.org/10.1109/DFT.2009.21}, bibsource = {DBLP, http://dblp.uni-trier.de} } @INPROCEEDINGS{DA08, author = {A. Darbari and B. Al-Hashimi and P. Harrod and D. Bradley}, title = {A New Approach for Transient Fault Injection using Symbolic Simulation}, booktitle = {Proc. IEEE International On-Line Testing Symposium}, pages = {93--98}, publisher = {IEEE Computer Society}, year = {2008} } @inproceedings{FeySD09, author = {G. Fey and A. S{\"u}lflow and R. Drechsler}, title = {Computing Bounds for Fault Tolerance using Formal Techniques}, booktitle = {Proc. Design Automation Conference}, year = {2009}, pages = {190--195}, publisher = {ACM}, ee = {http://doi.acm.org/10.1145/1629911.1629963}, bibsource = {DBLP, http://dblp.uni-trier.de} } @INPROCEEDINGS{FD08, author = {G. Fey and R. Drechsler}, title = {A Basis for Formal Robustness Checking}, booktitle = {Proc. IEEE International Symposium on Quality Electronic Design}, pages = {784--789}, publisher = {IEEE Computer Society}, year = {2008} } @INPROCEEDINGS{AL05, author = {L. Anghel and R. Leveugle and P. Vanhauwaert}, title = {Evaluation of {SET} and {SEU} Effects at Multiple Abstraction Levels}, booktitle = {Proc. 11th IEEE International On-Line Testing Symposium}, year = {2005} } @ARTICLE{BC06, author = {H. Bar-El and H. Choukri and D. Naccache and M. Tunstall and C. Whelan}, title = {The Sorcerer's Apprentice Guide to Fault Attacks}, journal = {Proceedings of the IEEE}, year = {2006}, volume = {94}, number = {2} } @ARTICLE{LH03, author = {R. Leveugle and K. Hadjiat}, title = {Multi-level Fault Injections in {VHDL} Descriptions: Alternative Approaches and Experiments}, journal = {Journal of Electronic Testing: Theory and Applications}, year = {2003}, volume = {19}, number = {5} } @INPROCEEDINGS{SL07, author = {S. Seshia and W. Li and S. Mitra}, title = {Verification-guided Soft Error Resilience}, booktitle = {Proc. Conference on Design, Automation and Test in Europe}, pages = {1442--1447}, publisher = {EDA Consortium}, year = {2007} } @INPROCEEDINGS{Le05, author = {R. Leveugle}, title = {A New Approach for Early Dependability Evaluation Based on Formal Property Checking and Controlled Mutation}, booktitle = {Proc. IEEE International On-Line Testing Symposium}, pages = {260--265}, publisher = {IEEE Computer Society}, year = {2005} } @INPROCEEDINGS{KP06, author = {U. Krautz and M. Pflanz and C. Jacobi and H. Tast and K. Weber and H. Vierhaus}, title = {Evaluating Coverage of Error Detection Logic for Soft Errors using Formal Methods}, booktitle = {Proc. Conference on Design, Automation and Test in Europe}, pages = {176--181}, publisher = {European Design and Automation Association}, year = {2006} } @INPROCEEDINGS{LH07, author = {D. Larsson and R. H\"ahnle}, title = {Symbolic Fault Injection}, booktitle = {Proc. International Verification Workshop}, series = {CEUR Workshop Proceedings}, year = {2007} } @PhdThesis{PhDAl05, author = {G. Al Sammane}, title = {Symbolic Simulation of Circuits Described at the Algorithmic Level}, school = {Joseph Fourier University, Grenoble, France}, year = {2005} } @book{KM02, author = "M. Kaufmann and P. Manolios and J. Moore", title = {Computer Aided Reasoning: an Approach}, publisher = {Kluwer Academic Pub.}, year = {2002} } @inproceedings{BK96, author = {B. Brock and M. Kaufmann and J Moore}, title = {{ACL2} Theorems about Commercial Microprocessors}, booktitle = {Proc. FMCAD'96}, year = 1996 } @inproceedings{SW99, author = "J. Sawada and W. A. Hunt", title = "Results of the Verification of a Complex Pipelined Machine Model", booktitle = "Proc. CHARME'99", year = "1999" } @Article{ML98, author = {J. Moore and T. Lynch and M. Kaufmann}, title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5K86} Floating-Point Division Algorithm}, year = "1998", journal = "IEEE Trans. on Computers", volume = "47", number = "9" } @book{KM00, author = "M. Kaufmann and P. Manolios and J. Moore", title = {Computer Aided Reasoning: {ACL2} Case Studies}, publisher = {Kluwer Academic Pub.}, year = {2000} } @INPROCEEDINGS{Vis96, author = {The {VIS} group}, title = {{VIS} : A System for Verification and Synthesis}, booktitle = {Proc. International Conference on Computer Aided Verification}, year = {1996}, volume = {1102}, series = {Lecture Notes in Computer Science}, pages = {428--432}, publisher = {Springer-Verlag}, url = {citeseer.ist.psu.edu/brayton96vis.html} } @inproceedings{BiereCCZ99, author = {A. Biere and A. Cimatti and E. M. Clarke and Y. Zhu}, title = {Symbolic Model Checking without {BDD}s}, booktitle = {Proc. International Conference on Tools and Algorithms for Construction and Analysis of Systems}, year = {1999}, pages = {193--207}, series = {Lecture Notes in Computer Science}, volume = {1579}, publisher = {Springer} } @inproceedings{Strichman00, author = {O. Shtrichman}, title = {Tuning {SAT} Checkers for Bounded Model Checking}, booktitle = {Proc. International Conference on Computer Aided Verification}, year = {2000}, pages = {480--494}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {1855}, } @inproceedings{DBLP:conf/sat/Thurley06, author = {Marc Thurley}, title = {sharpSAT - Counting Models with Advanced Component Caching and Implicit BCP}, booktitle = {SAT}, year = {2006}, pages = {424-429}, ee = {http://dx.doi.org/10.1007/11814948_38}, crossref = {DBLP:conf/sat/2006}, bibsource = {DBLP, http://dblp.uni-trier.de} }