@manual{rulebase06userguide,
  author = {Model Checking Systems group},
  title = {RuleBase Parallel Edition,User's Guide},
  year = {2005},
  note = {verion 1.26}
}

@inproceedings{Vis,
  author = {The VIS group},
  title = {VIS : A System for Verification and Synthesis},
  booktitle = {CAV'96: Proceedings of the 8th International Conference on Computer Aided Verification},
  publisher = {Springer-Verlag},
  year = {1996},
  volume = {1102},
  pages = {428--432},
  url = {citeseer.ist.psu.edu/brayton96vis.html}
}

@article{DBLP:journals/fmsd/CohenN09,
  author = {Ariel Cohen 0002 and Kedar S. Namjoshi},
  title = {Local proofs for global safety properties},
  journal = {Formal Methods in System Design},
  year = {2009},
  volume = {34},
  number = {2},
  pages = {104-125}
}

@inproceedings{aagaard03hazards,
  author = {M.~Aagaard},
  title = {A Hazards-Based Correctness Statement for Pipelined Circuits.},
  booktitle = {Proceedings of the 12th IFIP WG 10.5 Advanced Research Working Conference},
  publisher = {Springer},
  year = {2003},
  volume = {2860},
  pages = {66-80}
}

@inproceedings{alder06ticc,
  author = {B.T.~Adler and L.~de Alfaro and L.~Dias da Silva and M.~Faella and A.~Legay and V.~Raman and P.~Roy},
  title = {Ticc: A Tool for Interface Compatibility and Composition.},
  booktitle = {CAV'06: Proceedings of 18th International Conference of Computer Aided Verification},
  year = {2006},
  volume = {4144},
  pages = {59-62}
}

@article{akers78,
  author = {B.~Akers},
  title = {Binary Decision Diagrams},
  journal = {IEEE Transactions on Computers},
  year = {1978},
  volume = {27},
  number = {6},
  pages = {509--516}
}

@inproceedings{alfaro01interface,
  author = {L.~de Alfaro and T.A.~Henzinger},
  title = {Interface automata},
  booktitle = {ESEC/FSE-9: Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering},
  publisher = {ACM Press},
  year = {2001},
  pages = {109--120},
  doi = {http://doi.acm.org/10.1145/503209.503226}
}

@inproceedings{DBLP:conf/frocos/AlfaroSFLRS05,
  author = {Luca de Alfaro and Leandro Dias da Silva and Marco Faella and Axel Legay and Pritam Roy and Maria Sorea},
  title = {Sociable Interfaces.},
  booktitle = {FroCos'05: Proceedings of the 5th International Workshop on Frontiers of Combining Systems},
  publisher = {Springer},
  year = {2005},
  volume = {3717},
  pages = {81-105}
}

@inproceedings{bhdl03,
  author = {A.~Aljer and P.~Devienne and S.~Tison and J-L.~Boulanger and G.~Mariano},
  title = {BHDL: Circuit Design in B},
  booktitle = {ACSD '03: Proceedings of the Third International Conference on Application of Concurrency to System Design},
  year = {2003},
  pages = {241}
}

@inproceedings{alur99automating,
  author = {R. Alur and L.~de Alfaro and T. A. Henzinger and F.~Y.C. Mang},
  title = {Automating Modular Verification},
  booktitle = {CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings},
  publisher = {Springer},
  year = {1999},
  volume = {1664},
  pages = {82-97},
  url = {http://link.springer.de/link/service/series/0558/bibs/1664/16640082.htm}
}

@article{DBLP:journals/fmsd/AlurH99b,
  author = {R.~Alur and T.A.~Henzinger},
  title = {Reactive Modules.},
  journal = {Formal Methods in System Design},
  publisher = {Springer},
  year = {1999},
  volume = {15},
  number = {1},
  pages = {7-48}
}

@inproceedings{alur98alternatingtime,
  author = {Rajeev Alur and Thomas A. Henzinger and Orna Kupferman},
  title = {Alternating-Time Temporal Logic},
  booktitle = {COMPOS},
  publisher = {Springer},
  year = {1997},
  volume = {1536},
  pages = {23-60}
}

@inproceedings{alur98mocha,
  author = {R.~Alur and T.A.~Henzinger and F.Y. C.~Mang and S.~Qadeer and S.K.~Rajamani and S.~Tasiran},
  title = {MOCHA: Modularity in Model Checking},
  booktitle = {CAV'98: Proceedings of the 10th International Conference on Computer Aided Verification},
  year = {1998},
  volume = {1427},
  pages = {521-525}
}

@inproceedings{amla01assume,
  author = {N.~Amla and E.~A.~Emerson and K.~S.~Namjoshi and R.~J.~Trefler},
  title = {Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams},
  booktitle = {TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  publisher = {Springer-Verlag},
  year = {2001},
  pages = {465--479}
}

@inproceedings{DBLP:conf/lpar/AndrausLS08,
  author = {Zaher S. Andraus and Mark H. Liffiton and Karem A. Sakallah},
  title = {Reveal: A Formal Verification Tool for Verilog Designs},
  booktitle = {LPAR},
  publisher = {Springer},
  year = {2008},
  volume = {5330},
  pages = {343-352}
}

@inproceedings{DBLP:conf/dac/AndrausS04,
  author = {Zaher S. Andraus and Karem A. Sakallah},
  title = {Automatic abstraction and verification of verilog models},
  booktitle = {DAC},
  publisher = {ACM},
  year = {2004},
  pages = {218-223}
}

@article{arieliA98value,
  author = {Ofer Arieli and Arnon Avron},
  title = {The Value of the Four Values.},
  journal = {Artif. Intell.},
  year = {1998},
  volume = {102},
  number = {1},
  pages = {97-141}
}

@book{arnold94finite,
  author = {A.~Arnold},
  title = {Finite Transition Systems: Semantics of Communicating Systems},
  publisher = {Prentice Hall International Ltd.},
  year = {1994}
}

@article{DBLP:journals/entcs/AwedhS06,
  author = {M.~Awedh and F.~Somenzi},
  title = {Termination Criteria for Bounded Model Checking: Extensions and Comparison},
  journal = {Electronic Notes in Theoritical Computer Science.},
  year = {2006},
  volume = {144},
  number = {1},
  pages = {51-66}
}

@inproceedings{Awhed04Proving,
  author = {M.~Awedh and F.~Somenzi},
  title = {Proving More Properties with Bounded Model Checking},
  booktitle = {CAV'04: Proceedings of the 16th International Conference on Computer Aided Verification},
  publisher = {Springer},
  year = {2004},
  volume = {3114},
  pages = {96-108}
}

@manual{bmanual,
  author = {B-Core(UK) Ltd.},
  title = {B-Toolkit User's Manual},
  year = {1997},
  edition = {release 3.7},
  url = {http://www.b-core.com/downloading.html}
}

@inproceedings{BP-msr03,
  author = {M.~Baclet and R.~Pacalet},
  title = {Vérifications du protocole~VCI},
  booktitle = {Actes du 4ème Colloque sur la Modélisation des Systèmes Réactifs (MSR'03)},
  publisher = {Hermès},
  year = {2003},
  pages = {431-445},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/vci-msr03.ps}
}

@inproceedings{broissyval,
  author = {F.~Badeau and A.~Amelot},
  title = {Using B as a High Level Programming Language in an Industrial Project: Roissy VAL},
  booktitle = {ZB 2005: Formal Specification and Development in Z and B},
  publisher = {Springer Berlin / Heidelberg},
  year = {2005},
  volume = {3455/2005},
  pages = {334-354},
  url = {http://www.springerlink.com/content/x8mcgk2p8r82e2gl/},
  doi = {http://dx.doi.org/10.1007/11415787_20}
}

@inproceedings{503274,
  author = {T.~Ball and S.K.~Rajamani},
  title = {The SLAM project: debugging system software via static analysis},
  booktitle = {POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  year = {2002},
  pages = {1--3},
  doi = {http://doi.acm.org/10.1145/503272.503274}
}

@inproceedings{rulebase96,
  author = {I.~Beer and S.~Ben-David and C.~Eisner and A.~Landver},
  title = {RuleBase: an industry-oriented formal verification tool},
  booktitle = {DAC '96: Proceedings of the 33rd annual conference on Design automation},
  year = {1996},
  pages = {655--660},
  doi = {http://doi.acm.org/10.1145/240518.240642}
}

@inproceedings{bmethod99meteor,
  author = {P.~Behm and P.~Benoit and A.~Faivre and J-M.~Meynadier},
  title = {Météor: A Successful Application of B in a Large Project},
  booktitle = {World Congress on Formal Methods},
  publisher = {Springer},
  year = {1999},
  volume = {1708},
  pages = {369-387}
}

@inproceedings{1517440,
  author = {Bjesse, Per},
  title = {Word-level sequential memory abstraction for model checking},
  booktitle = {FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design},
  publisher = {IEEE Press},
  year = {2008},
  pages = {1--9}
}

@techreport{prosyd05,
  author = {R. Bloem and B. Jobstmann and A. Pnueli.},
  title = {Property-based Logic Synthesis for Rapid Design Prototyping},
  year = {2005}
}

@article{bozga97protocol,
  author = {M.~Bozga and J-C.~Fernandez and A.~Kerbrat and L.~Mounier},
  title = {Protocol Verification with the ALDÉBARAN Toolset.},
  journal = {STTT},
  publisher = {Springer},
  year = {1997},
  volume = {1},
  number = {1-2},
  pages = {166-184}
}

@inproceedings{DBLP:conf/vmcai/Bradley11,
  author = {Aaron R. Bradley},
  title = {SAT-Based Model Checking without Unrolling},
  booktitle = {VMCAI},
  publisher = {Springer},
  year = {2011},
  volume = {6538},
  pages = {70-87}
}

@techreport{Brady:EECS-2008-136,
  author = {Brady, Bryan and Bryant, Randal and Seshia, Sanjit A.},
  title = {Abstracting RTL Designs to the Term Level},
  year = {2008},
  number = {UCB/EECS-2008-136},
  url = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-136.html}
}

@phdthesis{braunstein_phd07,
  author = {C.~Braunstein},
  title = {"Conception Incrémentale, Vérification de Composants Matériels et Méthode d'abstraction pour la Vérification de Systèmes Intégrés sur Puce"},
  school = {Universitée Pierre et Marie Curie (Paris 6)},
  year = {2007}
}

@techreport{cecile03dea,
  author = {C.~Braunstein},
  title = {Transformation de propriétés CTL lors d'une méthode de conception incrémentale des wrappers VCI/PI},
  year = {2003}
}

@article{braunstein06sttt,
  author = {C.~Braunstein and E.~Encrenaz},
  title = {CTL-property Transformations along an Incremental Design Process},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  publisher = {Springer},
  year = {2007},
  volume = {9},
  number = {1},
  pages = {77--88},
  note = {A long version including the proof is available at www-asim.lip6.fr/~cecile}
}

@inproceedings{braunstein07acsd,
  author = {C.~Braunstein and E.~Encrenaz},
  title = {Using CTL formulae as Component Abstraction in a Design and Verification Flow},
  booktitle = {ACSD'07: Proceedings of the 7th International Conference on Application of Concurrency to System Design},
  year = {2007},
  note = {accepted}
}

@inproceedings{braunstein06lpar,
  author = {C.~Braunstein and E.~Encrenaz},
  title = {A Further Step in the Incremental Design Process: Incorporation of an Increment Specification},
  booktitle = {LPAR'06: Proceeding of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
  year = {2006},
  note = {it short paper, proceedings online http://www.lix.polytechnique.fr/~hermann/LPAR2006/}
}

@techreport{Braunstein_Encrenaz_RR_LIP6_07_2006,
  author = {C.~Braunstein and E.~Encrenaz},
  title = {Using CTL formulae as component abstraction},
  year = {2006}
}

@inproceedings{pipeline06,
  author = {C.~Braunstein and E.~Encrenaz},
  title = {Formalizing the Incremental Design and Verification Process of a Pipelined Protocol Converter},
  booktitle = {RSP '06: Proceedings of the Seventeenth IEEE International Workshop on Rapid System Prototyping (RSP'06)},
  publisher = {IEEE Computer Society},
  year = {2006},
  pages = {103--109},
  doi = {http://dx.doi.org/10.1109/RSP.2006.19}
}

@article{avocs_incr,
  author = {C.~Braunstein and E.~Encrenaz},
  title = {CTL-Property Transformations along an Incremental Design Process},
  journal = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
  year = {2005},
  volume = {128},
  number = {6},
  pages = {263--278}
}

@article{browneclarkegrum88,
  author = {M.C.~Browne and E.M.~Clarke and O.~Grumberg},
  title = {Characterizing Finite Kripke Structures in Propositional Temporal Logic},
  journal = {Theoritical Computer Science},
  publisher = {Elsevier Science Publishers Ltd.},
  year = {1988},
  volume = {59},
  number = {1-2},
  pages = {115--131},
  doi = {http://dx.doi.org/10.1016/0304-3975(88)90098-9}
}

@inproceedings{bruns00generalized,
  author = {G.~Bruns and P.~Godefroid},
  title = {Generalized Model Checking: Reasoning about Partial State Spaces},
  booktitle = {CONCUR'2000: Proceedings of the 11th International Conference on Concurrency Theory},
  publisher = {Springer},
  year = {2000},
  volume = {1877},
  pages = {168-182}
}

@inproceedings{burns99partial,
  author = {G.~Bruns and P.~Godefroid},
  title = {Model Checking Partial State Spaces with 3-Valued Temporal Logics},
  booktitle = {CAV'99: Proceedings of the 11th conference on Computer Aided Verification},
  publisher = {Springer},
  year = {1999},
  volume = {1633},
  pages = {274-287}
}

@article{Bryant86,
  author = {R.E.~Bryant},
  title = {Graph-Based Algorithms for Boolean Function Manipulation},
  journal = {IEEE Transactions on Computers},
  year = {1986},
  volume = {35},
  number = {8},
  pages = {677-691}
}

@inproceedings{bunker:idpt02,
  author = {A.~Bunker and G.~Gopalakrishnan},
  title = {Verifying a VCI Bus Interface Model Using an LSC-based Specification},
  booktitle = {Proceedings of the Sixth Biennial World Conference on Integrated Design and Process Technology},
  year = {2002},
  pages = {48},
  url = {http://www.engineering.usu.edu/ece/faculty/bunker/pubs/idpt02.pdf}
}

@article{macmillan,
  author = {J.R.~Burch and E.M.~Clarke and K.L.~McMillan and D.L.~Dill and L.J.~Hwang},
  title = {Symbolic Model Checking: $10^20$ States and Beyond},
  journal = {Information and Computation },
  publisher = {Academic Press, Inc.},
  year = {1992},
  volume = {98},
  number = {2},
  pages = {142--170},
  note = {Special issue for best papers from LICS'90}
}

@inproceedings{burch94automatic,
  author = {J.R.~Burch and D.L.~Dill},
  title = {Automatic Verification of Pipelined Microprocessors Control},
  booktitle = {Proceedings of the sixth International Conference on Computer-Aided Verification CAV'94},
  publisher = {Springer-Verlag},
  year = {1994},
  volume = {LNCS 818},
  pages = {68--80},
  url = {citeseer.ist.psu.edu/burch94automatic.html}
}

@article{bryant82,
  author = {J.R.~Burch and D.L.~Dill},
  title = {Graph-Based Algorithms for Boolean Function Manipulation},
  journal = {IEEE Transactions on Computers},
  year = {1982},
  volume = {35},
  number = {8},
  pages = {677--691}
}

@inproceedings{Buttner05isformal,
  author = {W. Büttner},
  title = {Is Formal Verification Bound to Remain a Junior Partner of Simulation?},
  booktitle = {CHARME'2005: Proceedings of the Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference},
  publisher = {Springer},
  year = {2005},
  volume = {3725},
  pages = {1}
}

@inproceedings{Cabodi09Speeding,
  author = {G. Cabodi and P. Camurati and L. Garcia and M. Murciano and S. Nocco and S. Quer},
  title = {Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints},
  booktitle = {DATE '09: Proceedings of the conference on Design, Automation and Test in Europe},
  year = {2009},
  pages = {1686-1691}
}

@incollection{Cansell2001AbstractionandRefinementofFeatures,
  author = {D.~Cansell and D.~Méry},
  title = {Abstraction and Refinement of Features},
  booktitle = {Language Constructs for Designing Features},
  publisher = {Springer-Verlag},
  year = {2001},
  pages = {65--84}
}

@incollection{cassez-proving,
  author = {F.~Cassez and M.~Ryan and P-Y.~Schobbens},
  title = {Proving Feature Non-Interaction with Alternating-Time Temporal Logic},
  booktitle = {Language Constructs for Describing Features},
  publisher = {Springer Verlag},
  year = {2001},
  pages = {85--104}
}

@inproceedings{DBLP:conf/fmcad/ChauhanCKSVW02,
  author = {P.~Chauhan and E.M.~Clarke and J.H.~Kukula and S.~Sapra and H.~Veith and D.~Wang},
  title = {Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis},
  booktitle = {FMCAD'02: Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design },
  publisher = {Springer},
  year = {2002},
  volume = {2517},
  pages = {33-51}
}

@article{chechik03multi,
  author = {M.~Chechik and B.~Devereux and S.~M.~Easterbrook and A.~Gurfinkel},
  title = {Multi-Valued Symbolic Model-Checking},
  journal = {ACM Transactions on Software Engineering and Methodology},
  year = {2003},
  volume = {12},
  number = {4},
  pages = {371-408}
}

@inproceedings{chechik05framework,
  author = {Marsha Chechik and Arie Gurfinkel},
  title = {A Framework for Counterexample Generation and Exploration.},
  booktitle = {FASE},
  publisher = {Springer},
  year = {2005},
  volume = {3442},
  pages = {220-236}
}

@inproceedings{ChocklerKV01,
  author = {H.~Chockler and O.~Kupferman and M.Y.~Vardi},
  title = {Coverage Metrics for Temporal Logic Model Checking},
  booktitle = {TACAS'01: 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  publisher = {Springer},
  year = {2001},
  volume = {2031},
  pages = {528-542}
}

@inproceedings{846816,
  author = {Hoon Choi and Myung-Kyoon Yim and Jae-Young Lee and Byeong-Whee Yun and Yun-Tae Lee},
  title = {Formal Verification of an Industrial System-on-a-Chip},
  booktitle = {ICCD '00: Proceedings of the 2000 IEEE International Conference on Computer Design},
  publisher = {IEEE Computer Society},
  year = {2000},
  pages = {453}
}

@inproceedings{CLS00,
  author = {G. Ciardo and G. Lüttgen and R. Siminiceanu},
  title = {Efficient Symbolic State-Space Construction for Asynchronous Systems},
  booktitle = {Proc. of ICATPN'2000},
  publisher = {Springer Verlag},
  year = {2000},
  volume = {1825},
  pages = {103--122}
}

@article{cimatti00nusmv,
  author = {A.~Cimatti and E.M.~Clarke and F.~Giunchiglia and M.~Roveri},
  title = {NUSMV: A New Symbolic Model Checker.},
  journal = {STTT},
  year = {2000},
  volume = {2},
  number = {4},
  pages = {410-425}
}

@inproceedings{DBLP:conf/fmcad/CimattiDJR09,
  author = {Alessandro Cimatti and Jori Dubrovin and Tommi A. Junttila and Marco Roveri},
  title = {Structure-aware computation of predicate abstraction},
  booktitle = {FMCAD},
  publisher = {IEEE},
  year = {2009},
  pages = {9-16}
}

@article{DBLP:journals/tocl/CimattiGS10,
  author = {Alessandro Cimatti and Alberto Griggio and Roberto Sebastiani},
  title = {Efficient generation of craig interpolants in satisfiability modulo theories},
  journal = {ACM Trans. Comput. Log.},
  year = {2010},
  volume = {12},
  number = {1},
  pages = {7}
}

@inproceedings{DBLP:conf/sfm/ClaessenR06,
  author = {Koen Claessen and Jan-Willem Roorda},
  title = {An Introduction to Symbolic Trajectory Evaluation},
  booktitle = {SFM},
  publisher = {Springer},
  year = {2006},
  volume = {3965},
  pages = {56-77}
}

@inproceedings{clarke03cegar,
  author = {E.M.~Clarke},
  title = {Counterexample-Guided Abstraction Refinement},
  booktitle = {TIME},
  publisher = {IEEE Computer Society},
  year = {2003},
  pages = {7}
}

@inproceedings{clarkeE81design,
  author = {E.M.~Clarke and E.A.~Emerson},
  title = {Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic.},
  booktitle = {Logic of Programs},
  publisher = {Springer},
  year = {1981},
  volume = {131},
  pages = {52-71}
}

@article{Clarke1986,
  author = {E.M.~Clarke and E.A.~Emerson and A.P.~Sistla},
  title = {Automatic verification of finite-state concurrent systems using temporal logic specifications},
  booktitle = {ICATPN'02: Proceedings of the 23rd International Conference on Applications and Theory of Petri Nets},
  journal = {ACM Transactions on Programming Languages and Systems},
  publisher = {ACM Press},
  year = {1986},
  volume = {8},
  number = {2},
  pages = {244--263},
  doi = {http://doi.acm.org/10.1145/5397.5399}
}

@article{clarke94model,
  author = {E.M.~Clarke and O.~Grumberg and D.E.~Long},
  title = {Model Checking and Abstraction},
  journal = {ACM Transactions on Programming Languages and Systems},
  publisher = {ACM Press},
  year = {1994},
  volume = {16},
  number = {5},
  pages = {1512--1542},
  doi = {http://doi.acm.org/10.1145/186025.186051}
}

@book{clarke99model,
  author = {E.M.~Clarke and O.~Grumberg and D.A.~Peled},
  title = {Model Checking},
  publisher = {The MIT Press},
  year = {1999}
}

@inproceedings{ClarkeGJLV00,
  author = {E.M.~Clarke and O.Grumberg and S.~Jha and Y.~Lu and H.~Veith},
  title = {Counterexample-Guided Abstraction Refinement.},
  booktitle = {CAV'00: Proceedings of the 12th International Conference on Computer Aided Verification},
  publisher = {Springer},
  year = {2000},
  volume = {1855},
  pages = {154-169}
}

@article{Clarke03cegarsymbolic,
  author = {E.~M. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith},
  title = {Counterexample-guided bstraction refinement for symbolic model checking.},
  journal = {Journal of the ACM},
  year = {2003},
  volume = {50},
  number = {5},
  pages = {752-794}
}

@inproceedings{DBLP:conf/dac/ClarkeGMZ95,
  author = {Edmund M. Clarke and Orna Grumberg and Kenneth L. McMillan and Xudong Zhao},
  title = {Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking},
  booktitle = {DAC},
  year = {1995},
  pages = {427-432}
}

@article{DBLP:journals/tcad/ClarkeGS04,
  author = {Edmund M. Clarke and Anubhav Gupta and Ofer Strichman},
  title = {SAT-based counterexample-guided abstraction refinement},
  journal = {IEEE Trans. on CAD of Integrated Circuits and Systems},
  year = {2004},
  volume = {23},
  number = {7},
  pages = {1113-1123}
}

@inproceedings{DBLP:conf/birthday/ClarkeKV10,
  author = {Edmund M. Clarke and Robert P. Kurshan and Helmut Veith},
  title = {The Localization Reduction and Counterexample-Guided Abstraction Refinement},
  booktitle = {Essays in Memory of Amir Pnueli},
  publisher = {Springer},
  year = {2010},
  volume = {6200},
  pages = {61-71}
}

@inproceedings{DBLP:conf/lics/ClarkeLM89,
  author = {E.~M.~Clarke and D.~E.~Long and K.~L.~McMillan},
  title = {Compositional Model Checking},
  booktitle = {LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer Science},
  publisher = {IEEE Computer Society},
  year = {1989},
  pages = {353-362}
}

@inproceedings{DBLP:conf/sat/ClarkeTVW03,
  author = {Edmund M. Clarke and Muralidhar Talupur and Helmut Veith and Dong Wang},
  title = {SAT Based Predicate Abstraction for Hardware Verification},
  booktitle = {SAT},
  publisher = {Springer},
  year = {2003},
  volume = {2919},
  pages = {78-92}
}

@misc{tata97,
  author = {H. Comon and M. Dauchet and R. Gilleron and F. Jacquemard and D. Lugiez and S. Tison and M. Tommasi},
  title = {Tree Automata Techniques and Applications},
  year = {1997},
  note = {release October, 1rst 2002}
}

@inproceedings{madre,
  author = {O.~Coudert and J.-C.~Madre},
  title = {A New Method to Compute Prime and Essential Prime Implicants of Boolean Functions},
  booktitle = {Advanced Research in VLSI and Parallel Systems},
  year = {1992},
  pages = {113--128}
}

@inproceedings{DBLP:conf/popl/CousotC77,
  author = {P.~Cousot and R.~Cousot},
  title = {Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.},
  booktitle = {POPL'77: Proceedings of the 14th Annual ACM Symposium on Principles of Programming Languages},
  year = {1977},
  pages = {238-252}
}

@inproceedings{jmc-ag-djs:ddd,
  author = {J.M.~Couvreur and A.~Griffault and D.J.~Sherman},
  title = {Diagrammes de décision pour la vérification de réseaux à files},
  booktitle = {Modélisation de systèmes réactifs (MSR'99)},
  year = {1999}
}

@inproceedings{CA94,
  author = {J.M. Couvreur and E. Paviot-Adet},
  title = {New Structural Invariants for Petri Nets Analysis},
  booktitle = {Proc. of ICATPN'94},
  publisher = {Springer Verlag},
  year = {1994},
  volume = {815},
  pages = {199--218}
}

@inproceedings{CouvreurEPPW02,
  author = {J-M.~Couvreur and E.~Encrenaz and E.~Paviot-Adet and D.~Poitrenaud and P-A.~Wacrenier},
  title = {Data Decision Diagrams for Petri Net Analysis.},
  booktitle = {ICATPN'02: Proceedings of the 23rd International Conference on Applications and Theory of Petri Nets},
  publisher = {Springer},
  year = {2002},
  volume = {2360},
  pages = {101-120}
}

@inproceedings{couvreur05hierarchie,
  author = {J-M.~Couvreur and Y.~Thierry-Mieg},
  title = {Hierarchical Decision Diagrams to Exploit Model Structure.},
  booktitle = {FORTE : Proceedings of the 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems},
  publisher = {Springer},
  year = {2005},
  volume = {3731},
  pages = {443-457}
}

@article{dams97abstract,
  author = {D.~Dams and R.~Gerth and O.~Grumberg},
  title = {Abstract interpretation of reactive systems},
  journal = {ACM Transactions on Programming Languages and Systems},
  publisher = {ACM Press},
  year = {1997},
  volume = {19},
  number = {2},
  pages = {253--291},
  doi = {http://doi.acm.org/10.1145/244795.244800}
}

@inproceedings{DBLP:conf/vmcai/DamsN05,
  author = {D.~Dams and K.~S.~Namjoshi},
  title = {Automata as Abstractions.},
  booktitle = {VMCAI'05: Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation},
  publisher = {Springer},
  year = {2005},
  volume = {3385},
  pages = {216-232}
}

@inproceedings{DBLP:conf/lics/DamsN04,
  author = {D.~Dams and K.~S.~Namjoshi},
  title = {The Existence of Finite Abstractions for Branching Time Model Checking.},
  booktitle = {LICS04},
  publisher = {IEEE Computer Society},
  year = {2004},
  pages = {335-344}
}

@inproceedings{Darbari08transient,
  author = {Darbari, A. and Al Hashimi, B. and Harrod, P. and Bradley, D.},
  title = {A New Approach for Transient Fault Injection Using Symbolic Simulation},
  booktitle = {IEEE International Symposium On-line Testing Symposium},
  journal = {On-Line Testing Symposium, 2008. IOLTS '08. 14th IEEE International},
  year = {2008},
  pages = {93-98},
  doi = {http://dx.doi.org/10.1109/IOLTS.2008.59}
}

@misc{duret03dea,
  author = {A.~Duret-Lutz and R.~Rebiha},
  title = {SPOT : Une bibliothèque de vérificaion de propriétés de logique temporelle à temps linéaire},
  year = {2003}
}

@inproceedings{dwyer99patterns,
  author = {M. B. Dwyer and G. S. Avrunin and J. C. Corbett},
  title = {Patterns in Property Specifications for Finite-State Verification.},
  booktitle = {ICSE' 99. Proceedings of the 1999 International Conference on Software Engineering},
  year = {1999},
  pages = {411-420},
  url = {http://patterns.projects.cis.ksu.edu/collaborations/papers.shtml}
}

@inproceedings{DBLP:conf/icse/DwyerHJLPRZV01,
  author = {Matthew B. Dwyer and John Hatcliff and Roby Joehanes and Shawn Laubach and Corina S. Pasareanu and Robby and Hongjun Zheng and Willem Visser},
  title = {Tool-Supported Program Abstraction for Finite-State Verification.},
  booktitle = {ICSE},
  publisher = {IEEE Computer Society},
  year = {2001},
  pages = {177-187}
}

@inproceedings{DBLP:conf/icse/EasterbrookCDGLPTT03,
  author = {S.M.~Easterbrook and M.~Chechik and B.~Devereux and A.~Gurfinkel and A.~Lai and V.~Petrovykh and A.~Tafliovich and C.~Thompson-Walsh},
  title = {$i$Chek: A Model Checker for Multi-Valued Reasoning.},
  booktitle = {ICSE'03: Proceedings of the 25th International Conference on Software Engineering},
  publisher = {IEEE Computer Society},
  year = {2003},
  pages = {804-805}
}

@inproceedings{EasterbrookC01,
  author = {Steve M. Easterbrook and Marsha Chechik},
  title = {A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints.},
  booktitle = {ICSE},
  publisher = {IEEE Computer Society},
  year = {2001},
  pages = {411-420}
}

@inproceedings{emerson82desision,
  author = {E.A.~Emerson and J.Y.~Halpern},
  title = {Decision Procedures and Expressiveness in the Temporal Logic of Branching Time},
  booktitle = {STOC},
  publisher = {ACM},
  year = {1982},
  pages = {169-180}
}

@article{DBLP:journals/tcad/FeySBD08,
  author = {Görschwin Fey and Stefan Staber and Roderick Bloem and Rolf Drechsler},
  title = {Automatic Fault Localization for Property Checking},
  journal = {IEEE Trans. on CAD of Integrated Circuits and Systems},
  year = {2008},
  volume = {27},
  number = {6},
  pages = {1138-1149}
}

@article{fitting91bilattices,
  author = {M.~Fitting},
  title = {Bilattices and the Semantics of Logic Programming.},
  journal = {Journal of Logic Programming},
  year = {1991},
  volume = {11},
  number = {1&2},
  pages = {91-116}
}

@inproceedings{DBLP:conf/date/GanaiGA05,
  author = {Malay K. Ganai and Aarti Gupta and Pranav Ashar},
  title = {Verification of Embedded Memory Systems using Efficient Memory Modeling},
  booktitle = {DATE},
  year = {2005},
  pages = {1096-1101}
}

@inproceedings{godefroid03expressiveness,
  author = {Patrice Godefroid and Radha Jagadeesan},
  title = {On the Expressiveness of 3-Valued Models},
  booktitle = {VMCAI 2003: Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation},
  publisher = {Springer-Verlag},
  year = {2003},
  pages = {206--222}
}

@inproceedings{DBLP:conf/cav/GodefroidJ02,
  author = {P.~Godefroid and R.~Jagadeesan},
  title = {Automatic Abstraction Using Generalized Model Checking.},
  booktitle = {CAV},
  publisher = {Springer},
  year = {2002},
  volume = {2404},
  pages = {137-150}
}

@inproceedings{goelL00formal,
  author = {A.~Goel and W.~R.~Lee},
  title = {Formal Verification of an IBM CoreConnect Processor Local Bus Arbiter Core},
  booktitle = {DAC'00: Proceedings of the 37th Conference on Design Automation},
  year = {2000},
  pages = {196-200}
}

@inproceedings{GrafS97pvs,
  author = {S.~Graf and H.~Sadi},
  title = {Construction of Abstract State Graphs with PVS.},
  booktitle = {CAV},
  publisher = {Springer},
  year = {1997},
  volume = {1254},
  pages = {72-83}
}

@inproceedings{grumberg05abstraction,
  author = {Orna Grumberg},
  title = {Abstraction and Refinement in Model Checking.},
  booktitle = {FMCO'05: 4th International Symposium on Formal Methods for Components and Objects,},
  publisher = {Springer},
  year = {2005},
  volume = {4111},
  pages = {219-242}
}

@inproceedings{GL91,
  author = {O.~Grumberg and D.E.~Long},
  title = {Model Checking and Modular Verification},
  booktitle = {International Conference on Concurrency Theory},
  publisher = {Springer Verlag},
  year = {1991},
  volume = {527},
  pages = {250--263}
}

@article{Gupta92syrvey,
  author = {A.~Gupta},
  title = {Formal Hardware Verification Methods: A Survey.},
  journal = {Formal Methods in System Design},
  year = {1992},
  volume = {1},
  number = {2/3},
  pages = {151-238}
}

@inproceedings{DBLP:conf/sfm/GuptaGW06,
  author = {Aarti Gupta and Malay K. Ganai and Chao Wang},
  title = {SAT-Based Verification Methods and Applications in Hardware Verification},
  booktitle = {SFM},
  publisher = {Springer},
  year = {2006},
  volume = {3965},
  pages = {108-143}
}

@inproceedings{gurfinkelC06waste,
  author = {A.~Gurfinkel and M.~Chechik},
  title = {Why Waste a Perfectly Good Abstraction?.},
  booktitle = {TACAS'06: Proceedings of the 12th international conference on Tools and Algorithms for the Construction and Analysis of Systems},
  publisher = {Springer},
  year = {2006},
  volume = {3920},
  pages = {212-226}
}

@inproceedings{DBLP:conf/vmcai/GurfinkelWC06,
  author = {Arie Gurfinkel and Ou Wei and Marsha Chechik},
  title = {Systematic Construction of Abstractions for Model-Checking},
  booktitle = {VMCAI},
  publisher = {Springer},
  year = {2006},
  volume = {3855},
  pages = {381-397}
}

@inproceedings{GurfinkelWC06,
  author = {Gurfinkel, A. and Wei, O. and Chechik, M.},
  title = {Systematic Construction of Abstractions for Model-Checking.},
  booktitle = {VMCAI'06: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation},
  publisher = {Springer},
  year = {2006},
  volume = {3855},
  pages = {381-397}
}

@inproceedings{henzinger99dsp,
  author = {T.~A.~Henzinger and X.~Liu and S.~Qadeer and S.~K.~Rajamani},
  title = {Formal Specification and Verification of a Dataflow Processor Array.},
  booktitle = {ICCAD'99: Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design},
  year = {1999},
  pages = {494-499}
}

@inproceedings{henzinger00decomposing,
  author = {Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani},
  title = {Decomposing refinement proofs using assume-guarantee reasoning},
  booktitle = {ICCAD '00: Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design},
  publisher = {IEEE Press},
  year = {2000},
  pages = {245--253}
}

@inproceedings{C:HJMS03,
  author = {Henzinger, T.A. and Jhala, R. and Majumdar, R. and Sutre, G.},
  title = {Software Verification with BLAST},
  booktitle = {SPIN'2003: Proceedings of the 10th International SPIN Workshop},
  publisher = {Springer},
  year = {2003},
  volume = {2648},
  pages = {235--239},
  note = {Tool paper},
  url = {http://www.labri.fr/publications/mvtsi/2003/HJMS03}
}

@inproceedings{henzinger98you,
  author = {T.A.~Henzinger and S.~Qadeer and S.K.~Rajamani},
  title = {You Assume, We Guarantee: Methodology and Case Studies},
  booktitle = {CAV'98: Proceedings of the 10th International Conference on Computer Aided Verification},
  publisher = {Springer-Verlag},
  year = {1998},
  volume = {1427},
  pages = {440--451}
}

@article{henzinger02anassume,
  author = {T.A.~Henzinger and S.~Qadeer and S.K.~Rajamani and S.~Tasiran},
  title = {An Assume-Guarantee Rule for Checking Simulation},
  journal = {ACM Transactions on Programming Languages Systems},
  publisher = {ACM Press},
  year = {2002},
  volume = {24},
  number = {1},
  pages = {51--64},
  doi = {http://doi.acm.org/10.1145/509705.509707}
}

@article{Holzmann97e,
  author = {G.J.~Holzmann},
  title = {The Model Checker Spin},
  journal = {IEEE Transactions on Software Engineering},
  year = {1997},
  volume = {23},
  number = {5},
  pages = {279--295},
  note = {Special issue on Formal Methods in Software Practice}
}

@inproceedings{hosabettu98decomposing,
  author = {R.~Hosabettu and M.~Srivas and G.~Gopalakrishnan},
  title = {Decomposing the Proof of Correctness of Pipelined Microprocessors},
  booktitle = {Computer-Aided Verification, CAV'98},
  publisher = {Springer-Verlag},
  year = {1998},
  volume = {1427},
  pages = {122--134},
  url = {citeseer.ist.psu.edu/208243.html}
}

@article{huggins98spec,
  author = {J.K.~Huggins and D.~Van Campenhout},
  title = {Specification and Verification of Pipelining in the ARM2 RISC Microprocessor},
  journal = {ACM Transactions on Design Automation of Electronic Systems},
  publisher = {ACM Press},
  year = {1998},
  volume = {3},
  number = {4},
  pages = {563--580},
  doi = {http://doi.acm.org/10.1145/296333.296345}
}

@article{HWA99,
  author = {H.~Hulgaard and P.~F.~Williams and H.~R.~Andersen},
  title = {Equivalence Checking of Combinational Circuits using Boolean Expression Diagrams},
  journal = {IEEE Transactions of Computer-Aided Design},
  year = {1999},
  volume = {18},
  number = {7},
  pages = {903-917}
}

@inproceedings{JainKSC05,
  author = {Jain, H. and Kroening, D. and Sharygina, N. and Clarke, E.M.},
  title = {Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog.},
  booktitle = {DAC'05: Proceedings of the 42nd Design Automation Conference},
  publisher = {ACM},
  year = {2005},
  pages = {445-450}
}

@article{DBLP:journals/tcad/JainKSC08,
  author = {H.~Jain and D.~Kroening and N.~Sharygina and E.M.~Clarke},
  title = {Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog},
  journal = {IEEE Transaction on CAD of Integrated Circuits and Systems},
  year = {2008},
  volume = {27},
  number = {2},
  pages = {366-379}
}

@inproceedings{kroening07vcegar,
  author = {H.~Jain and D.~Kroening and N.~Sharygina and E.~Clarke},
  title = {VCEGAR: Verilog CounterExample Guided Abstraction Refinement},
  booktitle = {TACAS'07: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  year = {2007},
  note = {Accepted paper}
}

@inproceedings{JainNFS97survey,
  author = {J.~Jain and A.~Narayan and M.~Fujita and A.L.~Sangiovanni-Vincentelli},
  title = {A Survey of Techniques for Formal Verification of Combinational Circuits.},
  booktitle = {ICCD},
  year = {1997},
  pages = {445-454}
}

@inproceedings{jhala01microarchi,
  author = {Jhala, R. and McMillan, K.L.},
  title = {Microarchitecture Verification by Compositional Model Checking.},
  booktitle = {CAV'01: Proceedings of the 13th International Conference on Computer Aided Verification},
  publisher = {Springer},
  year = {2001},
  volume = {2102},
  pages = {396-410}
}

@inproceedings{Somenzi04Circuscav,
  author = {HoonSang Jin and Mohammad Awedh and Fabio Somenzi},
  title = {CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking},
  booktitle = {CAV'04: Proceedings of the 16th International Conference onComputer Aided Verification },
  publisher = {Springer},
  year = {2004},
  volume = {3114},
  pages = {519-522}
}

@inproceedings{DBLP:conf/tacas/JinHS05,
  author = {HoonSang Jin and HyoJung Han and Fabio Somenzi},
  title = {Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit},
  booktitle = {TACAS'05: Proceedings of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  publisher = {Springer},
  year = {2005},
  volume = {3440},
  pages = {287-300}
}

@inproceedings{somenzi04Circus,
  author = {H*.~Jin and F.~Somenzi},
  title = {CirCUs: A Hybrid Satisfiability Solver},
  booktitle = {SAT'04: The 7th International Conference on Theory and Applications of Satisfiability Testing},
  year = {2004}
}

@article{kalushy93knowledge,
  author = {Yuri Kaluzhny and Alexei Yu. Muravitsky},
  title = {A knowledge representation based on the Belnap's four-valued logic},
  journal = {Journal of Applied Non-Classical Logics},
  year = {1993},
  volume = {3},
  number = {2},
  pages = {189-203}
}

@inproceedings{park03satunbounded,
  author = {H.-J.~Kang and I.-C.~Park},
  title = {SAT-based Unbounded Symbolic Model Checking},
  booktitle = {DAC'03: Proceedings of the 40th conference on Design automation},
  publisher = {ACM},
  year = {2003},
  pages = {840--843},
  doi = {http://doi.acm.org/10.1145/775832.776043}
}

@article{Kern99survey,
  author = {C.~Kern and M.R.~Greenstreet},
  title = {Formal Verification in Hardware Design: a Survey},
  journal = {ACM Transactions on Design Automation of Electronic Systems},
  publisher = {ACM Press},
  year = {1999},
  volume = {4},
  number = {2},
  pages = {123--193},
  doi = {http://doi.acm.org/10.1145/307988.307989}
}

@book{kleene52introduction,
  author = {Kleene, S.},
  title = {Introduction to Metamathematics},
  publisher = {North-Holland},
  year = {1952}
}

@inproceedings{KLM93,
  author = {T. Kolks and B. Lin and H. De Man},
  title = {Sizing and Verification of Communication Buffers for Communicating Processes},
  booktitle = {Proc. of IEEE International Conference on Computer-Aided Design},
  year = {1993},
  volume = {1825},
  pages = {660--664}
}

@inproceedings{kroening01automated,
  author = {D.~Kroening and W.J.~Paul},
  title = {Automated Pipeline Design},
  booktitle = {DAC '01: Proceedings of the 38th conference on Design Automation},
  publisher = {ACM Press},
  year = {2001},
  pages = {810--815},
  doi = {http://doi.acm.org/10.1145/378239.379071}
}

@book{kropf99introduction,
  author = {T.~Kropf},
  title = {Introduction to Formal Hardware Verification},
  publisher = {Springer Verlag},
  year = {1999}
}

@article{KupfermanG96branching,
  author = {O.~Kupferman and O.~Grumberg},
  title = {Branching-Time Temporal Logic and Tree Automata.},
  journal = {Information and Computation},
  year = {1996},
  volume = {125},
  number = {1},
  pages = {62-69}
}

@article{KupfermanVW00automata,
  author = {O.~Kupferman and M.Y.~Vardi and P.~Wolper},
  title = {An Automata-Theoretic Approach to Branching-Time Model Checking.},
  journal = {Journal of the ACM},
  year = {2000},
  volume = {47},
  number = {2},
  pages = {312-360}
}

@inproceedings{lamp83,
  author = {L.~Lamport},
  title = {Information Processing},
  booktitle = {What good is in temporal logic},
  publisher = {Elsevier},
  year = {1983},
  pages = {657--668}
}

@book{Lano,
  author = {K.~Lano},
  title = {The B Language and Method, A Guide to Practical Formal Development},
  publisher = {Springer-Verlag},
  year = {1996}
}

@inproceedings{693769,
  author = {K.G~Larsen and B.~Steffen and C.~Weise},
  title = {A Constraint Oriented Proof Methodology Based on Modal Transition Systems},
  booktitle = {TACAS '95: Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems},
  publisher = {Springer-Verlag},
  year = {1995},
  pages = {17--40}
}

@inproceedings{larsen88modal,
  author = {K.~G.~Larsen and B.~Thomsen},
  title = {A Modal Process Logic},
  booktitle = {Third Annual Symposium on Logic in Computer Science},
  publisher = {IEEE Computer Society},
  year = {1988},
  pages = {203-210}
}

@article{LiWS05PureSat,
  author = {B.~Li and C.~Wang and F.~Somenzi},
  title = {Abstraction Refinement in Symbolic Model Checking using Satisfiability as the Only Decision Procedure},
  journal = {STTT},
  year = {2005},
  volume = {7},
  number = {2},
  pages = {143-155}
}

@inproceedings{lin91implicit,
  author = {B.~Lin and A.R.~Newton},
  title = {Implicit Manipulation of Equivalence Classes Using Binary Decision Diagrams},
  booktitle = {ICCD '91: Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors},
  publisher = {IEEE Computer Society},
  year = {1991},
  pages = {81--85}
}

@article{Loiseaux,
  author = {C.~Loiseaux and S.~Graf and J.~Sifakis and A.~Bouajjani and S.~Bensalem},
  title = {Property Preserving Abstractions for the Verification of Concurrent Systems},
  journal = {Formal Methods in System Design},
  publisher = {Kluwer Academic Publisher},
  year = {1995},
  volume = {6},
  number = {1},
  pages = {11--44}
}

@phdthesis{long93thesis,
  author = {D.~E.~Long},
  title = {Model Checking, Abstraction, and Compositional Verification},
  school = {Carnegie Mellon University},
  year = {1993}
}

@inproceedings{santo,
  author = {S.~Malik and A.R.~Wang and R.K~Brayton and A.~Sangiovanni-Vincentelli},
  title = {Logic Verification using Binary Decision Diagrams in Logic Synthesis Environment},
  booktitle = {Proceedings of the IEEE International Conference on Computer Aided Design, ICCAD'88},
  year = {1988},
  pages = {6--9},
  note = {Santa Clara CA, USA}
}

@inproceedings{manolios00correctness,
  author = {P.~Manolios},
  title = {Correctness of Pipelined Machines},
  booktitle = {FMCAD '00: Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design},
  publisher = {Springer-Verlag},
  year = {2000},
  pages = {161--178},
  url = {citeseer.ist.psu.edu/426677.html}
}

@inproceedings{manolios04web,
  author = {P.~Manolios and S.K.~Srinivasan},
  title = {Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements},
  booktitle = {DATE '04: Proceedings of the conference on Design, Automation and Test in Europe},
  publisher = {IEEE Computer Society},
  year = {2004},
  pages = {168-174}
}

@inproceedings{DBLP:conf/iccad/ManoliosSV06,
  author = {Panagiotis Manolios and Sudarshan K. Srinivasan and Daron Vroon},
  title = {Automatic memory reductions for RTL model verification},
  booktitle = {ICCAD},
  publisher = {ACM},
  year = {2006},
  pages = {786-793}
}

@inproceedings{Mariano2002formalization,
  author = {G.~Mariano and J-L.~Boulanger and A. Aljer},
  title = {Formalization of Digital Circuits Using the B Method},
  booktitle = {CompRail VIII: 8th International Conference on Computer Aided Design, Manufacture and Operation in the Railway and other Advanced Mass Transit Systems},
  year = {2002},
  url = {http://www.wessex.ac.uk/conferences/2002/cr02/}
}

@inproceedings{Silva00Sat,
  author = {Marques-Silva, Jo ao P. and Sakallah, Karem A.},
  title = {Boolean satisfiability in electronic design automation},
  booktitle = {DAC '00: Proceedings of the 37th Annual Design Automation Conference},
  publisher = {ACM},
  year = {2000},
  pages = {675--680},
  doi = {http://doi.acm.org/10.1145/337292.337611}
}

@inproceedings{mcmillan98tomasulo,
  author = {K.L.~McMillan},
  title = {Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking.},
  booktitle = {CAV'98: Proceddings of the 10th International Conference on Computer Aided Verification},
  publisher = {Springer},
  year = {1998},
  volume = {1427},
  pages = {110-121}
}

@article{mcmillan00methodology,
  author = {K.L. McMillan},
  title = {A Methodology for Hardware Verification Using Compositional Model Checking},
  journal = {Science of Computer Programming},
  year = {2000},
  volume = {37},
  number = {1--3},
  pages = {279--309},
  url = {citeseer.ist.psu.edu/mcmillan99methodology.html}
}

@book{mcmillanSMV,
  author = {K.L.~McMillan},
  title = {Symbolic Model Checking},
  publisher = {Kluwer Academics Publishers},
  year = {1993}
}

@inproceedings{mcmillan02applyingSat,
  author = {Kenneth L. McMillan},
  title = {Applying SAT Methods in Unbounded Symbolic Model Checking},
  booktitle = {CAV'02: Proceedings of the 14th International Conference on Computer Aided vVrification},
  publisher = {Springer},
  year = {2002},
  volume = {2404},
  pages = {250-264}
}

@inproceedings{DBLP:conf/cav/McMillan97,
  author = {Kenneth L. McMillan},
  title = {A Compositional Rule for Hardware Design Refinement.},
  booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification},
  publisher = {Springer},
  year = {1997},
  volume = {1254},
  pages = {24-35}
}

@phdthesis{memmi:thesis,
  author = {G.~Memmi},
  title = {Méthodes d'analyse des réseaux de Petri, réseaux à files et application aux systèmes temps-réel},
  school = {Université Paris-6},
  year = {1983}
}

@book{Mil89,
  author = {R.~Milner},
  title = {Communication and Concurrency},
  publisher = {Prentice Hall},
  year = {1989}
}

@inproceedings{DBLP:conf/ijcai/Milner71,
  author = {R.~Milner},
  title = {An Algebraic Definition of Simulation Between
 Programs.},
  booktitle = {IJCAI'71: Proceedings of the 2nd International Joint Conference on Artificial Intelligence},
  year = {1971},
  pages = {481-489}
}

@inproceedings{minato,
  author = {S.~Minato and N.~Ishiura and S.~Yajima},
  title = {Shared Binary Decision Diagrams with Attributed Edges for Efficient Boolean Function Manipulation},
  booktitle = {Proceedings of the 27th ACM/IEEE Design Automation Conference, DAC'90},
  year = {1990},
  pages = {52--57}
}

@inproceedings{MC99,
  author = {A.S. Miner and G. Ciardo},
  title = {Efficient Reachability Set Generation and Storage Using Decision Diagrams},
  booktitle = {Proc. of ICATPN'99},
  publisher = {Springer Verlag},
  year = {1999},
  volume = {1639},
  pages = {6--25}
}

@article{Miskov-ZivanovM06,
  author = {N.~Miskov-Zivanov and D.~Marculescu},
  title = {Circuit Reliability Analysis Using Symbolic Techniques},
  journal = {IEEE Transaction on CAD of Integrated Circuits and Systems},
  year = {2006},
  volume = {25},
  number = {12},
  pages = {2638-2649}
}

@article{mooremachine,
  author = {E.F.~Moore},
  title = {Gedanken-experiments on Sequential Machines},
  journal = {Automata Studies, Annals of Mathematical Studies},
  year = {1956},
  volume = {34},
  pages = {129 – 153}
}

@inproceedings{Morin-AlloryB06,
  author = {K.~Morin-Allory and D.~Borrione},
  title = {Proven Correct Monitors from PSL Specifications.},
  booktitle = {DATE'06: Proceedings of the Conference on Design, Automation and Test in Europe},
  publisher = {European Design and Automation Association, Leuven, Belgium},
  year = {2006},
  pages = {1246-1251}
}

@inproceedings{DBLP:conf/dac/MoskewiczMZZM01,
  author = {M.W.~Moskewicz and C.F.~Madigan and Y.~Zhao and L.~Zhang and S.~Malik},
  title = {Chaff: Engineering an Efficient SAT Solver},
  booktitle = {DAC'01: Proceedings of the 38th Design Automation Conference},
  publisher = {ACM},
  year = {2001},
  pages = {530-535}
}

@article{DBLP:journals/tc/MoundanosAH98,
  author = {D.~Moundanos and J.A.~Abraham and Y.V.~Hoskote},
  title = {Abstraction Techniques for Validation Coverage Analysis and Test Generation},
  journal = {IEEE Trans. Computers},
  year = {1998},
  volume = {47},
  number = {1},
  pages = {2-14}
}

@inproceedings{DBLP:conf/sbmf/MouraB09,
  author = {Leonardo Mendonça de Moura and Nikolaj Bjørner},
  title = {Satisfiability Modulo Theories: An Appetizer},
  booktitle = {SBMF},
  publisher = {Springer},
  year = {2009},
  volume = {5902},
  pages = {23-36}
}

@inproceedings{DBLP:conf/tacas/MouraB08,
  author = {Leonardo Mendonça de Moura and Nikolaj Bjørner},
  title = {Z3: An Efficient SMT Solver},
  booktitle = {TACAS},
  publisher = {Springer},
  year = {2008},
  volume = {4963},
  pages = {337-340}
}

@article{moy06lussy,
  author = {M.~Moy and F.~Maraninchi and L.~Maillet},
  title = {LusSy: An open tool for the analysis of systems-on-a-chip at the transaction level},
  journal = {Design Automation for Embedded Systems},
  year = {2006},
  volume = {10},
  number = {2-3},
  pages = {73--104},
  doi = {http://dx.doi.org/10.1007/s10617-006-9044-6}
}

@article{namjoshi97simple,
  author = {K.S.~Namjoshi},
  title = {A Simple Characterization of Stuttering Bisimulation},
  journal = {LNCS, Proceedings of the 17th Conference on Foundations of Software Technology an Theoretical Computer Science},
  year = {1997},
  volume = {1346},
  pages = {284--296},
  url = {citeseer.ist.psu.edu/namjoshi97simple.html}
}

@inproceedings{DBLP:conf/cav/Namjoshi03,
  author = {Kedar S. Namjoshi},
  title = {Abstraction for Branching Time Properties.},
  booktitle = {CAV},
  publisher = {Springer},
  year = {2003},
  volume = {2725},
  pages = {288-300}
}

@inproceedings{namjoshiK00syntactic,
  author = {K.~S.~Namjoshi and R.~P.~Kurshan},
  title = {Syntactic Program Transformations for Automatic Abstraction},
  booktitle = {Proceedings of the 12th International Conference on Computer Aided Verification},
  publisher = {Springer-Verlag},
  year = {2000},
  volume = {1855},
  pages = {435--449}
}

@inproceedings{DBLP:conf/date/NanshiS08,
  author = {K.~Nanshi and F.~Somenzi},
  title = {Improved Visibility in One-to-Many Trace Concretization},
  booktitle = {DATE},
  year = {2008},
  pages = {819-824}
}

@inproceedings{DBLP:conf/dac/NanshiS06,
  author = {K.~Nanshi and F.~Somenzi},
  title = {Guiding simulation with increasingly refined abstract traces},
  booktitle = {DAC},
  publisher = {ACM},
  year = {2006},
  pages = {737-742}
}

@inproceedings{nejati05stutering,
  author = {Shiva Nejati and Arie Gurfinkel and Marsha Chechik},
  title = {Stuttering Abstraction for Model Checking},
  booktitle = {SEFM},
  publisher = {IEEE Computer Society},
  year = {2005},
  pages = {311-320}
}

@article{nicolaV95,
  author = {R.~De~Nicola and F.W.~Vaandrager},
  title = {Three Logics for Branching Bisimulation.},
  journal = {Journal of the ACM},
  year = {1995},
  volume = {42},
  number = {2},
  pages = {458-487}
}

@manual{VCI_spec,
  author = {On-Chip Bus Development Working Group},
  title = {Virtual Component Interface Standard (VCI).},
  year = {2000},
  volume = {version 2}
}

@manual{PI_proto,
  author = {Open Microprocessors System Initiatives},
  title = {OMI324: PI-Bus Standard Specification},
  year = {1994}
}

@techreport{specamba03,
  author = {J.~Ossima Khéba},
  title = {Spécification des Wrappers AHB/VCI},
  school = {Universitée Pierre et Marie Curie},
  year = {2003}
}

@techreport{joel02,
  author = {J.~Ossima Khéba},
  title = {Les Wrappers PI/VCI et Etude de Faisabilité des Wrappers AMBA/VCI},
  school = {Universitée Pierre et Marie Curie},
  year = {2002}
}

@inproceedings{cade92-pvs,
  author = {S. Owre and J. M. Rushby and and N. Shankar},
  title = {PVS: A Prototype Verification System},
  booktitle = {11th International Conference on Automated Deduction (CADE)},
  publisher = {Springer-Verlag},
  year = {1992},
  volume = {607},
  pages = {748--752},
  url = {http://www.csl.sri.com/papers/cade92-pvs/}
}

@inproceedings{DBLP:conf/tcs/Park81,
  author = {D.~Park},
  title = {Concurrency and Automata on Infinite Sequences.},
  booktitle = {Proceedings of the 5th GI-Conference on Theoretical Computer Science},
  publisher = {Springer},
  year = {1981},
  volume = {104},
  pages = {167-183}
}

@inproceedings{pasareanu99assume,
  author = {C.S.~Pasareanu and M.B.~Dwyer and M.~Huth},
  title = {Assume-Guarantee Model Checking of Software: A Comparative Case Study},
  booktitle = {Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking},
  publisher = {Springer-Verlag},
  year = {1999},
  pages = {168--183}
}

@inproceedings{passerone02convertibility,
  author = {R.~Passerone and L.~de Alfaro and T.A.~Henzinger and A.L.~Sangiovanni-Vincentelli},
  title = {Convertibility Verification and Converter Synthesis: Two Faces of The Same Coin},
  booktitle = {ICCAD '02: Proceedings of the 2002 IEEE/ACM International Conference on Computer-Aided Design},
  publisher = {ACM Press},
  year = {2002},
  pages = {132--139},
  doi = {http://doi.acm.org/10.1145/774572.774592}
}

@inproceedings{DBLP:conf/dac/PasseroneRS98,
  author = {R.~Passerone and J.A.~Rowson and A.L.~Sangiovanni-Vincentelli},
  title = {Automatic Synthesis of Interfaces Between
 Incompatible Protocols.},
  booktitle = {DAC'98: Proceedings of the 35th Conference on Design Automation},
  year = {1998},
  pages = {8-13}
}

@inproceedings{PRCB94,
  author = {E. Pastor and O. Roig and J. Cortadella and R.M. Badia},
  title = {Petri Net analysis using Boolean manipulation},
  booktitle = {Proc. of ICATPN'94},
  publisher = {Springer Verlag},
  year = {1994},
  volume = {815},
  pages = {416--435}
}

@book{hennessypattersonbook,
  author = {D.A.~Patterson and J.L~Hennessy},
  title = {Computer Organization and Design: The Hardware/Software Interface, Third Edition (The Morgan Kaufmann Series in Computer Architecture and Design) (The ... Series in Computer Architecture and Design)},
  publisher = {Morgan Kaufmann},
  year = {2004},
  edition = {third},
  url = {http://www.amazon.co.uk/exec/obidos/ASIN/1558606041/citeulike-21}
}

@phdthesis{peng02thesis,
  author = {H.~Peng},
  title = {Improving Compositional Verification through Environment Synthesis and Syntactic Model Reduction},
  school = {Dept. of Electrical and Computer Engenering, Concordia University, Montreal, Quebec, Canada},
  year = {2002}
}

@inproceedings{peng02tableau,
  author = {H.~Peng and Y.~Mokhtari and S.~Tahar},
  title = {Environment Synthesis for Compositional Model Checking.},
  booktitle = {ICCD'02: Proceedings of the 20th International Conference on Computer Design},
  publisher = {IEEE Computer Society},
  year = {2002},
  pages = {70-}
}

@article{peng03comparison,
  author = {H.~Peng and S.~Tahar and F.~Khendek},
  title = {Comparison of SPIN and VIS for Protocol Verification.},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  publisher = {Springer},
  year = {2003},
  volume = {4},
  number = {2},
  pages = {234-245}
}

@inproceedings{omi95rsp,
  author = {V. Pevtschin},
  title = {The Open Microprocessor Systems Initiative: A Strategy Towards Integrated System Design},
  booktitle = {RSP'95: Proceddings of the 6th IEEE International Workshop on Rapid System Prototyping},
  year = {1995},
  pages = {2--11},
  doi = {http://doi.ieeecomputersociety.org/10.1109/IWRSP.1995.518564}
}

@inproceedings{plath99sfi,
  author = {M.C.~Plath and M.D.~Ryan},
  title = {SFI: a Feature Integration Tool},
  booktitle = {Tool Support for System Specification, Development and Verification},
  publisher = {Springer},
  year = {1999},
  pages = {201--216}
}

@article{plath01feature,
  author = {M.~Plath and M.~Ryan},
  title = {Feature Integration using a Feature Construct},
  journal = {Science of Computer Programming},
  publisher = {Elsevier North-Holland, Inc.},
  year = {2001},
  volume = {41},
  number = {1},
  pages = {53--84},
  doi = {http://dx.doi.org/10.1016/S0167-6423(00)00018-6}
}

@inproceedings{plath98feature,
  author = {M.C.~Plath and M.D.~Ryan},
  title = {A feature construct for Promela},
  booktitle = {SPIN'98: Proceedings of the 4th SPIN workshop},
  year = {1998},
  url = {citeseer.ist.psu.edu/plath98feature.html}
}

@inproceedings{Purandare09Strengthening,
  author = {M. Purandare and T. Wahl and D. Kroening},
  title = {Strengthening Properties Using on Refinement},
  booktitle = {DATE '09: Proceedings of the conference on Design, Automation and Test in Europe},
  year = {2009},
  pages = {1692-1697}
}

@mastersthesis{fredHDR,
  author = {Pétrot, F.},
  title = {Intégration des systèmes matériel/logiciel},
  school = {Universitée Pierre et Marie Curie},
  year = {2003}
}

@book{rasiowa78algebra,
  author = {H.~Rasiowa},
  title = {An Algebraic Approach to Non-Classicals Logis},
  year = {1978}
}

@inproceedings{RaviS04MinimalAssig,
  author = {K.~Ravi and F.~Somenzi},
  title = {Minimal Assignments for Bounded Model Checking},
  booktitle = {TACAS'04: Proceedings of 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  publisher = {Springer},
  year = {2004},
  volume = {2988},
  pages = {31-45}
}

@inproceedings{DBLP:conf/cav/RoordaC06,
  author = {Jan-Willem Roorda and Koen Claessen},
  title = {SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation},
  booktitle = {CAV},
  year = {2006},
  volume = {4144},
  pages = {175-189}
}

@inproceedings{roux03ctl,
  author = {C.~Roux and E.~Encrenaz},
  title = {CTL May Be Ambiguous When Model Checking Moore Machines.},
  booktitle = {CHARME},
  publisher = {Springer},
  year = {2003},
  volume = {2860},
  pages = {164-169},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2860&spage=164}
}

@inproceedings{DBLP:conf/date/RoychoudhuryMK03,
  author = {Abhik Roychoudhury and Tulika Mitra and S. R. Karri},
  title = {Using Formal Techniques to Debug the AMBA System-on-Chip Bus Protocol.},
  booktitle = {DATE},
  publisher = {IEEE Computer Society},
  year = {2003},
  pages = {10828-10833}
}

@inproceedings{sawada97trace,
  author = {J.~Sawada and W.A.~Hunt},
  title = {Trace Table Based Approach for Pipeline Microprocessor Verification},
  booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification},
  publisher = {Springer-Verlag LNCS 1254},
  year = {1997},
  pages = {364--375}
}

@inproceedings{eveking06fdl,
  author = {M.~Schickel and V.~Nimbler and M.~Braun and H.~Eveking},
  title = {On Consistency and Completness of Property-Sets~: Exploiting the Property-Based Design Process},
  booktitle = {FDL'06: Proceeding of Forum on specification and Design Languages},
  year = {2006}
}

@article{DBLP:journals/fmsd/SegerB95,
  author = {Carl-Johan H. Seger and Randal E. Bryant},
  title = {Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories},
  journal = {Formal Methods in System Design},
  year = {1995},
  volume = {6},
  number = {2},
  pages = {147-189}
}

@article{Sharygin2012,
  author = {Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich},
  title = {An abstraction refinement approach combining precise and approximated techniques},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  publisher = {Springer},
  year = {2012},
  volume = {14},
  pages = {1-14},
  url = {http://dx.doi.org/10.1007/s10009-011-0185-y}
}

@inproceedings{magnier-sherman:factotum,
  author = {D.J Sherman and N. Magnier},
  title = {Factotum: Automatic and Systematic Sharing Support for Systems Analyzers},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98)},
  publisher = {Springer-Verlag LNCS 1384},
  year = {1982}
}

@inproceedings{shohamG04monotonic,
  author = {S.~Shoham and O.~Grumberg},
  title = {Monotonic Abstraction-Refinement for CTL.},
  booktitle = {TACAS'04: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  publisher = {Springer},
  year = {2004},
  volume = {2988},
  pages = {546-560}
}

@inproceedings{shoham06precision,
  author = {S.~Shoham and O.~Grumberg},
  title = {3-Valued Abstraction: More Precision at Less Cost},
  booktitle = {LICS '06: proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science},
  publisher = {IEEE Computer Society},
  year = {2006},
  pages = {399--410},
  doi = {http://dx.doi.org/10.1109/LICS.2006.5}
}

@article{DBLP:journals/tcad/SmithVAV05,
  author = {Alexander Smith and Andreas G. Veneris and Moayad Fahim Ali and Anastasios Viglas},
  title = {Fault diagnosis and logic debugging using Boolean satisfiability},
  journal = {IEEE Trans. on CAD of Integrated Circuits and Systems},
  year = {2005},
  volume = {24},
  number = {10},
  pages = {1606-1621}
}

@inproceedings{somenzi00efficient,
  author = {F.~Somenzi and R.~Bloem},
  title = {Efficient Büchi Automata from LTL Formulae.},
  booktitle = {CAV},
  publisher = {Springer},
  year = {2000},
  volume = {1855},
  pages = {248-263}
}

@incollection{IMM2001-0855,
  author = {J. Sparsø},
  title = {Asynchronous Circuit Design - A Tutorial},
  booktitle = {Chapters 1-8 in ''Principles of asynchronous circuit design - A systems Perspective''},
  publisher = {Kluwer Academic Publishers},
  year = {2001},
  pages = {1-152},
  url = {http://www2.imm.dtu.dk/pubdb/p.php?855}
}

@inproceedings{StaberFBD06,
  author = {Stefan Staber and Görschwin Fey and Roderick Bloem and Rolf Drechsler},
  title = {Automatic Fault Localization for Property Checking},
  booktitle = {Haifa Verification Conference},
  publisher = {Springer},
  year = {2006},
  volume = {4383},
  pages = {50-64}
}

@manual{AtelierB,
  author = {STERIA Technologie de l'information},
  title = {Atelier B, Manuel Utilisateur},
  year = {1998}
}

@inproceedings{DBLP:conf/date/SulflowFBKD09,
  author = {André Sülflow and Görschwin Fey and Cécile Braunstein and Ulrich Kühne and Rolf Drechsler},
  title = {Increasing the accuracy of SAT-based debugging},
  booktitle = {DATE},
  publisher = {IEEE},
  year = {2009},
  pages = {1326-1331}
}

@phdthesis{turk05thesis,
  author = {Türk, T.},
  title = {A Hierarchy for Accellera's Property Specification Language},
  school = {University of Kaiserslautern},
  year = {2005},
  url = {http://thomas-tuerk.de/dokumente/Diplomarbeit.pdf}
}

@manual{vismanual,
  author = {The VIS Group},
  title = {VIS User's Manual},
  year = {1996}
}

@misc{m106archi,
  author = {Université Pierre et Marie Curie (UPMC), Paris 6},
  title = {UE : Achitecture des systèmes intégrés, M1},
  note = {http://www-master.ufr-info-p6.jussieu.fr/ue/archi/}
}

@article{fms,
  author = {D.M.~Upton},
  title = {A Flexible Structure for Computer-Controlled Manufacturing Systems},
  journal = {Manufacturing Review},
  year = {1992},
  volume = {5},
  number = {1},
  pages = {58--74}
}

@inproceedings{Valk93,
  author = {R. Valk},
  title = {Bridging the Gap between Place- and Floyd-Invariants with Applications to Preemptive Scheduling},
  booktitle = {Proc. of ICATPN'93},
  publisher = {Springer Verlag},
  year = {1993},
  volume = {691},
  pages = {432--452}
}

@inproceedings{DBLP:conf/tacas/VelevB98,
  author = {Miroslav N. Velev and Randal E. Bryant},
  title = {Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation},
  booktitle = {TACAS},
  publisher = {Springer},
  year = {1998},
  volume = {1384},
  pages = {136-150}
}

@inproceedings{xie03verified,
  author = {F.~Xie and J.C.~Browne},
  title = {Verified Systems by Composition from Verified Components},
  booktitle = {ESEC/FSE 2003 : Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference},
  publisher = {ACM Press},
  year = {2003},
  pages = {277--286},
  doi = {http://doi.acm.org/10.1145/940071.940109}
}

@phdthesis{Yadgar10thesis,
  author = {Avi Yadgar},
  title = {New Approaches to Model Checking and to 3-Valued Abstraction and Refinement},
  school = {Technion - Israel Institute of Technology},
  year = {2010}
}

@techreport{cegarhwcasestudy07,
  author = {Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah},
  title = {CEGAR-Based Formal Hardware Verification: A Case Study},
  year = {2007}
}

@article{Zaki08analogformalsurvey,
  author = {M.H~Zaki and S.~Tahar and G.~Bois},
  title = {Formal verification of analog and mixed signal designs: A survey},
  journal = {Microelectronics Journal},
  publisher = {Elsevier Science Publishers B. V.},
  year = {2008},
  volume = {39},
  number = {12},
  pages = {1395--1404},
  doi = {http://dx.doi.org/10.1016/j.mejo.2008.05.013}
}

@proceedings{DBLP:conf/fmcad/2002,,
  title = {Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings},
  booktitle = {FMCAD},
  publisher = {Springer},
  year = {2002},
  volume = {2517}
}

@proceedings{DBLP:conf/sefm/2005,,
  title = {Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 7-9 September 2005, Koblenz, Germany},
  booktitle = {SEFM},
  publisher = {IEEE Computer Society},
  year = {2005}
}

@proceedings{DBLP:conf/cav/2004,,
  title = {Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  year = {2004},
  volume = {3114}
}

@proceedings{DBLP:conf/cav/2006,,
  title = {CAV'06: Proceedings of 18th International Conference of Computer Aided Verification},
  booktitle = {CAV},
  year = {2006},
  volume = {4144}
}

@proceedings{DBLP:conf/sfm/2006,,
  title = {Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced Lectures},
  booktitle = {SFM},
  publisher = {Springer},
  year = {2006},
  volume = {3965}
}

@proceedings{DBLP:conf/cav/2001,,
  title = {Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  year = {2001},
  volume = {2102}
}

@proceedings{DBLP:conf/hvc/2006,,
  title = {Hardware and Software, Verification and Testing, Second International Haifa Verification Conference, HVC 2006, Haifa, Israel, October 23-26, 2006. Revised Selected Papers},
  booktitle = {Haifa Verification Conference},
  publisher = {Springer},
  year = {2007},
  volume = {4383}
}

@proceedings{DBLP:conf/fmco/2005,,
  title = {Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures},
  booktitle = {FMCO},
  publisher = {Springer},
  year = {2006},
  volume = {4111}
}

@proceedings{DBLP:conf/charme/2005,,
  title = {Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings},
  booktitle = {CHARME},
  publisher = {Springer},
  year = {2005},
  volume = {3725}
}

@proceedings{DBLP:conf/cav/2002,,
  title = {Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  year = {2002},
  volume = {2404}
}

@proceedings{DBLP:conf/fase/2005,,
  title = {Fundamental Approaches to Software Engineering, 8th International Conference, FASE 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings},
  booktitle = {FASE},
  publisher = {Springer},
  year = {2005},
  volume = {3442}
}

@proceedings{DBLP:conf/lpar/2008,,
  title = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings},
  booktitle = {LPAR},
  publisher = {Springer},
  year = {2008},
  volume = {5330}
}

@proceedings{DBLP:conf/vmcai/2005,,
  title = {Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings},
  booktitle = {VMCAI},
  publisher = {Springer},
  year = {2005},
  volume = {3385}
}

@proceedings{DBLP:conf/tcs/1981,,
  title = {Theoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany, March 23-25, 1981, Proceedings},
  booktitle = {Theoretical Computer Science},
  publisher = {Springer},
  year = {1981},
  volume = {104}
}

@proceedings{DBLP:conf/vmcai/2006,,
  title = {Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings},
  booktitle = {VMCAI},
  publisher = {Springer},
  year = {2006},
  volume = {3855}
}

@proceedings{DBLP:conf/cav/2000,,
  title = {Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  year = {2000},
  volume = {1855}
}

@proceedings{DBLP:conf/apn/2002,,
  title = {Applications and Theory of Petri Nets 2002, 23rd International Conference, ICATPN 2002, Adelaide, Australia, June 24-30, 2002, Proceedings},
  booktitle = {ICATPN},
  publisher = {Springer},
  year = {2002},
  volume = {2360}
}

@proceedings{DBLP:conf/charme/2003,,
  title = {Correct Hardware Design and Verification Methods CHARME 2003},
  publisher = {Springer},
  year = {2003},
  volume = {2860}
}

@proceedings{DBLP:conf/date/2006p,,
  title = {Proceedings of the Conference on Design, Automation and Test in Europe, DATE 2006, Munich, Germany, March 6-10, 2006},
  booktitle = {DATE},
  publisher = {European Design and Automation Association, Leuven, Belgium},
  year = {2006}
}

@proceedings{DBLP:conf/sat/2003,,
  title = {Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers},
  booktitle = {SAT},
  publisher = {Springer},
  year = {2004},
  volume = {2919}
}

@proceedings{DBLP:conf/frocos/2005,,
  title = {Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, Proceedings},
  booktitle = {FroCoS},
  publisher = {Springer},
  year = {2005},
  volume = {3717}
}

@proceedings{DBLP:conf/cav/1997,,
  title = {Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  year = {1997},
  volume = {1254}
}

@proceedings{DBLP:conf/cav/1999,,
  title = {Computer Aided Verification, 11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  year = {1999},
  volume = {1633}
}

@proceedings{DBLP:conf/tacas/2005,,
  title = {Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  year = {2005},
  volume = {3440}
}

@proceedings{DBLP:conf/iccad/2006,,
  title = {2006 International Conference on Computer-Aided Design (ICCAD'06), November 5-9, 2006, San Jose, CA, USA},
  booktitle = {ICCAD},
  publisher = {ACM},
  year = {2006}
}

@proceedings{DBLP:conf/tacas/2006,,
  title = {Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  year = {2006},
  volume = {3920}
}

@proceedings{DBLP:conf/cav/1998,,
  title = {Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  year = {1998},
  volume = {1427}
}

@proceedings{DBLP:conf/tacas/2004,,
  title = {Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  year = {2004},
  volume = {2988}
}

@proceedings{DBLP:conf/vmcai/2011,,
  title = {Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings},
  booktitle = {VMCAI},
  publisher = {Springer},
  year = {2011},
  volume = {6538}
}

@proceedings{DBLP:conf/cav/2003,,
  title = {Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  year = {2003},
  volume = {2725}
}

@proceedings{DBLP:conf/dac/2005,,
  title = {Proceedings of the 42nd Design Automation Conference, DAC 2005, San Diego, CA, USA, June 13-17, 2005},
  booktitle = {DAC},
  publisher = {ACM},
  year = {2005}
}

@proceedings{DBLP:conf/lop/1981,,
  title = {Logic of Programs, Workshop},
  booktitle = {Logic of Programs},
  publisher = {Springer},
  year = {1982},
  volume = {131}
}

@proceedings{DBLP:conf/dac/2004,,
  title = {Proceedings of the 41th Design Automation Conference, DAC 2004, San Diego, CA, USA, June 7-11, 2004},
  booktitle = {DAC},
  publisher = {ACM},
  year = {2004}
}

@proceedings{DBLP:conf/birthday/2010pnueli,,
  title = {Time for Verification, Essays in Memory of Amir Pnueli},
  booktitle = {Essays in Memory of Amir Pnueli},
  publisher = {Springer},
  year = {2010},
  volume = {6200}
}

@proceedings{DBLP:conf/tacas/2001,,
  title = {Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  year = {2001},
  volume = {2031}
}

@proceedings{DBLP:conf/sbmf/2009,,
  title = {Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers},
  booktitle = {SBMF},
  publisher = {Springer},
  year = {2009},
  volume = {5902}
}

@proceedings{DBLP:conf/concur/2000,,
  title = {CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings},
  booktitle = {CONCUR},
  publisher = {Springer},
  year = {2000},
  volume = {1877}
}

@proceedings{DBLP:conf/tacas/2008,,
  title = {Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  year = {2008},
  volume = {4963}
}

@proceedings{DBLP:conf/compos/1997,,
  title = {Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures},
  booktitle = {COMPOS},
  publisher = {Springer},
  year = {1998},
  volume = {1536}
}

@proceedings{DBLP:conf/dac/2006,,
  title = {Proceedings of the 43rd Design Automation Conference, DAC 2006, San Francisco, CA, USA, July 24-28, 2006},
  booktitle = {DAC},
  publisher = {ACM},
  year = {2006}
}

@proceedings{DBLP:conf/tacas/1998,,
  title = {Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  year = {1998},
  volume = {1384}
}

@proceedings{DBLP:conf/forte/2005,,
  title = {Formal Techniques for Networked and Distributed Systems - FORTE 2005, 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005, Proceedings},
  booktitle = {FORTE},
  publisher = {Springer},
  year = {2005},
  volume = {3731}
}

@proceedings{DBLP:conf/fm/1999-1,,
  title = {FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume I},
  booktitle = {World Congress on Formal Methods},
  publisher = {Springer},
  year = {1999},
  volume = {1708}
}

@misc{alliance,,
  title = {Alliance, a free VLSI cad system},
  note = {\http://www-asim.lip6.fr/recherche/alliance/}
}

@misc{onespin,,
  title = {OneSpin Solutions},
  note = {http://www.onespin-solutions.com/}
}

@misc{prosyd,,
  title = {The Prosyd Project on Property-Based System Design},
  note = {http://www.prosyd.org/}
}

@misc{soclib,,
  title = {The SoCLib Project},
  note = {http://soclib.lip6.fr/},
  url = {http://soclib.lip6.fr/}
}

@misc{texas97bench,,
  title = {Texas-97 Verification Benchmarks},
  note = {\http://www.cad.eecs.berkeley.edu/Respep/Research/vis/texas-97/}
}

@misc{vsia,,
  title = {VSI Alliance},
  note = {http://www.vsi.org/}
}

@proceedings{DBLP:conf/date/2009,,
  title = {Design, Automation and Test in Europe, DATE 2009, Nice, France, April 20-24, 2009},
  booktitle = {DATE},
  publisher = {IEEE},
  year = {2009}
}

@proceedings{DBLP:conf/fmcad/2009,,
  title = {Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA},
  booktitle = {FMCAD},
  publisher = {IEEE},
  year = {2009}
}

@proceedings{DBLP:conf/lics/2004,,
  title = {19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings},
  booktitle = {LICS},
  publisher = {IEEE Computer Society},
  year = {2004}
}

@proceedings{DBLP:conf/sat/2004,,
  title = {SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings},
  booktitle = {SAT},
  year = {2004}
}

@proceedings{DBLP:conf/date/2003,,
  title = {2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), 3-7 March 2003, Munich, Germany},
  booktitle = {DATE},
  publisher = {IEEE Computer Society},
  year = {2003}
}

@proceedings{DBLP:conf/icse/2003,,
  title = {Proceedings of the 25th International Conference on Software Engineering, May 3-10, 2003, Portland, Oregon, USA},
  booktitle = {ICSE},
  publisher = {IEEE Computer Society},
  year = {2003}
}

@proceedings{DBLP:conf/time/2003,,
  title = {10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), 8-10 July 2003, Cairns, Queensland, Australia},
  booktitle = {TIME},
  publisher = {IEEE Computer Society},
  year = {2003}
}

@proceedings{DBLP:conf/iccd/2002,,
  title = {20th International Conference on Computer Design (ICCD 2002), VLSI in Computers and Processors, 16-18 September 2002, Freiburg, Germany, Proceedings},
  booktitle = {ICCD},
  publisher = {IEEE Computer Society},
  year = {2002}
}

@proceedings{DBLP:conf/dac/2001,,
  title = {Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001},
  booktitle = {DAC},
  publisher = {ACM},
  year = {2001}
}

@proceedings{DBLP:conf/icse/2001,,
  title = {Proceedings of the 23rd International Conference on Software Engineering, ICSE 2001, 12-19 May 2001, Toronto, Ontario, Canada},
  booktitle = {ICSE},
  publisher = {IEEE Computer Society},
  year = {2001}
}

@manual{amba,,
  title = {AMBA Specification},
  year = {1999},
  edition = {2.0},
  note = {ARM Limited pyright. All right reserved}
}

@manual{formalcheck,,
  title = {Formal Verification Using Affirma FormalCheck},
  year = {1999}
}

@proceedings{DBLP:conf/lics/LICS4,,
  title = {Proceedings, Fourth Annual Symposium on Logic in Computer Science, 5-8 June, 1989, Asilomar Conference Center, Pacific Grove, California, USA},
  booktitle = {LICS},
  publisher = {IEEE Computer Society},
  year = {1989}
}

@proceedings{DBLP:conf/lics/LICS3,,
  title = {Proceedings, Third Annual Symposium on Logic in Computer Science},
  booktitle = {LICS},
  publisher = {IEEE Computer Society},
  year = {1988}
}

@proceedings{DBLP:conf/stoc/STOC14,,
  title = {Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, 5-7 May 1982, San Francisco, California, USA},
  booktitle = {STOC},
  publisher = {ACM},
  year = {1982}
}