source: biblio/biblio.bib @ 45

% This file was created with JabRef 2.5.
% Encoding: UTF8

@STRING{LICS04 = {LICS'04: Proceedings of the 19th IEEE Symposium on Logic in Computer
        Science}}

@STRING{LNCS = {}}

@INPROCEEDINGS{aagaard03hazards,
  author = {M.~Aagaard},
  title = {A {H}azards-{B}ased {C}orrectness {S}tatement for {P}ipelined {C}ircuits.},
  booktitle = {Proceedings of the 12th IFIP WG 10.5 Advanced Research Working Conference},
  year = {2003},
  pages = {66-80},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/charme/2003},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2860{\&}spage=66},
  file = {aagard.pdf:/dsk/l1/misc/doc/verif_archi/aagard.pdf:PDF},
  keywords = {pipeline}
}

@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 T}ool for {I}nterface {C}ompatibility and {C}omposition.},
  booktitle = {CAV'06: Proceedings of 18th International Conference of Computer
        Aided Verification},
  year = {2006},
  pages = {59-62},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/2006},
  ee = {http://dx.doi.org/10.1007/11817963_8},
  file = {tiicctool.pdf:/dsk/l1/misc/doc/interface/tiicctool.pdf:PDF},
  keywords = {interface, wrapper}
}

@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},
  year = {2005},
  pages = {81-105},
  address = {Vienna, Austria},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/frocos/2005},
  ee = {http://dx.doi.org/10.1007/11559306_5}
}

@INPROCEEDINGS{alur98alternatingtime,
  author = {Rajeev Alur and Thomas A. Henzinger and Orna Kupferman},
  title = {{Alternating-Time Temporal Logic}},
  booktitle = {COMPOS},
  year = {1997},
  pages = {23-60},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/compos/1997},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1536/15360023.htm},
  keywords = {atl}
}

@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},
  year = {2008},
  pages = {343-352},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/lpar/2008},
  ee = {http://dx.doi.org/10.1007/978-3-540-89439-1_25},
  keywords = {CEGAR,Hardware, TOOLS}
}

@INPROCEEDINGS{DBLP:conf/dac/AndrausS04,
  author = {Zaher S. Andraus and Karem A. Sakallah},
  title = {Automatic abstraction and verification of verilog models},
  booktitle = {DAC},
  year = {2004},
  pages = {218-223},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/dac/2004},
  ee = {http://doi.acm.org/10.1145/996566.996629},
  file = {:Abstraction/Andraus_DAC_Vapor.pdf:PDF},
  keywords = {Abstraction, Hardware, Verilog, TOOLS, Vapor}
}

@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},
  year = {2004},
  pages = {96-108},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/2004},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3114{\&}spage=96},
  file = {:BMC/ProvingMorePropwithBC04.pdf:PDF},
  keywords = {BMC, VIS}
}

@INPROCEEDINGS{bmethod99meteor,
  author = {P.~Behm and P.~Benoit and A.~Faivre and J-M.~Meynadier},
  title = {{M{\'e}t{\'e}or: A Successful Application of B in a Large Project}},
  booktitle = {World Congress on Formal Methods},
  year = {1999},
  pages = {369-387},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/fm/1999-1},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1708/17080369.htm}
}

@INPROCEEDINGS{DBLP:conf/vmcai/Bradley11,
  author = {Aaron R. Bradley},
  title = {SAT-Based Model Checking without Unrolling},
  booktitle = {VMCAI},
  year = {2011},
  pages = {70-87},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/vmcai/2011},
  ee = {http://dx.doi.org/10.1007/978-3-642-18275-4_7}
}

@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},
  year = {2000},
  editor = {Nicolas Halbwachs and Doron Peled},
  series = {Lecture Notes in Computer Science},
  pages = {168-182},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/concur/2000},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1877/18770168.htm},
  file = {godefroid00.pdf:/dsk/l1/misc/doc/abstraction/godefroid00.pdf:PDF},
  keywords = {3-valued, Kripke structure, abstraction}
}

@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},
  year = {1999},
  series = {Lecture Notes in Computer Science},
  pages = {274-287},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/1999},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1633/16330274.htm},
  file = {burns99partial.pdf:/dsk/l1/misc/doc/abstraction/burns99partial.pdf:PDF},
  keywords = {tree automata, CTL, automata approach},
  owner = {cecile},
  timestamp = {2006.04.25}
}

@INPROCEEDINGS{Buttner05isformal,
  author = {W. B{\"u}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},
  year = {2005},
  editor = {Dominique Borrione, Wolfgang J. Paul},
  volume = {3725},
  series = {Lecture Notes in Computer Science},
  pages = {1},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/charme/2005},
  ee = {http://dx.doi.org/10.1007/11560548_1},
  owner = {cecile},
  timestamp = {2006.06.27}
}

@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 },
  year = {2002},
  pages = {33-51},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/fmcad/2002},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2517/25170033.htm},
  file = {:Cegar/AutomatedAbstractionRefinment02Chauchan.pdf:PDF},
  keywords = {Cegar, SAT}
}

@INPROCEEDINGS{chechik05framework,
  author = {Marsha Chechik and Arie Gurfinkel},
  title = {A Framework for Counterexample Generation and Exploration.},
  booktitle = {FASE},
  year = {2005},
  pages = {220-236},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/fase/2005},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3442{\&}spage=220},
  file = {chechik05a.pdf:/dsk/l1/misc/doc/abstraction/chechik05a.pdf:PDF}
}

@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},
  year = {2001},
  series = {LNCS},
  pages = {528-542},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/tacas/2001},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2031/20310528.htm},
  file = {:Fault/Coverage_Metric_for_temporal_MC01.pdf:PDF},
  keywords = {coverage}
}

@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},
  year = {2009},
  pages = {9-16},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/fmcad/2009},
  ee = {http://dx.doi.org/10.1109/FMCAD.2009.5351149},
  file = {:Cegar/StructureAwareComputationofPredicateAbstraction09.pdf:PDF},
  keywords = {Abstraction}
}

@INPROCEEDINGS{DBLP:conf/sfm/ClaessenR06,
  author = {Koen Claessen and Jan-Willem Roorda},
  title = {An Introduction to Symbolic Trajectory Evaluation},
  booktitle = {SFM},
  year = {2006},
  pages = {56-77},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/sfm/2006},
  ee = {http://dx.doi.org/10.1007/11757283_3}
}

@INPROCEEDINGS{clarke03cegar,
  author = {E.M.~Clarke},
  title = {Counterexample-Guided Abstraction Refinement},
  booktitle = {TIME},
  year = {2003},
  pages = {7},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/time/2003},
  ee = {http://csdl.computer.org/comp/proceedings/time-ictl/2003/1912/00/19120007.pdf},
  file = {ce03time.pdf:/dsk/l1/misc/doc/CEGAR/ce03time.pdf:PDF},
  keywords = {abstraction, CEGAR}
}

@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},
  year = {1981},
  pages = {52-71},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/lop/1981}
}

@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},
  year = {2000},
  pages = {154-169},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/2000}
}

@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},
  year = {2010},
  pages = {61-71},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/birthday/2010pnueli},
  ee = {http://dx.doi.org/10.1007/978-3-642-13754-9_4}
}

@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},
  year = {1989},
  pages = {353-362},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/lics/LICS4},
  file = {clarke89compo.ps:/dsk/l1/misc/doc/model_check/clarke89compo.ps:PDF},
  keywords = {composition, model checking, Kripke structure, Moore machine, CTL}
}

@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},
  year = {2003},
  pages = {78-92},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/sat/2003},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2919{\&}spage=78},
  file = {:Abstraction/SATBasedPredicateAbstactforHWVerif2004.pdf:PDF},
  keywords = {SAT, predicate abstraction, hardware}
}

@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},
  year = {2002},
  pages = {101-120},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/apn/2002},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2360/23600101.htm}
}

@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},
  year = {2005},
  editor = {Farn Wang},
  volume = {3731},
  series = {Lecture Notes in Computer Science},
  pages = {443-457},
  address = {Taipei, Taiwan},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/forte/2005},
  ee = {http://dx.doi.org/10.1007/11562436_32}
}

@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},
  year = {2005},
  series = {Lecture Notes in Computer science},
  pages = {216-232},
  address = {Paris, France},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/vmcai/2005},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3385{\&}spage=216},
  file = {automata_aabstr.pdf:/dsk/l1/misc/doc/modular/abstraction/automata_aabstr.pdf:PDF},
  keywords = {tree automata, CTL, automata approach}
}

@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},
  year = {2004},
  pages = {335-344},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/lics/2004},
  ee = {http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920335abs.htm},
  file = {abstractforbtl.pdf:/dsk/l1/misc/doc/ctl_auto/abstractforbtl.pdf:PDF},
  keywords = {CTL, tree automata ,model checking, automata approach}
}

@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},
  year = {2001},
  pages = {177-187},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/icse/2001},
  file = {bandera.pdf:/dsk/l1/misc/doc/softMC/bandera.pdf:PDF},
  keywords = {software, model-checking, CEGAR}
}

@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 = {{$\chi$Chek: A Model Checker for Multi-Valued Reasoning.}},
  booktitle = {ICSE'03: Proceedings of the 25th International Conference on Software
        Engineering},
  year = {2003},
  pages = {804-805},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/icse/2003},
  ee = {http://computer.org/proceedings/icse/1877/18770804.pdf}
}

@INPROCEEDINGS{EasterbrookC01,
  author = {Steve M. Easterbrook and Marsha Chechik},
  title = {A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints.},
  booktitle = {ICSE},
  year = {2001},
  pages = {411-420},
  bibsource = {DBLP,http://dblp.uni-trier.de},
  crossref = {DBLP:conf/icse/2001},
  file = {easterbrook01a.pdf:/dsk/l1/misc/doc/multi_valued/easterbrook01a.pdf:PDF},
  keywords = {abstraction, 3-valued, 4-valued, logic, model checking}
}

@INPROCEEDINGS{emerson82desision,
  author = {E.A.~Emerson and J.Y.~Halpern},
  title = {Decision Procedures and Expressiveness in the Temporal Logic of Branching
        Time},
  booktitle = {STOC},
  year = {1982},
  pages = {169-180},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/stoc/STOC14},
  file = {ctl_emerson82.pdf:/dsk/l1/misc/doc/model_check/ctl_emerson82.pdf:PDF},
  keywords = {CTL, model checking}
}

@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},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/date/2005},
  ee = {http://doi.ieeecomputersociety.org/10.1109/DATE.2005.325},
  file = {:Abstraction/VerifEmbededMemoryusingEMM09.pdf:PDF},
  keywords = {Abstraction, Memory,},
  owner = {cecile},
  timestamp = {2010.06.10}
}

@INPROCEEDINGS{DBLP:conf/cav/GodefroidJ02,
  author = {P.~Godefroid and R.~Jagadeesan},
  title = {Automatic Abstraction Using Generalized Model Checking.},
  booktitle = {CAV},
  year = {2002},
  pages = {137-150},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/2002},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040137.htm}
}

@INPROCEEDINGS{GrafS97pvs,
  author = {S.~Graf and H.~Sa\"{\i}di},
  title = {{Construction of Abstract State Graphs with PVS.}},
  booktitle = {CAV},
  year = {1997},
  pages = {72-83},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/1997},
  file = {graf97cinstructionpvs.ps:/dsk/l1/misc/doc/abstraction/graf97cinstructionpvs.ps:PDF},
  keywords = {abstraction, CEGAR}
}

@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,},
  year = {2005},
  pages = {219-242},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/fmco/2005},
  ee = {http://dx.doi.org/10.1007/11804192_11},
  keywords = {abstraction, refinement, CEGAR}
}

@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},
  year = {2006},
  pages = {108-143},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/sfm/2006},
  ee = {http://dx.doi.org/10.1007/11757283_5},
  file = {:BMC/SATBasedVerifMethodAndApplitoHdw2006.pdf:PDF},
  keywords = {SAT, verification,}
}

@INPROCEEDINGS{gurfinkelC06waste,
  author = {A.~Gurfinkel and M.~Chechik},
  title = {{Why Waste a Perfectly Good Abstraction?.}},
  booktitle = {T{ACAS}'06: {P}roceedings of the 12th international conference on
        {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis of
        {S}ystems},
  year = {2006},
  series = {Lecture Notes in Computer Science},
  pages = {212-226},
  address = {Vienna, Austria},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/tacas/2006},
  ee = {http://dx.doi.org/10.1007/11691372_14},
  file = {gurfinkel_tacas_06.pdf:/dsk/l1/misc/doc/abstraction/gurfinkel_tacas_06.pdf:PDF},
  keywords = {abstraction, 3-valued, 4-valued, logic, model checking}
}

@INPROCEEDINGS{DBLP:conf/vmcai/GurfinkelWC06,
  author = {Arie Gurfinkel and Ou Wei and Marsha Chechik},
  title = {Systematic Construction of Abstractions for Model-Checking},
  booktitle = {VMCAI},
  year = {2006},
  pages = {381-397},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/vmcai/2006},
  ee = {http://dx.doi.org/10.1007/11609773_25}
}

@INPROCEEDINGS{GurfinkelWC06,
  author = {Gurfinkel, A. and Wei, O. and Chechik, M.},
  title = {Systematic {C}onstruction of {A}bstractions for {M}odel-{C}hecking.},
  booktitle = {V{MCAI}'06: {P}roceedings of the 7th {I}nternational {C}onference
        on {V}erification, {M}odel {C}hecking, and {A}bstract {I}nterpretation},
  year = {2006},
  pages = {381-397},
  address = {Charleston, USA},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/vmcai/2006},
  ee = {http://dx.doi.org/10.1007/11609773_25},
  keywords = {abstraction, abstract interpretation}
}

@INPROCEEDINGS{JainKSC05,
  author = {Jain, H. and Kroening, D. and Sharygina, N. and Clarke, E.M.},
  title = {Word {L}evel {P}redicate {A}bstraction and {R}efinement for {V}erifying
        {RTL} {V}erilog.},
  booktitle = {D{AC}'05: {P}roceedings of the 42nd {D}esign {A}utomation {C}onference},
  year = {2005},
  editor = {William H. Joyner Jr., Grant Martin, Andrew B. Kahng},
  series = {ACM},
  pages = {445-450},
  address = {San Diego, USA},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/dac/2005},
  ee = {http://doi.acm.org/10.1145/1065579.1065697}
}

@INPROCEEDINGS{jhala01microarchi,
  author = {Jhala, R. and McMillan, K.L.},
  title = {Microarchitecture {V}erification by {C}ompositional {M}odel {C}hecking.},
  booktitle = {C{AV}'01: {P}roceedings of the 13th {I}nternational {C}onference
        on {C}omputer {A}ided {V}erification},
  year = {2001},
  editor = {G\'erard Berry, Hubert Comon, Alain Finkel},
  series = {Lecture Notes in Computer Science},
  pages = {396-410},
  address = {Paris, France},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/2001},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2102/21020396.htm}
}

@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 },
  year = {2004},
  pages = {519-522},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/2004},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3114{\&}spage=519},
  file = {:SAT/CirCUsToward.pdf:PDF},
  keywords = {SAT, SAT solver, VIS}
}

@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},
  year = {2005},
  pages = {287-300},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/tacas/2005},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3440{\&}spage=287},
  file = {:SAT/efficientConflict05Jin.pdf:PDF},
  keywords = {SAT, All-sat}
}

@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},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/sat/2004},
  ee = {http://www.satisfiability.org/SAT04/programme/24.pdf},
  owner = {cecile},
  timestamp = {2009.01.27}
}

@INPROCEEDINGS{larsen88modal,
  author = {K.~G.~Larsen and B.~Thomsen},
  title = {A {M}odal {P}rocess {L}ogic},
  booktitle = {Third Annual Symposium on Logic in Computer Science},
  year = {1988},
  pages = {203-210},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/lics/LICS3}
}

@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},
  year = {2006},
  pages = {786-793},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/iccad/2006},
  ee = {http://doi.acm.org/10.1145/1233501.1233663},
  file = {:Abstraction/AutomaticMemoryReductionforRTL06.pdf:PDF},
  keywords = {Abstraction, memory}
}

@INPROCEEDINGS{mcmillan98tomasulo,
  author = {K.L.~McMillan},
  title = {Verification of an {I}mplementation of {T}omasulo's {A}lgorithm by
        {C}ompositional {M}odel {C}hecking.},
  booktitle = {C{AV}'98: {P}roceddings of the 10th {I}nternational {C}onference
        on {C}omputer {A}ided {V}erification},
  year = {1998},
  editor = {Alan J. Hu, Moshe Y. Vardi},
  volume = {1427},
  series = {Lecture Notes in Computer Science},
  pages = {110-121},
  address = {Vancouver, Canada},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/1998}
}

@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},
  year = {2002},
  pages = {250-264},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/2002},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040250.htm},
  file = {:BMC/Mcmillan02applyingSat.pdf:PDF}
}

@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},
  year = {1997},
  volume = {1254},
  series = {Lecture Notes in Computer Science},
  pages = {24-35},
  adress = {Haifa, Israel},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/1997}
}

@INPROCEEDINGS{Morin-AlloryB06,
  author = {K.~Morin-Allory and D.~Borrione},
  title = {Proven {C}orrect {M}onitors from {PSL} {S}pecifications.},
  booktitle = {D{ATE}'06: {P}roceedings of the {C}onference on {D}esign, {A}utomation
        and {T}est in {E}urope},
  year = {2006},
  editor = {{Georges G. E. Gielen}},
  pages = {1246-1251},
  address = {Munich, Germany},
  organization = {European Design and Automation Association},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/date/2006p},
  ee = {http://doi.acm.org/10.1145/1131827}
}

@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},
  year = {2001},
  pages = {530-535},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/dac/2001},
  ee = {http://jamaica.ee.pitt.edu/Archives/ProceedingArchives/Dac/Dac2001/papers/2001/dac01/pdffiles/33_1.pdf},
  file = {:SAT/4 - moskewicz01chaff.pdf:PDF}
}

@INPROCEEDINGS{DBLP:conf/sbmf/MouraB09,
  author = {Leonardo Mendon\c{c}a de Moura and Nikolaj Bj{\o}rner},
  title = {Satisfiability Modulo Theories: An Appetizer},
  booktitle = {SBMF},
  year = {2009},
  pages = {23-36},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/sbmf/2009},
  ee = {http://dx.doi.org/10.1007/978-3-642-10452-7_3}
}

@INPROCEEDINGS{DBLP:conf/tacas/MouraB08,
  author = {Leonardo Mendon\c{c}a de Moura and Nikolaj Bj{\o}rner},
  title = {Z3: An Efficient SMT Solver},
  booktitle = {TACAS},
  year = {2008},
  pages = {337-340},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/tacas/2008},
  ee = {http://dx.doi.org/10.1007/978-3-540-78800-3_24}
}

@INPROCEEDINGS{DBLP:conf/cav/Namjoshi03,
  author = {Kedar S. Namjoshi},
  title = {Abstraction for Branching Time Properties.},
  booktitle = {CAV},
  year = {2003},
  pages = {288-300},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/2003},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2725{\&}spage=288},
  file = {abstractforbtl.pdf:/dsk/l1/misc/doc/ctl_auto/abstractforbtl.pdf:PDF},
  keywords = {abstraction}
}

@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},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/date/2008},
  ee = {http://dx.doi.org/10.1109/DATE.2008.4484775}
}

@INPROCEEDINGS{DBLP:conf/dac/NanshiS06,
  author = {K.~Nanshi and F.~Somenzi},
  title = {Guiding simulation with increasingly refined abstract traces},
  booktitle = {DAC},
  year = {2006},
  pages = {737-742},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/dac/2006},
  ee = {http://doi.acm.org/10.1145/1146909.1147097}
}

@INPROCEEDINGS{nejati05stutering,
  author = {Shiva Nejati and Arie Gurfinkel and Marsha Chechik},
  title = {Stuttering Abstraction for Model Checking},
  booktitle = {SEFM},
  year = {2005},
  pages = {311-320},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/sefm/2005},
  ee = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.44},
  file = {nejati05.pdf:/dsk/l1/misc/doc/abstraction/nejati05.pdf:PDF}
}

@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},
  year = {1981},
  pages = {167-183},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/tcs/1981}
}

@INPROCEEDINGS{peng02tableau,
  author = {H.~Peng and Y.~Mokhtari and S.~Tahar},
  title = {Environment {S}ynthesis for {C}ompositional {M}odel {C}hecking.},
  booktitle = {I{CCD}'02: {P}roceedings of the 20th {I}nternational {C}onference
        on {C}omputer {D}esign},
  year = {2002},
  pages = {70-},
  address = {Freiburg, Germany},
  publisher = {IEEE Computer Society},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/iccd/2002},
  ee = {http://csdl.computer.org/comp/proceedings/iccd/2002/1700/00/17000070abs.htm}
}

@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},
  year = {2004},
  series = {LNCS},
  pages = {31-45},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/tacas/2004},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2988{\&}spage=31},
  file = {:SAT/minimal_assignment_for_bmc.pdf:PDF}
}

@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},
  pages = {175-189},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/2006},
  ee = {http://dx.doi.org/10.1007/11817963_19}
}

@INPROCEEDINGS{roux03ctl,
  author = {C.~Roux and E.~Encrenaz},
  title = {CTL May Be Ambiguous When Model Checking Moore Machines.},
  booktitle = {CHARME},
  year = {2003},
  pages = {164-169},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/charme/2003},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2860{\&}spage=164},
  file = {rouxctl.pdf:/dsk/l1/misc/doc/modular/model_checking/rouxctl.pdf:PDF},
  keywords = {CTL},
  owner = {cecile},
  timestamp = {2006.02.28},
  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},
  year = {2003},
  pages = {10828-10833},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/date/2003},
  ee = {http://csdl.computer.org/comp/proceedings/date/2003/1870/01/187010828abs.htm},
  keywords = {AMBA}
}

@INPROCEEDINGS{shohamG04monotonic,
  author = {S.~Shoham and O.~Grumberg},
  title = {Monotonic {A}bstraction-{R}efinement for {CTL}.},
  booktitle = {T{ACAS}'04: {P}roceedings of the 10th {I}nternational {C}onference
        on {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis
        of {S}ystems},
  year = {2004},
  editor = {Kurt Jensen, Andreas Podelski},
  volume = {2988},
  series = {Lecture Notes in Computer Science},
  pages = {546-560},
  address = {Barcelona, Spain},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/tacas/2004},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2988{\&}spage=546},
  file = {monotone-abs-ref.ps:/dsk/l1/misc/doc/ctl_auto/monotone-abs-ref.ps:PDF},
  keywords = {CTL , abstraction , 3-valued , refinment loop}
}

@INPROCEEDINGS{somenzi00efficient,
  author = {F.~Somenzi and R.~Bloem},
  title = {Efficient B{\"u}chi Automata from LTL Formulae.},
  booktitle = {CAV},
  year = {2000},
  pages = {248-263},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/cav/2000},
  file = {wring.ps:/dsk/l1/misc/doc/ltl_auto/wring.ps:PDF},
  keywords = {LTL, automata approach,},
  owner = {cecile},
  timestamp = {2006.02.13}
}

@INPROCEEDINGS{StaberFBD06,
  author = {Stefan Staber and G{\"o}rschwin Fey and Roderick Bloem and Rolf Drechsler},
  title = {Automatic Fault Localization for Property Checking},
  booktitle = {Haifa Verification Conference},
  year = {2006},
  pages = {50-64},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/hvc/2006},
  ee = {http://dx.doi.org/10.1007/978-3-540-70889-6_4},
  file = {:Debug/FaultLocalizationforpropertychecking-CAD06.pdf:PDF},
  keywords = {Debug, SAT}
}

@INPROCEEDINGS{DBLP:conf/date/SulflowFBKD09,
  author = {Andr{\'e} S{\"u}lflow and G{\"o}rschwin Fey and C{\'e}cile Braunstein
        and Ulrich K{\"u}hne and Rolf Drechsler},
  title = {Increasing the accuracy of SAT-based debugging},
  booktitle = {DATE},
  year = {2009},
  pages = {1326-1331},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/date/2009},
  ee = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?isnumber=5090609{\&}arnumber=5090870{\&}count=326{\&}index=256},
  file = {:Debug/increasingaccuracy-DATE09.pdf:PDF},
  keywords = {Debug, SAT, localization reduction, abstraction}
}

@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},
  year = {1998},
  pages = {136-150},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  crossref = {DBLP:conf/tacas/1998},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1384/13840136.htm},
  file = {:Abstraction/EfficientModelingMemoryArraySymbolicTernarySimulation98.pdf:PDF},
  keywords = {Abstraction, Memory, STE}
}

@PROCEEDINGS{DBLP:conf/charme/2003,
  title = {Correct Hardware Design and Verification Methods CHARME 2003},
  year = {2003},
  editor = {Daniel Geist and Enrico Tronci},
  volume = {2860},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  crossref = {DBLP:conf/charme/2003},
  owner = {cecile},
  timestamp = {2006.02.02}
}

@MANUAL{rulebase06userguide,
  title = {RuleBase Parallel Edition,User's Guide},
  author = {Model Checking Systems group},
  organization = {IBM Labs},
  address = {Haifa, Israel},
  year = {2005},
  note = {verion 1.26},
  owner = {cecile},
  timestamp = {2007.03.07}
}

@INPROCEEDINGS{Vis,
  author = {The {VIS} group},
  title = {{VIS} : {A} {S}ystem for {V}erification and {S}ynthesis},
  booktitle = {CAV'96: Proceedings of the 8th International Conference on Computer
        Aided Verification},
  year = {1996},
  editor = {{Rajeev Alur} and {Thomas A. Henzinger}},
  volume = {1102},
  series = {Lecture Notes in Computer Science},
  pages = {428--432},
  address = {New Brunswick, NJ, USA},
  publisher = {Springer-Verlag},
  abstract = {Manual abstraction can be performed by giving a file containing the
        names of variables to abstract. For each variable appearing in the
        file, a new primary input node is created to drive all the nodes
        that were previously driven by the variable. Abstracting a net effectively
        allows it to take any value in its range, at every clock cycle. Fair
        CTL model checking and language emptiness check VIS performs fair
        CTL model checking under Buchi fairness constraints. In addition,
        VIS can perform ...},
  citeseerurl = {citeseer.ist.psu.edu/brayton96vis.html},
  comment = {Proceedings of the Eighth International Conference on Computer Aided
        Verification},
  keywords = {model checker},
  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},
  pages = {104-125},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1007/s10703-008-0063-8},
  keywords = {Refinement}
}

@ARTICLE{akers78,
  author = {B.~Akers},
  title = {Binary Decision Diagrams},
  journal = {IEEE Transactions on Computers},
  year = {1978},
  volume = {27},
  pages = {509--516},
  number = {6},
  abstract = { The seminal paper in which BDD's were introduced. Note that none
        of the today implementation techniques for BDD package is given in
        this paper. },
  keywords = {BDD description}
}

@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},
  year = {2001},
  pages = {109--120},
  address = {New York, NY, USA},
  publisher = {ACM Press},
  doi = {http://doi.acm.org/10.1145/503209.503226},
  isbn = {1-58113-390-1},
  location = {Vienna, Austria}
}

@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},
  editor = {IEEE Computer Society},
  pages = {241},
  address = {Washington, DC, USA},
  isbn = {0-7695-1887-7}
}

@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},
  year = {1999},
  editor = {Jos C. M. Baeten and Sjouke Mauw},
  volume = {1664},
  series = {Lecture Notes in Computer Science},
  pages = {82-97},
  address = {Eindhoven, The Netherlands},
  publisher = {Springer},
  abstract = {Modular techniques for automatic verification attempt to overcome
        the state-explosion problem by exploiting the modular structure naturally
        present in many system designs. Unlike other tasks in the verification
        of finite-state systems, current modular techniques rely heavily
        on user guidance. In particular, the user is typically required to
        construct module abstractions that are neither too detailed as to
        render insufficient benefits in state exploration, nor too coarse
        as to invalidate the desired system properties. In this paper, we
        construct abstract modules automatically, using reachability and
        controllability information about the concrete modules. This allows
        us to leverage automatic verification techniques by applying them
        in layers: first we compute on the state spaces of system components,
        then we use the results for constructing abstractions, and finally
        we compute on the abstract state space of the system. Our experimental
        results indicate that if reachability and controllabil ity information
        is used in the construction of abstractions, the resulting abstract
        modules are often significantly smaller than the concrete modules
        and can drastically reduce the space and time requirements for verification.},
  file = {automatic_modular.pdf:/dsk/l1/misc/doc/modular/modular/automatic_modular.pdf:PDF},
  keywords = {modular, abstraction, refinment loop, case study},
  owner = {cecile},
  timestamp = {2006.02.06},
  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},
  year = {1999},
  volume = {15},
  pages = {7-48},
  number = {1},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  publisher = {Springer}
}

@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}: {M}odularity in {M}odel {C}hecking},
  booktitle = {CAV'98: Proceedings of the 10th International Conference on Computer
        Aided Verification},
  year = {1998},
  volume = {1427},
  series = {Lecture Notes in Computer Science},
  pages = {521-525},
  address = {London, UK},
  abstract = {We describe a new interactive verification environment called Mocha
        for modular verification of heterogeneous systems. Mocha differs
        from existing model checkers in three important ways. First, instead
        of manipulating unstructured statetransition graphs, it supports
        the heterogeneous modeling framework of Reactive Modules. Second,
        instead of traditional temporal logics such as CTL, it uses Alternating
        Temporal Logic (ATL), a temporal logic that is designed to specify
        collaborative as ...},
  file = {alur98mocha.ps.gz:/dsk/l1/misc/doc/modular/mocha/alur98mocha.ps.gz:PDF},
  keywords = {model checker, atl, modular}
}

@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},
  year = {2001},
  pages = {465--479},
  address = {London, UK},
  publisher = {Springer-Verlag},
  isbn = {3-540-41865-2}
}

@ARTICLE{arieliA98value,
  author = {Ofer Arieli and Arnon Avron},
  title = {The Value of the Four Values.},
  journal = {Artif. Intell.},
  year = {1998},
  volume = {102},
  pages = {97-141},
  number = {1},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1016/S0004-3702(98)00032-0},
  file = {arieli98four.ps:/dsk/l1/misc/doc/logique/arieli98four.ps:PDF},
  keywords = {4-valued, logic}
}

@BOOK{arnold94finite,
  title = {Finite {T}ransition {S}ystems: {S}emantics of {C}ommunicating {S}ystems},
  publisher = {Prentice Hall International Ltd.},
  year = {1994},
  editor = {Translator-John Plaice},
  author = {A.~Arnold},
  address = {Hertfordshire,UK},
  isbn = {0-13-092990-5},
  keywords = {simulation}
}

@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},
  pages = {51-66},
  number = {1},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1016/j.entcs.2005.07.019},
  file = {:BMC/TerminationCriteriaForBMC06.pdf:PDF},
  keywords = {BMC, VIS}
}

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

@INPROCEEDINGS{BP-msr03,
  author = {M.~Baclet and R.~Pacalet},
  title = {V{\'e}rifications du protocole~{VCI}},
  booktitle = {{A}ctes du 4{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes
        {R}{\'e}actifs ({MSR}'03)},
  year = {2003},
  editor = {M{\'e}ry, Dominique and Rezg, Nidhal and Xie, Xiaolan},
  pages = {431-445},
  address = {Metz, France},
  month = oct,
  publisher = {Herm{\`e}s},
  keywords = {protocol},
  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},
  year = {2005},
  volume = {3455/2005},
  series = {Lecture Notes in Computer Science},
  pages = {334-354},
  publisher = {Springer Berlin / Heidelberg},
  doi = {10.1007/11415787_20},
  keywords = {b method},
  owner = {cecile},
  timestamp = {2007.01.31},
  url = {http://www.springerlink.com/content/x8mcgk2p8r82e2gl/}
}

@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},
  address = {New York, NY, USA},
  doi = {http://doi.acm.org/10.1145/503272.503274},
  isbn = {1-58113-450-9},
  keywords = {CEGAR, refinment loop, model checking software},
  location = {Portland, Oregon},
  owner = {cecile},
  timestamp = {2007.01.14}
}

@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},
  series = {ACM Press},
  pages = {655--660},
  address = {New York, NY, USA},
  doi = {http://doi.acm.org/10.1145/240518.240642},
  isbn = {0-89791-779-0},
  location = {Las Vegas, Nevada, United States},
  owner = {cecile},
  timestamp = {2007.01.31}
}

@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},
  year = {2008},
  pages = {1--9},
  address = {Piscataway, NJ, USA},
  publisher = {IEEE Press},
  file = {:Cegar/worllevelSeqMemAbstrforMCbjesse08.pdf:PDF},
  isbn = {978-1-4244-2735-2},
  keywords = {Abstractions, Model-checking},
  location = {Portland, Oregon}
}

@TECHREPORT{prosyd05,
  author = {R. Bloem and B. Jobstmann and A. Pnueli.},
  title = {{Property-based Logic Synthesis for Rapid Design Prototyping}},
  institution = {Prosyd Deliverable D2.2/1},
  year = {2005},
  owner = {cecile},
  timestamp = {2007.02.07}
}

@ARTICLE{bozga97protocol,
  author = {M.~Bozga and J-C.~Fernandez and A.~Kerbrat and L.~Mounier},
  title = {Protocol {V}erification with the {ALD{\'E}BARAN} {T}oolset.},
  journal = {STTT},
  year = {1997},
  volume = {1},
  pages = {166-184},
  number = {1-2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://link.springer.de/link/service/journals/10009/bibs/7001001/70010166.htm},
  keywords = {model checking, model checker},
  publisher = {Springer}
}

@TECHREPORT{Brady:EECS-2008-136,
  author = {Brady, Bryan and Bryant, Randal and Seshia, Sanjit A.},
  title = {Abstracting RTL Designs to the Term Level},
  institution = {EECS Department, University of California, Berkeley},
  year = {2008},
  number = {UCB/EECS-2008-136},
  month = {Oct},
  abstract = {Term-level verification is a formal technique that seeks to verify
        RTL hardware descriptions by abstracting away details of data representations
        and operations. The key to making term-level verification automatic
        and efficient is in deciding what to abstract. We investigate this
        question in this paper and propose a solution based on the use of
        type qualifiers. First, we demonstrate through case studies that
        only selective term-level abstraction can be very effective in reducing
        the run-time of formal tools while still retaining precision of analysis.
        Second, the term-level abstraction process can be guided using lightweight
        type qualifiers. We present an annotation language and type inference
        scheme that is applied to the formal verification of the Verilog
        implementation of a chip multiprocessor router. Experimental results
        indicate type-based selective term-level abstraction is effective
        at scaling up verification with minimal designer guidance.},
  file = {:Abstraction/abstractingRTLtoTermLevel.pdf:PDF},
  keywords = {Abstraction, memory},
  owner = {cecile},
  timestamp = {2010.06.10},
  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},
  address = {LIP6/SOC},
  owner = {cecile},
  timestamp = {2007.04.16}
}

@TECHREPORT{cecile03dea,
  author = {C.~Braunstein},
  title = {{Transformation de propri\'et\'es CTL lors d'une m\'ethode de conception
        incr\'ementale des wrappers {VCI/PI}}},
  institution = {LIP6/ASIM},
  year = {2003},
  type = {Rapport de {DEA}},
  owner = {cecile},
  timestamp = {2006.09.07}
}

@ARTICLE{braunstein06sttt,
  author = {C.~Braunstein and E.~Encrenaz},
  title = {{CTL}-property {T}ransformations along an {I}ncremental {D}esign
        {P}rocess},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  year = {2007},
  volume = {9},
  pages = {77--88},
  number = {1},
  note = {A long version including the proof is available at www-asim.lip6.fr/~cecile},
  owner = {cecile},
  publisher = {Springer},
  timestamp = {2006.09.05}
}

@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},
  owner = {cecile},
  timestamp = {2007.03.27}
}

@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 \url{http://www.lix.polytechnique.fr/~hermann/LPAR2006/}},
  owner = {cecile},
  timestamp = {2007.03.27}
}

@TECHREPORT{Braunstein_Encrenaz_RR_LIP6_07_2006,
  author = {C.~Braunstein and E.~Encrenaz},
  title = {Using CTL formulae as component abstraction},
  institution = {UPMC/LIP6},
  year = {2006},
  type = {Research report},
  owner = {cecile},
  timestamp = {2006.09.29}
}

@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)},
  year = {2006},
  pages = {103--109},
  address = {Washington, DC, USA},
  publisher = {IEEE Computer Society},
  doi = {http://dx.doi.org/10.1109/RSP.2006.19},
  isbn = {0-7695-2580-6},
  owner = {cecile},
  timestamp = {2006.08.31}
}

@ARTICLE{avocs_incr,
  author = {C.~Braunstein and E.~Encrenaz},
  title = {{CTL}-{P}roperty {T}ransformations along an {I}ncremental {D}esign
        {P}rocess},
  journal = {Electronic Notes in Theoretical Computer Science},
  year = {2005},
  volume = {128},
  pages = {263--278},
  number = {6},
  file = {braunstein_avocs_o4.pdf:/dsk/l1/misc/Article/Concep_incr/Avocs/Avocs_paper/braunstein_avocs_o4.pdf:PDF},
  issue = {6},
  publisher = {Elsevier},
  series = {AVOCS'04~-~Proceedings of the 4th International Workshop on Automated
        Verification of Critical Systems}
}

@ARTICLE{browneclarkegrum88,
  author = {M.C.~Browne and E.M.~Clarke and O.~Grumberg},
  title = {Characterizing {F}inite {K}ripke {S}tructures in {P}ropositional
        {T}emporal {L}ogic},
  journal = {Theoritical Computer Science},
  year = {1988},
  volume = {59},
  pages = {115--131},
  number = {1-2},
  doi = {http://dx.doi.org/10.1016/0304-3975(88)90098-9},
  issn = {0304-3975},
  publisher = {Elsevier Science Publishers Ltd.}
}

@ARTICLE{Bryant86,
  author = {R.E.~Bryant},
  title = {{Graph-Based Algorithms for Boolean Function Manipulation}},
  journal = {IEEE Transactions on Computers},
  year = {1986},
  volume = {35},
  pages = {677-691},
  number = {8},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  keywords = {BDD},
  owner = {cecile},
  timestamp = {2006.11.07}
}

@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},
  editor = {H. Ehrig and B. J. Kr\"amer and A. Ertas},
  pages = {48},
  month = {June},
  organization = {Society of Design and Process Science},
  keywords = {protocol},
  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 {M}odel {C}hecking: $10^{20}$ {S}tates and {B}eyond},
  journal = {{I}nformation and {C}omputation },
  year = {1992},
  volume = {98},
  pages = {142--170},
  number = {2},
  note = {Special issue for best papers from LICS'90},
  address = {Duluth, MN, USA},
  publisher = {Academic Press, Inc.}
}

@INPROCEEDINGS{burch94automatic,
  author = {J.R.~Burch and D.L.~Dill},
  title = {Automatic {V}erification of {P}ipelined {M}icroprocessors {C}ontrol},
  booktitle = {Proceedings of the sixth International Conference on Computer-Aided
        Verification {CAV'94}},
  year = {1994},
  editor = {{D.L.~Dill}},
  volume = {LNCS 818},
  pages = {68--80},
  address = {Standford, California, USA},
  publisher = {Springer-Verlag},
  citeseerurl = {citeseer.ist.psu.edu/burch94automatic.html},
  keywords = {model checking, pipeline, archi},
  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},
  pages = {677--691},
  number = {8},
  month = {August},
  abstract = {Available}
}

@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},
  file = {:Composition/Speeding up MC by exploiting Explicit09.PDF:PDF},
  owner = {cecile},
  timestamp = {2009.04.30}
}

@INCOLLECTION{Cansell2001AbstractionandRefinementofFeatures,
  author = {D.~Cansell and D.~M{\'e}ry},
  title = {Abstraction and {R}efinement of {F}eatures},
  booktitle = {{Language Constructs for Designing Features}},
  publisher = {Springer-Verlag},
  year = {2001},
  editor = {S.~Gilmore and M.~Ryan},
  pages = {65--84},
  abstract = {The composition of services and features often leads to unwanted situations,
        because it is a non-monotonic operation over services and features.
        When a new service is added to an existing system, conditions have
        to be checked to ensure that the resulting system satisfies a list
        of required properties. Following the system approach of Abrial,
        we develop services and features in an incremental way and use refinement
        to model the composition of services and features. Proof obligations
        state the preservation or the non-preservation of properties, namely
        invariant or more generally safety properties. The method helps us
        in understanding when a service is interfering with another, and
        allows us to give multiple views of each service according to the
        level of its refinement. Finally, we validate our method with the
        Atelier B tool.}
}

@INCOLLECTION{cassez-proving,
  author = {F.~Cassez and M.~Ryan and P-Y.~Schobbens},
  title = {Proving {F}eature {N}on-{I}nteraction with {A}lternating-{T}ime {T}emporal
        {L}ogic},
  booktitle = {{Language Constructs for Describing Features}},
  publisher = {Springer Verlag},
  year = {2001},
  editor = {S.~Gilmore and M.~Ryan},
  pages = {85--104}
}

@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},
  pages = {371-408},
  number = {4},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/990010.990011},
  file = {chechik03a.pdf:/dsk/l1/misc/doc/abstraction/chechik03a.pdf:PDF},
  keywords = {abstraction, 3-valued, 4-valued, logic, model checking}
}

@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},
  year = {2000},
  pages = {453},
  address = {Washington, DC, USA},
  publisher = {IEEE Computer Society},
  isbn = {0-7695-0801-4},
  keywords = {AMBA}
}

@INPROCEEDINGS{CLS00,
  author = {G. Ciardo and G. L\"uttgen and R. Siminiceanu},
  title = {Efficient Symbolic State-Space Construction for Asynchronous Systems},
  booktitle = {Proc. of ICATPN'2000},
  year = {2000},
  volume = {1825},
  series = {Lecture Notes in Computer Science},
  pages = {103--122},
  publisher = {Springer Verlag}
}

@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},
  pages = {410-425},
  number = {4},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://link.springer.de/link/service/journals/10009/bibs/0002004/00020410.htm}
}

@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},
  pages = {7},
  number = {1},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/1838552.1838559}
}

@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},
  journal = {ACM Transactions on Programming Languages and Systems},
  year = {1986},
  volume = {8},
  pages = {244--263},
  number = {2},
  booktitle = {ICATPN'02: Proceedings of the 23rd International Conference on Applications
        and Theory of Petri Nets},
  doi = {http://doi.acm.org/10.1145/5397.5399},
  issn = {0164-0925},
  publisher = {ACM Press}
}

@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},
  year = {1994},
  volume = {16},
  pages = {1512--1542},
  number = {5},
  address = {New York, NY, USA},
  doi = {http://doi.acm.org/10.1145/186025.186051},
  issn = {0164-0925},
  keywords = {model cheking, abstraction, CTL, preservation},
  publisher = {ACM Press}
}

@BOOK{clarke99model,
  title = {Model Checking},
  publisher = {The {MIT} {P}ress},
  year = {1999},
  author = {E.M.~Clarke and O.~Grumberg and D.A.~Peled},
  address = {Cambridge, Massachusetts},
  isbn = {0-262-03270-8},
  keywords = {CTL,LTL, model checking,kripke structure, simulation}
}

@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},
  pages = {752-794},
  number = {5},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/876638.876643},
  file = {:Cegar/Counterexample-guided abstraction refinement.pdf:PDF},
  keywords = {abstraction, CEGAR},
  owner = {cecile},
  timestamp = {2006.06.27}
}

@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},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/217474.217565}
}

@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},
  pages = {1113-1123},
  number = {7},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.ieeecomputersociety.org/10.1109/TCAD.2004.829807},
  file = {:Cegar/SATBasedCegar2004Clarke.pdf:PDF},
  keywords = {CEGAR,SAT},
  owner = {cecile},
  timestamp = {2010.06.03}
}

@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},
  howpublished = {Available on: \url{http://www.grappa.univ-lille3.fr/tata}},
  year = {1997},
  note = {release October, 1rst 2002},
  file = {tata.pdf:/dsk/l1/misc/doc/automate/tata.pdf:PDF},
  keywords = {tree automata}
}

@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},
  editor = {T.~Knight and J.~Savage},
  pages = {113--128},
  month = {March},
  abstract = { This paper presents how prime implicants and essential prime implicants
        can be computed by means of meta-products encoded with of BDD's.
        It gives the equations that mimic the definitions, but it does not
        propose a recursive algorithm. The variable ordering is discussed
        and experimental results are provided that come from a benchmark
        of circuits. },
  keywords = {Prime Implicants}
}

@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},
  address = {Munich, Germany},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  keywords = {abstraction},
  owner = {cecile},
  timestamp = {2007.01.13}
}

@INPROCEEDINGS{jmc-ag-djs:ddd,
  author = {J.M.~Couvreur and A.~Griffault and D.J.~Sherman},
  title = {Diagrammes de d\'ecision pour la v\'erification de r\'eseaux \`a
        files},
  booktitle = {Mod\'elisation de syst\`emes r\'eactifs (MSR'99)},
  year = {1999},
  address = {ENS Cachan},
  month = {March}
}

@INPROCEEDINGS{CA94,
  author = {J.M. Couvreur and E. Paviot-Adet},
  title = {New Structural Invariants for {P}etri Nets Analysis},
  booktitle = {Proc. of ICATPN'94},
  year = {1994},
  volume = {815},
  series = {Lecture Notes in Computer Science},
  pages = {199--218},
  publisher = {Springer Verlag}
}

@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},
  year = {1997},
  volume = {19},
  pages = {253--291},
  number = {2},
  address = {New York, NY, USA},
  doi = {http://doi.acm.org/10.1145/244795.244800},
  issn = {0164-0925},
  keywords = {abstraction},
  publisher = {ACM Press}
}

@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},
  year = {2008},
  pages = {93-98},
  month = {July},
  doi = {10.1109/IOLTS.2008.59},
  journal = {On-Line Testing Symposium, 2008. IOLTS '08. 14th IEEE International},
  keywords = {fault tolerance, fault trees, reduced instruction set computing, temporal
        logicbinary image, multicycle RISC processor, program image. shadow,
        symbolic simulation, transient fault injection}
}

@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},
  file = {rap_stage_duret_lutz_2003.pdf:/dsk/l1/misc/doc/ltl_auto/rap_stage_duret_lutz_2003.pdf:PDF},
  keywords = {LTL, automata approach},
  owner = {cecile},
  timestamp = {2006.02.13}
}

@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},
  editor = {ACM},
  pages = {411-420},
  address = {Los Angeles, CA, USA},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://portal.acm.org/citation.cfm?id=302405.302672},
  keywords = {CTL , patterns , Specification},
  url = {http://patterns.projects.cis.ksu.edu/collaborations/papers.shtml}
}

@ARTICLE{DBLP:journals/tcad/FeySBD08,
  author = {G{\"o}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},
  pages = {1138-1149},
  number = {6},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1109/TCAD.2008.923234}
}

@ARTICLE{fitting91bilattices,
  author = {M.~Fitting},
  title = {{Bilattices and the Semantics of Logic Programming.}},
  journal = {Journal of Logic Programming},
  year = {1991},
  volume = {11},
  pages = {91-116},
  number = {1{\&}2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  file = {BilSemLP.pdf:/dsk/l1/misc/doc/logique/BilSemLP.pdf:PDF},
  keywords = {4-valued, logic, 3-valued},
  owner = {cecile},
  timestamp = {2006.04.05}
}

@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},
  year = {2003},
  pages = {206--222},
  address = {London, UK},
  publisher = {Springer-Verlag},
  file = {vmcai2003.ps:/dsk/l1/misc/doc/logique/vmcai2003.ps:PDF},
  isbn = {3-540-00348-7},
  keywords = {3-valued, logic, model checking, Kripke structure}
}

@INPROCEEDINGS{goelL00formal,
  author = {A.~Goel and W.~R.~Lee},
  title = {{{F}ormal {V}erification of an {IBM} {C}ore{C}onnect {P}rocessor
        {L}ocal {B}us {A}rbiter {C}ore}},
  booktitle = {DAC'00: Proceedings of the 37th Conference on Design Automation},
  year = {2000},
  editor = {ACM},
  pages = {196-200},
  address = {Los Angeles, CA, USA},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/337292.337384},
  file = {p196-goel.pdf:/dsk/l1/misc/doc/verif_archi/rulebase/p196-goel.pdf:PDF},
  keywords = {CTL, model checking, Rulebase},
  owner = {cecile},
  timestamp = {2006.06.29}
}

@INPROCEEDINGS{GL91,
  author = {O.~Grumberg and D.E.~Long},
  title = {Model {C}hecking and {M}odular {V}erification},
  booktitle = {International Conference on Concurrency Theory},
  year = {1991},
  volume = {527},
  series = {Lecture Notes in Computer Science},
  pages = {250--263},
  publisher = {Springer Verlag},
  file = {p843-grumberg.pdf:/dsk/l1/misc/doc/modular/model_checking/p843-grumberg.pdf:PDF},
  keywords = {simulation,CTL, modular}
}

@ARTICLE{Gupta92syrvey,
  author = {A.~Gupta},
  title = {{Formal Hardware Verification Methods: A Survey.}},
  journal = {Formal Methods in System Design},
  year = {1992},
  volume = {1},
  pages = {151-238},
  number = {2/3},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  keywords = {survey, hardware, formal verification}
}

@INPROCEEDINGS{henzinger99dsp,
  author = {T.~A.~Henzinger and X.~Liu and S.~Qadeer and S.~K.~Rajamani},
  title = {Formal {S}pecification and {V}erification of a {D}ataflow {P}rocessor
        {A}rray.},
  booktitle = {I{CCAD}'99: {P}roceedings of the 1999 {IEEE}/{ACM} {I}nternational
        {C}onference on {C}omputer-{A}ided {D}esign},
  year = {1999},
  editor = {Jacob K. White, Ellen Sentovich},
  pages = {494-499},
  address = {San Jose, USA},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://portal.acm.org/citation.cfm?id=339492.340066},
  file = {formal_specification_and_verification_of_a_dataflow_processor_array.pdf:/dsk/l1/misc/doc/modular/mocha/formal_specification_and_verification_of_a_dataflow_processor_array.pdf:PDF},
  keywords = {abstraction, assume-guarantee, ATL, modular, archi, MOCHA}
}

@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},
  year = {2000},
  pages = {245--253},
  address = {San Jose, California},
  publisher = {IEEE Press},
  file = {decomposing00henzinger.pdf:/dsk/l1/misc/doc/modular/assume/decomposing00henzinger.pdf:PDF},
  isbn = {0-7803-6448-1}
}

@INPROCEEDINGS{C:HJMS03,
  author = {Henzinger, T.A. and Jhala, R. and Majumdar, R. and Sutre, G.},
  title = {Software {V}erification with {BLAST}},
  booktitle = {SPIN'2003: Proceedings of the 10th International SPIN Workshop},
  year = {2003},
  volume = {2648},
  series = {Lecture Notes in Computer Science},
  pages = {235--239},
  address = {USA},
  publisher = {Springer},
  note = {Tool paper},
  keywords = {software, model-checking},
  url = {http://www.labri.fr/publications/mvtsi/2003/HJMS03}
}

@INPROCEEDINGS{henzinger98you,
  author = {T.A.~Henzinger and S.~Qadeer and S.K.~Rajamani},
  title = {{Y}ou {A}ssume, {W}e {G}uarantee: {M}ethodology and {C}ase {S}tudies},
  booktitle = {C{AV}'98: {P}roceedings of the 10th {I}nternational {C}onference
        on {C}omputer {A}ided {V}erification},
  year = {1998},
  editor = {Alan J. Hu, Moshe Y. Vardi},
  volume = {1427},
  series = {Lecture Notes in Computer Science},
  pages = {440--451},
  address = {Vancouver, Canada},
  publisher = {Springer-Verlag},
  file = {henzinger98you.ps.gz:/dsk/l1/misc/doc/modular/assume/henzinger98you.ps.gz:PDF}
}

@ARTICLE{henzinger02anassume,
  author = {T.A.~Henzinger and S.~Qadeer and S.K.~Rajamani and S.~Tasiran},
  title = {An {A}ssume-{G}uarantee {R}ule for {C}hecking {S}imulation},
  journal = {ACM Transactions on Programming Languages Systems},
  year = {2002},
  volume = {24},
  pages = {51--64},
  number = {1},
  address = {New York, NY, USA},
  doi = {http://doi.acm.org/10.1145/509705.509707},
  file = {henzinger98assumeguarantee.ps:/dsk/l1/misc/doc/modular/assume/henzinger98assumeguarantee.ps:PDF},
  issn = {0164-0925},
  publisher = {ACM Press}
}

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

@INPROCEEDINGS{hosabettu98decomposing,
  author = {R.~Hosabettu and M.~Srivas and G.~Gopalakrishnan},
  title = {Decomposing the {P}roof of {C}orrectness of {P}ipelined {M}icroprocessors},
  booktitle = {Computer-Aided Verification, {CAV'98}},
  year = {1998},
  editor = {Alan J. Hu and Moshe Y. Vardi},
  volume = {1427},
  pages = {122--134},
  address = {Vancouver, Canada},
  publisher = {Springer-Verlag},
  url = {citeseer.ist.psu.edu/208243.html}
}

@ARTICLE{huggins98spec,
  author = {J.K.~Huggins and D.~Van Campenhout},
  title = {Specification and {V}erification of {P}ipelining in the {ARM2 RISC}
        {M}icroprocessor},
  journal = {ACM Transactions on Design Automation of Electronic Systems},
  year = {1998},
  volume = {3},
  pages = {563--580},
  number = {4},
  address = {New York, NY, USA},
  doi = {http://doi.acm.org/10.1145/296333.296345},
  issn = {1084-4309},
  publisher = {ACM Press}
}

@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},
  pages = {903-917},
  number = {7},
  month = {July}
}

@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},
  pages = {366-379},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1109/TCAD.2007.907270},
  file = {:Cegar/WLPredicateAbstractionRefinment08.pdf:PDF},
  keywords = {Cegar, predicate abstraction, SAT}
}

@INPROCEEDINGS{kroening07vcegar,
  author = {H.~Jain and D.~Kroening and N.~Sharygina and E.~Clarke},
  title = {{{VCEGAR}: Verilog CounterExample Guided Abstraction Refinement}},
  booktitle = {T{ACAS}'07: {P}roceedings of the 13th {I}nternational {C}onference
        on {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis
        of {S}ystems},
  year = {2007},
  note = {Accepted paper},
  owner = {cecile},
  timestamp = {2007.02.07}
}

@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},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  keywords = {survey, hadware, formal veriication}
}

@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},
  pages = {189-203},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  file = {kaluzhny93knowledge.pdf:/dsk/l1/misc/doc/logique/kaluzhny93knowledge.pdf:PDF},
  keywords = {CTL , abstraction , 3-valued , refinment loop},
  owner = {cecile},
  timestamp = {2006.04.03}
}

@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},
  year = {2003},
  pages = {840--843},
  address = {New York,USA},
  publisher = {ACM},
  doi = {http://doi.acm.org/10.1145/775832.776043},
  file = {:BMC/kang03satunbounded.pdf:PDF;:BMC/Park05satUnbound.pdf:PDF},
  isbn = {1-58113-688-9},
  keywords = {SAT, all-sat},
  location = {Anaheim, CA, USA}
}

@ARTICLE{Kern99survey,
  author = {C.~Kern and M.R.~Greenstreet},
  title = {Formal {V}erification in {H}ardware {D}esign: a {S}urvey},
  journal = {ACM Transactions on Design Automation of Electronic Systems},
  year = {1999},
  volume = {4},
  pages = {123--193},
  number = {2},
  address = {New York, NY, USA},
  doi = {http://doi.acm.org/10.1145/307988.307989},
  issn = {1084-4309},
  keywords = {survey, hadware, formal veriication},
  publisher = {ACM Press}
}

@BOOK{kleene52introduction,
  title = {Introduction to Metamathematics},
  publisher = {North-Holland},
  year = {1952},
  author = {Kleene, S.},
  series = {Bibliotheca mathematica},
  owner = {cecile},
  timestamp = {2006.04.27}
}

@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},
  address = {Santa Clara, USA}
}

@INPROCEEDINGS{kroening01automated,
  author = {D.~Kroening and W.J.~Paul},
  title = {Automated {P}ipeline {D}esign},
  booktitle = {DAC '01: Proceedings of the 38th conference on Design Automation},
  year = {2001},
  pages = {810--815},
  publisher = {ACM Press},
  doi = {http://doi.acm.org/10.1145/378239.379071},
  isbn = {1-58113-297-2},
  location = {Las Vegas, Nevada, United States}
}

@BOOK{kropf99introduction,
  title = {Introduction to Formal Hardware Verification},
  publisher = {Springer Verlag},
  year = {1999},
  author = {T.~Kropf},
  address = {Secaucus, NJ, USA},
  isbn = {3540654453},
  keywords = {survey, hardware},
  owner = {cecile},
  timestamp = {2006.11.07}
}

@ARTICLE{KupfermanG96branching,
  author = {O.~Kupferman and O.~Grumberg},
  title = {Branching-Time Temporal Logic and Tree Automata.},
  journal = {Information and Computation},
  year = {1996},
  volume = {125},
  pages = {62-69},
  number = {1},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  file = {branchingand automata.ps:/dsk/l1/misc/doc/ctl_auto/branchingand automata.ps:PDF},
  keywords = {CTL, tree automata ,model checking, automata approach}
}

@ARTICLE{KupfermanVW00automata,
  author = {O.~Kupferman and M.Y.~Vardi and P.~Wolper},
  title = {An {A}utomata-{T}heoretic {A}pproach to {B}ranching-{T}ime {M}odel
        {C}hecking.},
  journal = {Journal of the ACM},
  year = {2000},
  volume = {47},
  pages = {312-360},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/333979.333987},
  file = {an-automata-theoretic-approach.pdf:/dsk/l1/misc/doc/automate/an-automata-theoretic-approach.pdf:PDF},
  keywords = {tree automata, CTL, automata approach},
  owner = {cecile},
  timestamp = {2006.06.27}
}

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

@BOOK{Lano,
  title = {The {B} {L}anguage and {M}ethod, {A} {G}uide to {P}ractical {F}ormal
        {D}evelopment},
  publisher = {Springer-Verlag},
  year = {1996},
  author = {K.~Lano},
  series = {FACIT},
  address = {UK},
  keywords = {b method}
}

@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},
  year = {1995},
  pages = {17--40},
  address = {London, UK},
  publisher = {Springer-Verlag},
  isbn = {3-540-60630-0}
}

@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},
  pages = {143-155},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1007/s10009-004-0169-2},
  file = {:Cegar/Li04PureSatSTTT.pdf:PDF},
  keywords = {CEGAR, SAT}
}

@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},
  year = {1991},
  pages = {81--85},
  address = {Washington, DC, USA},
  publisher = {IEEE Computer Society},
  isbn = {0-8186-2270-9}
}

@ARTICLE{Loiseaux,
  author = {C.~Loiseaux and S.~Graf and J.~Sifakis and A.~Bouajjani and S.~Bensalem},
  title = {Property {P}reserving {A}bstractions for the {V}erification of {C}oncurrent
        {S}ystems},
  journal = {Formal Methods in System Design},
  year = {1995},
  volume = {6},
  pages = {11--44},
  number = {1},
  address = {Hingham, MA, USA},
  publisher = {Kluwer Academic Publisher}
}

@PHDTHESIS{long93thesis,
  author = {D.~E.~Long},
  title = {Model {C}hecking, {A}bstraction, and {C}ompositional {V}erification},
  school = {Carnegie Mellon University},
  year = {1993},
  file = {long93model.ps.gz:/dsk/l1/misc/doc/modular/model_checking/long93model.ps.gz:PDF},
  keywords = {abstraction, CTL, modular, simulation, model checking},
  owner = {cecile},
  timestamp = {2006.03.08}
}

@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},
  month = {November},
  note = {Santa Clara CA, USA},
  abstract = { This paper proposes two heuristics for variable ordering based on
        the topology of the circuit under study. \begin{enumerate} \item
        One defines the level of a variable or a gate as follows: $level(root)=0$
        and $level(f)=max(level(g))+1$, where the $g$'s are the fathers of
        $f$. The first heuristics consists in indexing the variables according
        to the decreasing order of their levels. The justification is that
        the influence of variables high in the circuit must be computed as
        soon as possible. \item Same as the previous heuristics but respecting
        modules. Modules are treated in the decreasing order of their depths.
        The depth of a formula being the maximum depth of its variables.
        \end{enumerate} Experimental results are reported, showing that the
        second heuristics is very good (on the ICSAS'85 benchmark). Lu },
  keywords = {Variable ordering heuristics, Combinatorial Circuits}
}

@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},
  year = {2000},
  pages = {161--178},
  publisher = {Springer-Verlag},
  url = {citeseer.ist.psu.edu/426677.html}
}

@INPROCEEDINGS{manolios04web,
  author = {P.~Manolios and S.K.~Srinivasan},
  title = {Automatic {V}erification of {S}afety and {L}iveness for {XS}cale-{L}ike
        {P}rocessor {M}odels {U}sing {WEB} Refinements},
  booktitle = {DATE '04: Proceedings of the conference on Design, Automation and
        Test in Europe},
  year = {2004},
  pages = {168-174},
  address = {Washington, DC, USA},
  publisher = {IEEE Computer Society},
  isbn = {0-7695-2085-5-1}
}

@INPROCEEDINGS{Mariano2002formalization,
  author = {G.~Mariano and J-L.~Boulanger and A. Aljer},
  title = {Formalization of {D}igital {C}ircuits {U}sing the {B} {M}ethod},
  booktitle = {Comp{R}ail {VIII}: 8th {I}nternational {C}onference on {C}omputer
        {A}ided {D}esign, {M}anufacture and {O}peration in the {R}ailway
        and other {A}dvanced {M}ass {T}ransit {S}ystems},
  year = {2002},
  address = {Lemnos, Greece},
  month = {12 - 14 } # jun,
  keywords = {B method, formal development, software verification, safety-critical
        applications, VHDL, BHDL, Hardware},
  url = {http://www.wessex.ac.uk/conferences/2002/cr02/}
}

@INPROCEEDINGS{Silva00Sat,
  author = {Marques-Silva, Jo\, {a}o P. and Sakallah, Karem A.},
  title = {Boolean satisfiability in electronic design automation},
  booktitle = {DAC '00: Proceedings of the 37th Annual Design Automation Conference},
  year = {2000},
  pages = {675--680},
  address = {New York, NY, USA},
  publisher = {ACM},
  doi = {http://doi.acm.org/10.1145/337292.337611},
  file = {:SAT/p675-marques-silva.pdf:PDF},
  isbn = {1-58113-187-9},
  keywords = {SAT, circuit},
  location = {Los Angeles, California, United States},
  owner = {cecile},
  timestamp = {2009.11.30}
}

@ARTICLE{mcmillan00methodology,
  author = {K.L. McMillan},
  title = {A {M}ethodology for {H}ardware {V}erification {U}sing {C}ompositional
        {M}odel {C}hecking},
  journal = {Science of Computer Programming},
  year = {2000},
  volume = {37},
  pages = {279--309},
  number = {1--3},
  file = {mcmillan99methodology.pdf:/dsk/l1/misc/doc/modular/assume/mcmillan99methodology.pdf:PDF},
  keywords = {CTL, LTL, model checking, modular, composition, assume-guarantee},
  url = {citeseer.ist.psu.edu/mcmillan99methodology.html}
}

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

@PHDTHESIS{memmi:thesis,
  author = {G.~Memmi},
  title = {M\'ethodes d'analyse des r\'eseaux de Petri, r\'eseaux \`a files
        et application aux syst\`emes temps-r\'eel},
  school = {Universit\'e Paris-6},
  year = {1983}
}

@BOOK{Mil89,
  title = {Communication and {C}oncurrency},
  publisher = {Prentice Hall},
  year = {1989},
  author = {R.~Milner},
  series = {International series in computer science},
  address = {Upper Saddle River, USA},
  isbn = {0-13-115007-3}
}

@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},
  adress = {London, UK},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  editors = {D. C. Cooper},
  keywords = {simulation, bisimulation}
}

@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},
  editor = {L.J.M Claesen},
  pages = {52--57},
  month = {June},
  abstract = { This paper is the first one in which management of BDD nodes via
        a hash table is proposed (and thus the reduction operation is suppressed).
        Then, various labelling of edges are discussed: first, the flag $+/-$
        already proposed by Billon and Madre \cite{Bil87,MB88}. Second, another
        flag so-called input inverter, is proposed. It transforms $ite(x,F,G)$
        into $ite(\neg x,F,G)=ite(x,G,F)$. Canonicity is maintained by keeping
        only nodes such that $F<G$ (for say the memory order). Third, labelling
        edges with shifts between variable indices is proposed. Fourth, it
        is proposed to encode small BDD's (with only two variables) by means
        of a single word. Then, a variable ordering heuristics is proposed.
        It consists in propagating a flow from the outputs to the inputs
        of the circuits and labelling inputs by the order of their flow values.
        The flow at each input is $1.0$, the flow at a gate is the sum of
        its in-flow. Its is shared equally by its parents. Then, A way to
        manage {\em don't care} parts of circuits is proposed. It consists
        in using a second variable $\neg x_1 \wedge \neg x_2 \rightarrow
        \neg x$, $x_1 \wedge x_2 \rightarrow x$, otherwise {\em don't care}.
        Finally, experimental results are reported. },
  keywords = {BDD encoding, Heuristics for variable ordering}
}

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

@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},
  pages = {2638-2649},
  number = {12},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1109/TCAD.2006.882592}
}

@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},
  eid = {Princeton University Press},
  owner = {cecile},
  timestamp = {2006.09.04}
}

@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},
  pages = {2-14},
  number = {1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@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},
  pages = {73--104},
  number = {2-3},
  doi = {10.1007/s10617-006-9044-6},
  owner = {cecile},
  timestamp = {2007.01.31}
}

@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{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},
  year = {2000},
  volume = {1855},
  series = {Lecture Notes In Computer Science},
  pages = {435--449},
  address = {London, UK},
  publisher = {Springer-Verlag},
  file = {auto_abstra.ps:/dsk/l1/misc/doc/ctl_auto/auto_abstra.ps:PDF},
  keywords = {abstraction, model checking},
  owner = {cecile},
  timestamp = {2006.02.03}
}

@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},
  pages = {458-487},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/201019.201032}
}

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

@MANUAL{PI_proto,
  title = {{OMI324: {PI}-{B}us {S}tandard {S}pecification}},
  author = {{Open Microprocessors System Initiatives}},
  organization = {Siemens},
  address = {Munich, Germany},
  year = {1994},
  file = {Pidoc31.pdf:/dsk/l1/misc/doc/archi/Pidoc31.pdf:PDF}
}

@TECHREPORT{specamba03,
  author = {J.~{Ossima Kh\'eba}},
  title = {Sp\'ecification des {W}rappers {AHB}/{VCI}},
  institution = {LIP6 dept. ASIM},
  year = {2003},
  type = {Rapport de {DEA}},
  owner = {cecile},
  school = {{Universit\'ee} {Pierre} et {Marie} {Curie}},
  timestamp = {2006.09.07}
}

@TECHREPORT{joel02,
  author = {J.~{Ossima Kh\'eba}},
  title = {Les {W}rappers {PI}/{VCI} et {E}tude de {F}aisabilit\'e des {W}rappers
        {AMBA}/{VCI}},
  institution = {LIP6 dept. ASIM},
  year = {2002},
  type = {Rapport de stage},
  owner = {cecile},
  school = {{Universit\'ee} {Pierre} et {Marie} {Curie}},
  timestamp = {2006.09.07}
}

@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)},
  year = {1992},
  editor = {Deepak Kapur},
  volume = {607},
  series = {Lecture Notes in Artificial Intelligence},
  pages = {748--752},
  address = {Saratoga, {NY}},
  month = {jun},
  publisher = {Springer-Verlag},
  url = {http://www.csl.sri.com/papers/cade92-pvs/}
}

@INPROCEEDINGS{pasareanu99assume,
  author = {C.S.~Pasareanu and M.B.~Dwyer and M.~Huth},
  title = {Assume-{G}uarantee {M}odel {C}hecking of {S}oftware: {A} {C}omparative
        {C}ase {S}tudy},
  booktitle = {Proceedings of the 5th and 6th International SPIN Workshops on Theoretical
        and Practical Aspects of SPIN Model Checking},
  year = {1999},
  pages = {168--183},
  address = {London, UK},
  publisher = {Springer-Verlag},
  isbn = {3-540-66499-8}
}

@INPROCEEDINGS{passerone02convertibility,
  author = {R.~Passerone and L.~de Alfaro and T.A.~Henzinger and A.L.~Sangiovanni-Vincentelli},
  title = {Convertibility {V}erification and {C}onverter {S}ynthesis: {T}wo
        {F}aces of {T}he {S}ame {C}oin},
  booktitle = {I{CCAD} '02: {P}roceedings of the 2002 {IEEE}/{ACM} {I}nternational
        {C}onference on {C}omputer-{A}ided {D}esign},
  year = {2002},
  pages = {132--139},
  address = {New York, USA},
  publisher = {ACM Press},
  doi = {http://doi.acm.org/10.1145/774572.774592},
  file = {samecoin.pdf:/dsk/l1/misc/doc/interface/samecoin.pdf:PDF},
  isbn = {0-7803-7607-2},
  location = {San Jose, California}
}

@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},
  adress = {San Francico, USA},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/277044.277047},
  file = {samecoin.pdf:/dsk/l1/misc/doc/interface/samecoin.pdf:PDF},
  keywords = {interface, wrapper}
}

@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},
  year = {1994},
  volume = {815},
  series = {Lecture Notes in Computer Science},
  pages = {416--435},
  publisher = {Springer Verlag}
}

@BOOK{hennessypattersonbook,
  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},
  author = {D.A.~Patterson and J.L~Hennessy},
  edition = {third},
  month = {August},
  abstract = {{In addition to thoroughly updating every aspect of the text to reflect
        the most current computing technology, the third edition<br><br>*Uses
        standard 32-bit MIPS 32 as the primary teaching ISA.<br>*Presents
        the assembler-to-HLL translations in both C and Java.<br>*Highlights
        the latest developments in architecture in Real Stuff sections:<br><br>+
        Intel IA-32<br>+ Power PC 604<br>+ Googles PC cluster<br>+ Pentium
        P4<br>+ SPEC CPU2000 benchmark suite for processors<br>+ SPEC Web99
        benchmark for web servers<br>+ EEMBC benchmark for embedded systems<br>+
        AMD Opteron memory hierarchy<br>+ AMD vs. 1A-64<br><br><br><b>New
        support for distinct course goals</b><br><br>Many of the adopters
        who have used our book throughout its two editions are refining their
        courses with a greater hardware or software focus. We have provided
        new material to support these course goals:<br><br><i>New material
        to support a Hardware Focus</i><br><br>+Using logic design conventions<br>+Designing
        with hardware description languages<br>+Advanced pipelining<br>+Designing
        with FPGAs<br>+HDL simulators and tutorials<br>+Xilinx CAD tools<br><br><i>New
        material to support a Software Focus</i><br><br>+How compilers Work<br>+How
        to optimize compilers<br>+How to implement object oriented languages<br>+MIPS
        simulator and tutorial<br>+History sections on programming languages,
        compilers, operating systems and databases<br><br><i><b>Whats New
        in the Third Edition</b></i><br><br><b>New pedagogical features</b><br><br><i>Understanding
        Program Performance</i> <br>-Analyzes key performance issues from
        the programmers perspective <br><br><i>Check Yourself Questions</i>
        <br>-Helps students assess their understanding of key points of a
        section <br><br><i>Computers In the Real World</i> <br>-Illustrates
        the diversity of applications of computing technology beyond traditional
        desktop and servers<br><br><i>For More Practice</i><br>-Provides
        students with additional problems they can tackle<br><br><i>In More
        Depth</i> <br>-Presents new information and challenging exercises
        for the advanced student<br><br><br><b>New reference features</b><br><br>Highlighted
        glossary terms and definitions appear on the book page, as bold-faced
        entries in the index, and as a separate and searchable reference
        on the CD.<br><br>A complete index of the material in the book and
        on the CD appears in the printed index and the CD includes a fully
        searchable version of the same index.<br><br>Historical Perspectives
        and Further Readings have been updated and expanded to include the
        history of software R\&D.<br><br>CD-Library provides materials collected
        from the web which directly support the text.<br><br><b>On the CD</b><br><br>CD-Bars:
        Full length sections that are introduced in the book and presented
        on the CD<br><br>CD-Appendixes: The entire set of appendixes<br><br>CD-Library:
        Materials collected from the web which directly support the text<br><br>CD-Exercises:
        <i>For More Practice</i> provides exercises and solutions for self-study<br><i>In
        More Depth</i> presents new information and challenging exercises
        for the advanced or curious student<br> <br>Glossary: Terms that
        are defined in the text are collected in this searchable reference<br><br>Further
        Reading: References are organized by the chapter they support<br><br>Software:
        HDL simulators, MIPS simulators, and FPGA design tools<br><br>Tutorials:
        SPIM, Verilog, and VHDL<br><br>Additional Support: Processor Models,
        Labs, Homeworks, Index covering the book and CD contents<br><br><b>Instructor
        Support</b><br><br>+ Instructor Support is provided in a password-protected
        site to adopters who request the password from our sales representative<br>+
        Solutions to all the exercises <br>+ Figures from the book in a number
        of formats<br>+ Lecture slides prepared by the authors and other
        instructors<br>+ Lecture notes<br><br><b>For instructor resources
        click on the grey "companion site" button found on the right side
        of this page.</B><br>This new edition represents a major revision.
        <br>New to this edition:<br><br>* Entire Text has been updated to
        reflect new technology<br>* 70% new exercises.<br>* Includes a CD
        loaded with software, projects and exercises to support courses using
        a number of tools <br>* A new interior design presents defined terms
        in the margin for quick reference <br>* A new feature, Understanding
        Program Performance focuses on performance from the programmers perspective
        <br>* Two sets of exercises and solutions, For More Practice and
        In More Depth, are included on the CD <br>* Check Yourself questions
        help students check their understanding of major concepts <br>* Computers
        In the Real World feature illustrates the diversity of uses for information
        technology <br>*More detail below...}},
  citeulike-article-id = {808853},
  howpublished = {Paperback},
  isbn = {1558606041},
  keywords = {pipeline,processor},
  priority = {2},
  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},
  owner = {cecile},
  timestamp = {2007.01.09}
}

@ARTICLE{peng03comparison,
  author = {H.~Peng and S.~Tahar and F.~Khendek},
  title = {Comparison of {SPIN} and {VIS} for {P}rotocol {V}erification.},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  year = {2003},
  volume = {4},
  pages = {234-245},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1007/s100090200073},
  publisher = {Springer}
}

@INPROCEEDINGS{omi95rsp,
  author = {V. Pevtschin},
  title = {The {O}pen {M}icroprocessor {S}ystems {I}nitiative: {A} {S}trategy
        {T}owards {I}ntegrated {S}ystem {D}esign},
  booktitle = {R{SP}'95: {P}roceddings of the 6th {IEEE} {I}nternational {W}orkshop
        on {R}apid {S}ystem {P}rototyping},
  year = {1995},
  pages = {2--11},
  doi = {http://doi.ieeecomputersociety.org/10.1109/IWRSP.1995.518564},
  owner = {cecile},
  timestamp = {2007.02.19}
}

@INPROCEEDINGS{plath99sfi,
  author = {M.C.~Plath and M.D.~Ryan},
  title = {S{FI}: a {F}eature {I}ntegration {T}ool},
  booktitle = {Tool Support for System Specification, Development and Verification},
  year = {1999},
  editor = {R. Berghammer and Y. Lakhnech},
  series = {Advances in Computing Science},
  pages = {201--216},
  publisher = {Springer},
  file = {plath99sfi.ps:/dsk/l1/misc/doc/telecom/plath99sfi.ps:PDF},
  keywords = {feature}
}

@ARTICLE{plath01feature,
  author = {M.~Plath and M.~Ryan},
  title = {Feature {I}ntegration using a {F}eature {C}onstruct},
  journal = {Science of Computer Programming},
  year = {2001},
  volume = {41},
  pages = {53--84},
  number = {1},
  address = {Amsterdam, The Netherlands},
  doi = {http://dx.doi.org/10.1016/S0167-6423(00)00018-6},
  issn = {0167-6423},
  publisher = {Elsevier North-Holland, Inc.}
}

@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},
  file = {:Cegar/Strenghtening Properties Using AR 09.PDF:PDF},
  owner = {cecile},
  timestamp = {2009.04.30}
}

@MASTERSTHESIS{fredHDR,
  author = {P{\'e}trot, F.},
  title = {Int{\'e}gration des syst{\`e}mes mat{\'e}riel/logiciel},
  school = {Universit{\'e}e Pierre et Marie Curie},
  year = {2003},
  type = {Habilitation {\`a} Diriger des Recherches},
  owner = {cecile},
  timestamp = {2007.02.03}
}

@BOOK{rasiowa78algebra,
  title = {An Algebraic Approach to Non-Classicals Logis},
  year = {1978},
  editor = {Studies in Logics and the Foundations of Mathematics},
  author = {H.~Rasiowa},
  address = {Amsterdam},
  owner = {cecile},
  timestamp = {2006.05.15}
}

@INPROCEEDINGS{sawada97trace,
  author = {J.~Sawada and W.A.~Hunt},
  title = {Trace {T}able {B}ased {A}pproach for {P}ipeline {M}icroprocessor
        {V}erification},
  booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer
        Aided Verification},
  year = {1997},
  pages = {364--375},
  address = {London, UK},
  publisher = {Springer-Verlag LNCS 1254},
  isbn = {3-540-63166-6}
}

@INPROCEEDINGS{eveking06fdl,
  author = {M.~Schickel and V.~Nimbler and M.~Braun and H.~Eveking},
  title = {On {C}onsistency and {C}ompletness of {P}roperty-{S}ets~: {Exploiting
        the {P}roperty-{B}ased {D}esign {P}rocess}},
  booktitle = {FDL'06: Proceeding of Forum on specification and Design Languages},
  year = {2006},
  keywords = {Property-based design}
}

@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},
  pages = {147-189},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@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)},
  year = {2012},
  volume = {14},
  pages = {1-14},
  file = {:/users/outil/verif/biblio/Cegar/A_framework_forCVofMVviaAR-ATVA09.pdf:PDF},
  keywords = {Predicate abstraction, Precise abstraction, Approximated abstraction,
        CEGAR},
  publisher = {Springer},
  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)},
  year = {1982},
  editor = {Bernhard Steffen},
  address = {Lisbon, Portugal},
  month = {March-April},
  publisher = {Springer-Verlag LNCS 1384}
}

@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},
  year = {2006},
  pages = {399--410},
  address = {Washington, DC, USA},
  publisher = {IEEE Computer Society},
  doi = {http://dx.doi.org/10.1109/LICS.2006.5},
  owner = {cecile},
  timestamp = {2007.01.14}
}

@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},
  pages = {1606-1621},
  number = {10},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1109/TCAD.2005.852031}
}

@INCOLLECTION{IMM2001-0855,
  author = {J. Spars{\o}},
  title = {Asynchronous {C}ircuit {D}esign - {A} {T}utorial},
  booktitle = {Chapters {1-}8 in {''}Principles of asynchronous circuit design -
        A systems Perspective''},
  publisher = {Kluwer Academic Publishers},
  year = {2001},
  pages = {1-152},
  address = {London},
  month = {dec},
  isbn_issn = {0-7923-7613-7},
  url = {http://www2.imm.dtu.dk/pubdb/p.php?855}
}

@MANUAL{AtelierB,
  title = {{A}telier {B}, {M}anuel {U}tilisateur},
  author = {{{STERIA} Technologie de l'information}},
  address = {Aix-en-Provence, France},
  year = {1998},
  keywords = {theorem prover, b},
  series = {version 3.5}
}

@PHDTHESIS{turk05thesis,
  author = {T\"urk, T.},
  title = {A Hierarchy for Accellera's Property Specification Language},
  school = {University of Kaiserslautern},
  year = {2005},
  comment = {Je l'ai en papier},
  keywords = {automata approach, PSL},
  owner = {cecile},
  timestamp = {2006.02.13},
  url = {http://thomas-tuerk.de/dokumente/Diplomarbeit.pdf}
}

@MANUAL{vismanual,
  title = {VIS User's Manual},
  author = {{The VIS Group}},
  year = {1996},
  file = {vis_user.ps:/dsk/l1/misc/doc/checker/vis_user.ps:PDF},
  key = VIS,
  keywords = {model checker},
  owner = {cecile},
  timestamp = {2006.02.09}
}

@MISC{m106archi,
  author = {{Universit\'e Pierre et Marie Curie (UPMC), Paris 6}},
  title = {{{UE} : Achitecture des syst\`emes int\'egr\'es, {M1}}},
  note = {\url{http://www-master.ufr-info-p6.jussieu.fr/ue/archi/}},
  owner = {cecile},
  timestamp = {2006.10.05}
}

@ARTICLE{fms,
  author = {D.M.~Upton},
  title = {A {F}lexible {S}tructure for {C}omputer-{C}ontrolled {M}anufacturing
        {S}ystems},
  journal = {Manufacturing Review},
  year = {1992},
  volume = {5},
  pages = {58--74},
  number = {1},
  keywords = {FMS},
  owner = {cecile},
  timestamp = {2007.01.22}
}

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

@INPROCEEDINGS{xie03verified,
  author = {F.~Xie and J.C.~Browne},
  title = {Verified {S}ystems by {C}omposition from {V}erified {C}omponents},
  booktitle = {E{SEC}/{FSE} 2003 : {P}roceedings of the 11th {ACM} {SIGSOFT} {S}ymposium
        on {F}oundations of {S}oftware {E}ngineering 2003 held jointly with
        9th {E}uropean {S}oftware {E}ngineering {C}onference},
  year = {2003},
  pages = {277--286},
  address = {Helsinki, Finland},
  publisher = {ACM Press},
  comment = {: Proceedings of the 9th European software engineering conference
        held jointly with 11th ACM SIGSOFT international symposium on Foundations
        of software engineering},
  doi = {http://doi.acm.org/10.1145/940071.940109},
  isbn = {1-58113-743-5},
  location = {Helsinki, Finland}
}

@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},
  file = {:/users/outil/verif/biblio/Cegar/AviYadgarPhDThesisReport.pdf:PDF},
  keywords = {Cegar, BMC, 3-valued, Abstraction},
  owner = {verif},
  timestamp = {2010.06.15}
}

@TECHREPORT{cegarhwcasestudy07,
  author = {Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah},
  title = {CEGAR-Based Formal Hardware Verification: A Case Study},
  institution = {Department of Electrical Engineering and Computer Science
        
        University of Michigan},
  year = {2007},
  file = {:Cegar/CEGARHWVerifCaseStudy07.pdf:PDF},
  keywords = {CEGAR,hardware},
  owner = {cecile},
  timestamp = {2010.06.10}
}

@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},
  year = {2008},
  volume = {39},
  pages = {1395--1404},
  number = {12},
  address = {Amsterdam, The Netherlands, The Netherlands},
  doi = {http://dx.doi.org/10.1016/j.mejo.2008.05.013},
  file = {:Analog/surveyZaki08.pdf:PDF},
  issn = {0026-2692},
  publisher = {Elsevier Science Publishers B. V.}
}

@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},
  year = {2002},
  editor = {Mark Aagaard and John W. O'Leary},
  volume = {2517},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {FMCAD},
  isbn = {3-540-00116-6}
}

@PROCEEDINGS{DBLP:conf/sefm/2005,
  title = {Third IEEE International Conference on Software Engineering and Formal
        Methods (SEFM 2005), 7-9 September 2005, Koblenz, Germany},
  year = {2005},
  editor = {Bernhard K. Aichernig and Bernhard Beckert},
  publisher = {IEEE Computer Society},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {SEFM},
  isbn = {0-7695-2435-4}
}

@PROCEEDINGS{DBLP:conf/cav/2004,
  title = {Computer Aided Verification, 16th International Conference, CAV 2004,
        Boston, MA, USA, July 13-17, 2004, Proceedings},
  year = {2004},
  editor = {Rajeev Alur and Doron Peled},
  volume = {3114},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CAV},
  isbn = {3-540-22342-8}
}

@PROCEEDINGS{DBLP:conf/cav/2006,
  title = {CAV'06: Proceedings of 18th International Conference of Computer
        Aided Verification},
  year = {2006},
  editor = {Thomas Ball and Robert B. Jones},
  volume = {4144},
  series = {Lecture Notes in Computer Science},
  address = {Seattle, WA, USA},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CAV},
  isbn = {3-540-37406-X}
}

@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},
  year = {2006},
  editor = {Marco Bernardo and Alessandro Cimatti},
  volume = {3965},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {SFM},
  isbn = {978-3-540-34304-2}
}

@PROCEEDINGS{DBLP:conf/cav/2001,
  title = {Computer Aided Verification, 13th International Conference, CAV 2001,
        Paris, France, July 18-22, 2001, Proceedings},
  year = {2001},
  editor = {G{\'e}rard Berry and Hubert Comon and Alain Finkel},
  volume = {2102},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CAV},
  isbn = {3-540-42345-1}
}

@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},
  year = {2007},
  editor = {Eyal Bin and Avi Ziv and Shmuel Ur},
  volume = {4383},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {Haifa Verification Conference},
  isbn = {978-3-540-70888-9}
}

@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},
  year = {2006},
  editor = {Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem
        P. de Roever},
  volume = {4111},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {FMCO},
  isbn = {3-540-36749-7}
}

@PROCEEDINGS{DBLP:conf/charme/2005,
  title = {Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5
        Advanced Research Working Conference, CHARME 2005, Saarbr{\"u}cken,
        Germany, October 3-6, 2005, Proceedings},
  year = {2005},
  editor = {Dominique Borrione and Wolfgang J. Paul},
  volume = {3725},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CHARME},
  isbn = {3-540-29105-9},
  owner = {cecile},
  timestamp = {2006.06.27}
}

@PROCEEDINGS{DBLP:conf/cav/2002,
  title = {Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen,
        Denmark, July 27-31, 2002, Proceedings},
  year = {2002},
  editor = {Ed Brinksma and Kim Guldstrand Larsen},
  volume = {2404},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CAV},
  isbn = {3-540-43997-8}
}

@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},
  year = {2005},
  editor = {Maura Cerioli},
  volume = {3442},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {FASE},
  isbn = {3-540-25420-X}
}

@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},
  year = {2008},
  editor = {Iliano Cervesato and Helmut Veith and Andrei Voronkov},
  volume = {5330},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {LPAR},
  isbn = {978-3-540-89438-4}
}

@PROCEEDINGS{DBLP:conf/vmcai/2005,
  title = {Verification, Model Checking, and Abstract Interpretation, 6th International
        Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings},
  year = {2005},
  editor = {Radhia Cousot},
  volume = {3385},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {VMCAI},
  isbn = {3-540-24297-X}
}

@PROCEEDINGS{DBLP:conf/tcs/1981,
  title = {Theoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany,
        March 23-25, 1981, Proceedings},
  year = {1981},
  editor = {Peter Deussen},
  volume = {104},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {Theoretical Computer Science},
  isbn = {3-540-10576-X}
}

@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},
  year = {2006},
  editor = {E. Allen Emerson and Kedar S. Namjoshi},
  volume = {3855},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {VMCAI},
  isbn = {3-540-31139-4}
}

@PROCEEDINGS{DBLP:conf/cav/2000,
  title = {Computer Aided Verification, 12th International Conference, CAV 2000,
        Chicago, IL, USA, July 15-19, 2000, Proceedings},
  year = {2000},
  editor = {E.A.~Emerson and A.P.~Sistla},
  volume = {1855},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CAV},
  isbn = {3-540-67770-4},
  owner = {cecile},
  timestamp = {2006.02.13}
}

@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},
  year = {2002},
  editor = {Javier Esparza and Charles Lakos},
  volume = {2360},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {ICATPN},
  isbn = {3-540-43787-8}
}

@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},
  year = {2006},
  editor = {Georges G. E. Gielen},
  publisher = {European Design and Automation Association, Leuven, Belgium},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {DATE},
  isbn = {3-9810801-0-6}
}

@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},
  year = {2004},
  editor = {Enrico Giunchiglia and Armando Tacchella},
  volume = {2919},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {SAT},
  isbn = {3-540-20851-8}
}

@PROCEEDINGS{DBLP:conf/frocos/2005,
  title = {Frontiers of Combining Systems, 5th International Workshop, FroCoS
        2005, Vienna, Austria, September 19-21, 2005, Proceedings},
  year = {2005},
  editor = {Bernhard Gramlich},
  volume = {3717},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {FroCoS},
  isbn = {3-540-29051-6}
}

@PROCEEDINGS{DBLP:conf/cav/1997,
  title = {Computer Aided Verification, 9th International Conference, CAV '97,
        Haifa, Israel, June 22-25, 1997, Proceedings},
  year = {1997},
  editor = {Orna Grumberg},
  volume = {1254},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CAV},
  isbn = {3-540-63166-6}
}

@PROCEEDINGS{DBLP:conf/cav/1999,
  title = {Computer Aided Verification, 11th International Conference, CAV '99,
        Trento, Italy, July 6-10, 1999, Proceedings},
  year = {1999},
  editor = {Nicolas Halbwachs and Doron Peled},
  volume = {1633},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CAV},
  isbn = {3-540-66202-2},
  owner = {cecile},
  timestamp = {2006.04.25}
}

@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},
  year = {2005},
  editor = {Nicolas Halbwachs and Lenore D. Zuck},
  volume = {3440},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {TACAS},
  isbn = {3-540-25333-5}
}

@PROCEEDINGS{DBLP:conf/iccad/2006,
  title = {2006 International Conference on Computer-Aided Design (ICCAD'06),
        November 5-9, 2006, San Jose, CA, USA},
  year = {2006},
  editor = {Soha Hassoun},
  publisher = {ACM},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {ICCAD},
  isbn = {1-59593-389-1}
}

@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},
  year = {2006},
  editor = {Holger Hermanns and Jens Palsberg},
  volume = {3920},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {TACAS},
  isbn = {3-540-33056-9}
}

@PROCEEDINGS{DBLP:conf/cav/1998,
  title = {Computer Aided Verification, 10th International Conference, CAV '98,
        Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings},
  year = {1998},
  editor = {Alan J. Hu and Moshe Y. Vardi},
  volume = {1427},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CAV},
  isbn = {3-540-64608-6}
}

@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},
  year = {2004},
  editor = {Kurt Jensen and Andreas Podelski},
  volume = {2988},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {TACAS},
  isbn = {3-540-21299-X}
}

@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},
  year = {2011},
  editor = {Ranjit Jhala and David A. Schmidt},
  volume = {6538},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {VMCAI},
  ee = {http://dx.doi.org/10.1007/978-3-642-18275-4},
  isbn = {978-3-642-18274-7}
}

@PROCEEDINGS{DBLP:conf/cav/2003,
  title = {Computer Aided Verification, 15th International Conference, CAV 2003,
        Boulder, CO, USA, July 8-12, 2003, Proceedings},
  year = {2003},
  editor = {Warren A. Hunt Jr. and Fabio Somenzi},
  volume = {2725},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CAV},
  isbn = {3-540-40524-0}
}

@PROCEEDINGS{DBLP:conf/dac/2005,
  title = {Proceedings of the 42nd Design Automation Conference, DAC 2005, San
        Diego, CA, USA, June 13-17, 2005},
  year = {2005},
  editor = {William H. Joyner Jr. and Grant Martin and Andrew B. Kahng},
  publisher = {ACM},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {DAC},
  isbn = {1-59593-058-2}
}

@PROCEEDINGS{DBLP:conf/lop/1981,
  title = {Logic of Programs, Workshop},
  year = {1982},
  editor = {Dexter Kozen},
  volume = {131},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {Logic of Programs},
  isbn = {3-540-11212-X}
}

@PROCEEDINGS{DBLP:conf/dac/2004,
  title = {Proceedings of the 41th Design Automation Conference, DAC 2004, San
        Diego, CA, USA, June 7-11, 2004},
  year = {2004},
  editor = {Sharad Malik and Limor Fix and Andrew B. Kahng},
  publisher = {ACM},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {DAC},
  isbn = {1-58113-828-8}
}

@PROCEEDINGS{DBLP:conf/birthday/2010pnueli,
  title = {Time for Verification, Essays in Memory of Amir Pnueli},
  year = {2010},
  editor = {Zohar Manna and Doron Peled},
  volume = {6200},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {Essays in Memory of Amir Pnueli},
  ee = {http://dx.doi.org/10.1007/978-3-642-13754-9},
  isbn = {978-3-642-13753-2}
}

@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},
  year = {2001},
  editor = {Tiziana Margaria and Wang Yi},
  volume = {2031},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {TACAS},
  isbn = {3-540-41865-2}
}

@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},
  year = {2009},
  editor = {Marcel Vinicius Medeiros Oliveira and Jim Woodcock},
  volume = {5902},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {SBMF},
  ee = {http://dx.doi.org/10.1007/978-3-642-10452-7},
  isbn = {978-3-642-10451-0}
}

@PROCEEDINGS{DBLP:conf/concur/2000,
  title = {CONCUR 2000 - Concurrency Theory, 11th International Conference,
        University Park, PA, USA, August 22-25, 2000, Proceedings},
  year = {2000},
  editor = {Catuscia Palamidessi},
  volume = {1877},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {CONCUR},
  isbn = {3-540-67897-2}
}

@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},
  year = {2008},
  editor = {C. R. Ramakrishnan and Jakob Rehof},
  volume = {4963},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {TACAS},
  isbn = {978-3-540-78799-0}
}

@PROCEEDINGS{DBLP:conf/compos/1997,
  title = {Compositionality: The Significant Difference, International Symposium,
        COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures},
  year = {1998},
  editor = {Willem P. de Roever and Hans Langmaack and Amir Pnueli},
  volume = {1536},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {COMPOS},
  isbn = {3-540-65493-3}
}

@PROCEEDINGS{DBLP:conf/dac/2006,
  title = {Proceedings of the 43rd Design Automation Conference, DAC 2006, San
        Francisco, CA, USA, July 24-28, 2006},
  year = {2006},
  editor = {Ellen Sentovich},
  publisher = {ACM},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {DAC},
  isbn = {1-59593-381-6}
}

@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},
  year = {1998},
  editor = {Bernhard Steffen},
  volume = {1384},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {TACAS},
  isbn = {3-540-64356-7}
}

@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},
  year = {2005},
  editor = {Farn Wang},
  volume = {3731},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {FORTE},
  isbn = {3-540-29189-X}
}

@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},
  year = {1999},
  editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
  volume = {1708},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {World Congress on Formal Methods},
  isbn = {3-540-66587-0}
}

@MISC{alliance,
  title = {Alliance, a free {VLSI} cad system},
  note = {\\\url{http://www-asim.lip6.fr/recherche/alliance/}},
  owner = {cecile},
  timestamp = {2007.02.01}
}

@MISC{onespin,
  title = {OneSpin Solutions},
  note = {\url{http://www.onespin-solutions.com/}},
  key = OneS,
  owner = {cecile},
  timestamp = {2007.03.07}
}

@MISC{prosyd,
  title = {The Prosyd Project on Property-Based System Design},
  note = {{\url{http://www.prosyd.org/}}},
  owner = {cecile},
  timestamp = {2007.02.07}
}

@MISC{soclib,
  title = {The {S}o{CL}ib {P}roject},
  note = {\url{http://soclib.lip6.fr/}},
  key = SoC,
  owner = {cecile},
  timestamp = {2006.09.07},
  url = {http://soclib.lip6.fr/}
}

@MISC{texas97bench,
  title = {Texas-97 {V}erification {B}enchmarks},
  note = {\\\url{http://www.cad.eecs.berkeley.edu/Respep/Research/vis/texas-97/}},
  key = TEXAS,
  keywords = {protocol, PIbus},
  owner = {cecile},
  timestamp = {2006.11.30}
}

@MISC{vsia,
  title = {{VSI A}lliance},
  note = {\url{http://www.vsi.org/}},
  key = VSI,
  owner = {cecile},
  timestamp = {2006.09.13}
}

@PROCEEDINGS{DBLP:conf/date/2009,
  title = {Design, Automation and Test in Europe, DATE 2009, Nice, France, April
        20-24, 2009},
  year = {2009},
  publisher = {IEEE},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {DATE}
}

@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},
  year = {2009},
  publisher = {IEEE},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {FMCAD},
  isbn = {978-1-4244-4966-8}
}

@PROCEEDINGS{DBLP:conf/lics/2004,
  title = {19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17
        July 2004, Turku, Finland, Proceedings},
  year = {2004},
  publisher = {IEEE Computer Society},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {LICS},
  isbn = {0-7695-2192-4}
}

@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},
  year = {2004},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {SAT},
  owner = {cecile},
  timestamp = {2009.01.27}
}

@PROCEEDINGS{DBLP:conf/date/2003,
  title = {2003 Design, Automation and Test in Europe Conference and Exposition
        (DATE 2003), 3-7 March 2003, Munich, Germany},
  year = {2003},
  publisher = {IEEE Computer Society},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {DATE},
  isbn = {0-7695-1870-2}
}

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

@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},
  year = {2003},
  publisher = {IEEE Computer Society},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {TIME},
  isbn = {0-7695-1912-1}
}

@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},
  year = {2002},
  publisher = {IEEE Computer Society},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {ICCD},
  isbn = {0-7695-1700-5},
  keywords = {3-valued, logic, model checking, Kripke structure}
}

@PROCEEDINGS{DBLP:conf/dac/2001,
  title = {Proceedings of the 38th Design Automation Conference, DAC 2001, Las
        Vegas, NV, USA, June 18-22, 2001},
  year = {2001},
  publisher = {ACM},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {DAC},
  isbn = {1-58113-297-2}
}

@PROCEEDINGS{DBLP:conf/icse/2001,
  title = {Proceedings of the 23rd International Conference on Software Engineering,
        ICSE 2001, 12-19 May 2001, Toronto, Ontario, Canada},
  year = {2001},
  publisher = {IEEE Computer Society},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {ICSE},
  isbn = {0-7695-1050-7}
}

@MANUAL{amba,
  title = {AMBA Specification},
  organization = {ARM limited},
  edition = {2.0},
  year = {1999},
  note = {ARM Limited \copyright. All right reserved},
  file = {IHI0011A_AMBA_SPEC.pdf:/dsk/l1/misc/doc/amba/IHI0011A_AMBA_SPEC.pdf:PDF},
  key = AMBA,
  owner = {cecile},
  timestamp = {2006.09.07}
}

@MANUAL{formalcheck,
  title = {Formal Verification Using Affirma {FormalCheck}},
  organization = {Cadence},
  month = {October},
  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},
  year = {1989},
  publisher = {IEEE Computer Society},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {LICS}
}

@PROCEEDINGS{DBLP:conf/lics/LICS3,
  title = {Proceedings, Third Annual Symposium on Logic in Computer Science},
  year = {1988},
  address = {Edinburgh, Scotland, UK},
  publisher = {IEEE Computer Society},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {LICS}
}

@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},
  year = {1982},
  publisher = {ACM},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  booktitle = {STOC}
}