source: biblio/biblio.bib @ 62

Last change on this file since 62 was 51, checked in by cecile, 13 years ago

new articles for components based abstraction and compostion added
File size: 144.3 KB
Line 
1% This file was created with JabRef 2.5.
2% Encoding: UTF8
3
4@STRING{LICS04 = {LICS'04: Proceedings of the 19th IEEE Symposium on Logic in Computer
5        Science}}
6
7@STRING{LNCS = {}}
8
9@INPROCEEDINGS{aagaard03hazards,
10  author = {M.~Aagaard},
11  title = {A {H}azards-{B}ased {C}orrectness {S}tatement for {P}ipelined {C}ircuits.},
12  booktitle = {Proceedings of the 12th IFIP WG 10.5 Advanced Research Working Conference},
13  year = {2003},
14  pages = {66-80},
15  publisher = {Springer},
16  bibsource = {DBLP, http://dblp.uni-trier.de},
17  crossref = {DBLP:conf/charme/2003},
18  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2860{\&}spage=66},
19  file = {aagard.pdf:/dsk/l1/misc/doc/verif_archi/aagard.pdf:PDF},
20  keywords = {pipeline}
21}
22
23@INPROCEEDINGS{alder06ticc,
24  author = {B.T.~Adler and L.~de Alfaro and L.~Dias da Silva and M.~Faella and
25        A.~Legay and V.~Raman and P.~Roy},
26  title = {Ticc: {A T}ool for {I}nterface {C}ompatibility and {C}omposition.},
27  booktitle = {CAV'06: Proceedings of 18th International Conference of Computer
28        Aided Verification},
29  year = {2006},
30  pages = {59-62},
31  bibsource = {DBLP, http://dblp.uni-trier.de},
32  crossref = {DBLP:conf/cav/2006},
33  ee = {http://dx.doi.org/10.1007/11817963_8},
34  file = {tiicctool.pdf:/dsk/l1/misc/doc/interface/tiicctool.pdf:PDF},
35  keywords = {interface, wrapper}
36}
37
38@INPROCEEDINGS{DBLP:conf/frocos/AlfaroSFLRS05,
39  author = {Luca de Alfaro and Leandro Dias da Silva and Marco Faella and Axel
40        Legay and Pritam Roy and Maria Sorea},
41  title = {{Sociable Interfaces.}},
42  booktitle = {FroCos'05: Proceedings of the 5th International Workshop on Frontiers
43        of Combining Systems},
44  year = {2005},
45  pages = {81-105},
46  address = {Vienna, Austria},
47  bibsource = {DBLP, http://dblp.uni-trier.de},
48  crossref = {DBLP:conf/frocos/2005},
49  ee = {http://dx.doi.org/10.1007/11559306_5}
50}
51
52@INPROCEEDINGS{alur98alternatingtime,
53  author = {Rajeev Alur and Thomas A. Henzinger and Orna Kupferman},
54  title = {{Alternating-Time Temporal Logic}},
55  booktitle = {COMPOS},
56  year = {1997},
57  pages = {23-60},
58  bibsource = {DBLP, http://dblp.uni-trier.de},
59  crossref = {DBLP:conf/compos/1997},
60  ee = {http://link.springer.de/link/service/series/0558/bibs/1536/15360023.htm},
61  keywords = {atl}
62}
63
64@INPROCEEDINGS{DBLP:conf/lpar/AndrausLS08,
65  author = {Zaher S. Andraus and Mark H. Liffiton and Karem A. Sakallah},
66  title = {Reveal: A Formal Verification Tool for Verilog Designs},
67  booktitle = {LPAR},
68  year = {2008},
69  pages = {343-352},
70  bibsource = {DBLP, http://dblp.uni-trier.de},
71  crossref = {DBLP:conf/lpar/2008},
72  ee = {http://dx.doi.org/10.1007/978-3-540-89439-1_25},
73  keywords = {CEGAR,Hardware, TOOLS}
74}
75
76@INPROCEEDINGS{DBLP:conf/dac/AndrausS04,
77  author = {Zaher S. Andraus and Karem A. Sakallah},
78  title = {Automatic abstraction and verification of verilog models},
79  booktitle = {DAC},
80  year = {2004},
81  pages = {218-223},
82  bibsource = {DBLP, http://dblp.uni-trier.de},
83  crossref = {DBLP:conf/dac/2004},
84  ee = {http://doi.acm.org/10.1145/996566.996629},
85  file = {:Abstraction/Andraus_DAC_Vapor.pdf:PDF},
86  keywords = {Abstraction, Hardware, Verilog, TOOLS, Vapor}
87}
88
89@INPROCEEDINGS{Awhed04Proving,
90  author = {M.~Awedh and F.~Somenzi},
91  title = {Proving More Properties with Bounded Model Checking},
92  booktitle = {CAV'04: Proceedings of the 16th International Conference on Computer
93        Aided Verification},
94  year = {2004},
95  pages = {96-108},
96  bibsource = {DBLP, http://dblp.uni-trier.de},
97  crossref = {DBLP:conf/cav/2004},
98  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3114{\&}spage=96},
99  file = {:BMC/ProvingMorePropwithBC04.pdf:PDF},
100  keywords = {BMC, VIS}
101}
102
103@INPROCEEDINGS{bmethod99meteor,
104  author = {P.~Behm and P.~Benoit and A.~Faivre and J-M.~Meynadier},
105  title = {{M{\'e}t{\'e}or: A Successful Application of B in a Large Project}},
106  booktitle = {World Congress on Formal Methods},
107  year = {1999},
108  pages = {369-387},
109  bibsource = {DBLP, http://dblp.uni-trier.de},
110  crossref = {DBLP:conf/fm/1999-1},
111  ee = {http://link.springer.de/link/service/series/0558/bibs/1708/17080369.htm}
112}
113
114@INPROCEEDINGS{DBLP:conf/vmcai/Bradley11,
115  author = {Aaron R. Bradley},
116  title = {SAT-Based Model Checking without Unrolling},
117  booktitle = {VMCAI},
118  year = {2011},
119  pages = {70-87},
120  bibsource = {DBLP, http://dblp.uni-trier.de},
121  crossref = {DBLP:conf/vmcai/2011},
122  ee = {http://dx.doi.org/10.1007/978-3-642-18275-4_7}
123}
124
125@INPROCEEDINGS{bruns00generalized,
126  author = {G.~Bruns and P.~Godefroid},
127  title = {{Generalized Model Checking: Reasoning about Partial State Spaces}},
128  booktitle = {CONCUR'2000: Proceedings of the 11th International Conference on
129        Concurrency Theory},
130  year = {2000},
131  editor = {Nicolas Halbwachs and Doron Peled},
132  series = {Lecture Notes in Computer Science},
133  pages = {168-182},
134  bibsource = {DBLP, http://dblp.uni-trier.de},
135  crossref = {DBLP:conf/concur/2000},
136  ee = {http://link.springer.de/link/service/series/0558/bibs/1877/18770168.htm},
137  file = {godefroid00.pdf:/dsk/l1/misc/doc/abstraction/godefroid00.pdf:PDF},
138  keywords = {3-valued, Kripke structure, abstraction}
139}
140
141@INPROCEEDINGS{burns99partial,
142  author = {G.~Bruns and P.~Godefroid},
143  title = {{Model Checking Partial State Spaces with 3-Valued Temporal Logics}},
144  booktitle = {CAV'99: Proceedings of the 11th conference on Computer Aided Verification},
145  year = {1999},
146  series = {Lecture Notes in Computer Science},
147  pages = {274-287},
148  bibsource = {DBLP, http://dblp.uni-trier.de},
149  crossref = {DBLP:conf/cav/1999},
150  ee = {http://link.springer.de/link/service/series/0558/bibs/1633/16330274.htm},
151  file = {burns99partial.pdf:/dsk/l1/misc/doc/abstraction/burns99partial.pdf:PDF},
152  keywords = {tree automata, CTL, automata approach},
153  owner = {cecile},
154  timestamp = {2006.04.25}
155}
156
157@INPROCEEDINGS{Buttner05isformal,
158  author = {W. B{\"u}ttner},
159  title = {{Is Formal Verification Bound to Remain a Junior Partner of Simulation?}},
160  booktitle = {CHARME'2005: Proceedings of the Correct Hardware Design and Verification
161        Methods, 13th IFIP WG 10.5 Advanced Research Working Conference},
162  year = {2005},
163  editor = {Dominique Borrione, Wolfgang J. Paul},
164  volume = {3725},
165  series = {Lecture Notes in Computer Science},
166  pages = {1},
167  publisher = {Springer},
168  bibsource = {DBLP, http://dblp.uni-trier.de},
169  crossref = {DBLP:conf/charme/2005},
170  ee = {http://dx.doi.org/10.1007/11560548_1},
171  owner = {cecile},
172  timestamp = {2006.06.27}
173}
174
175@INPROCEEDINGS{DBLP:conf/fmcad/ChauhanCKSVW02,
176  author = {P.~Chauhan and E.M.~Clarke and J.H.~Kukula and S.~Sapra and H.~Veith
177        and D.~Wang},
178  title = {Automated Abstraction Refinement for Model Checking Large State Spaces
179        Using SAT Based Conflict Analysis},
180  booktitle = {FMCAD'02: Proceedings of the 4th International Conference on Formal
181        Methods in Computer-Aided Design },
182  year = {2002},
183  pages = {33-51},
184  bibsource = {DBLP, http://dblp.uni-trier.de},
185  crossref = {DBLP:conf/fmcad/2002},
186  ee = {http://link.springer.de/link/service/series/0558/bibs/2517/25170033.htm},
187  file = {:Cegar/AutomatedAbstractionRefinment02Chauchan.pdf:PDF},
188  keywords = {Cegar, SAT}
189}
190
191@INPROCEEDINGS{chechik05framework,
192  author = {Marsha Chechik and Arie Gurfinkel},
193  title = {A Framework for Counterexample Generation and Exploration.},
194  booktitle = {FASE},
195  year = {2005},
196  pages = {220-236},
197  bibsource = {DBLP, http://dblp.uni-trier.de},
198  crossref = {DBLP:conf/fase/2005},
199  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3442{\&}spage=220},
200  file = {chechik05a.pdf:/dsk/l1/misc/doc/abstraction/chechik05a.pdf:PDF}
201}
202
203@INPROCEEDINGS{ChocklerKV01,
204  author = {H.~Chockler and O.~Kupferman and M.Y.~Vardi},
205  title = {Coverage Metrics for Temporal Logic Model Checking},
206  booktitle = {TACAS'01: 7th International Conference on Tools and Algorithms for
207        the Construction and Analysis of Systems},
208  year = {2001},
209  series = {LNCS},
210  pages = {528-542},
211  bibsource = {DBLP, http://dblp.uni-trier.de},
212  crossref = {DBLP:conf/tacas/2001},
213  ee = {http://link.springer.de/link/service/series/0558/bibs/2031/20310528.htm},
214  file = {:Fault/Coverage_Metric_for_temporal_MC01.pdf:PDF},
215  keywords = {coverage}
216}
217
218@INPROCEEDINGS{DBLP:conf/fmcad/CimattiDJR09,
219  author = {Alessandro Cimatti and Jori Dubrovin and Tommi A. Junttila and Marco
220        Roveri},
221  title = {Structure-aware computation of predicate abstraction},
222  booktitle = {FMCAD},
223  year = {2009},
224  pages = {9-16},
225  bibsource = {DBLP, http://dblp.uni-trier.de},
226  crossref = {DBLP:conf/fmcad/2009},
227  ee = {http://dx.doi.org/10.1109/FMCAD.2009.5351149},
228  file = {:Cegar/StructureAwareComputationofPredicateAbstraction09.pdf:PDF},
229  keywords = {Abstraction}
230}
231
232@INPROCEEDINGS{DBLP:conf/sfm/ClaessenR06,
233  author = {Koen Claessen and Jan-Willem Roorda},
234  title = {An Introduction to Symbolic Trajectory Evaluation},
235  booktitle = {SFM},
236  year = {2006},
237  pages = {56-77},
238  bibsource = {DBLP, http://dblp.uni-trier.de},
239  crossref = {DBLP:conf/sfm/2006},
240  ee = {http://dx.doi.org/10.1007/11757283_3}
241}
242
243@INPROCEEDINGS{clarke03cegar,
244  author = {E.M.~Clarke},
245  title = {Counterexample-Guided Abstraction Refinement},
246  booktitle = {TIME},
247  year = {2003},
248  pages = {7},
249  bibsource = {DBLP, http://dblp.uni-trier.de},
250  crossref = {DBLP:conf/time/2003},
251  ee = {http://csdl.computer.org/comp/proceedings/time-ictl/2003/1912/00/19120007.pdf},
252  file = {ce03time.pdf:/dsk/l1/misc/doc/CEGAR/ce03time.pdf:PDF},
253  keywords = {abstraction, CEGAR}
254}
255
256@INPROCEEDINGS{clarkeE81design,
257  author = {E.M.~Clarke and E.A.~Emerson},
258  title = {Design and Synthesis of Synchronization Skeletons Using Branching-Time
259        Temporal Logic.},
260  booktitle = {Logic of Programs},
261  year = {1981},
262  pages = {52-71},
263  bibsource = {DBLP, http://dblp.uni-trier.de},
264  crossref = {DBLP:conf/lop/1981}
265}
266
267@INPROCEEDINGS{ClarkeGJLV00,
268  author = {E.M.~Clarke and O.Grumberg and S.~Jha and Y.~Lu and H.~Veith},
269  title = {{Counterexample-Guided Abstraction Refinement.}},
270  booktitle = {CAV'00: Proceedings of the 12th International Conference on Computer
271        Aided Verification},
272  year = {2000},
273  pages = {154-169},
274  bibsource = {DBLP, http://dblp.uni-trier.de},
275  crossref = {DBLP:conf/cav/2000}
276}
277
278@INPROCEEDINGS{DBLP:conf/birthday/ClarkeKV10,
279  author = {Edmund M. Clarke and Robert P. Kurshan and Helmut Veith},
280  title = {The Localization Reduction and Counterexample-Guided Abstraction
281        Refinement},
282  booktitle = {Essays in Memory of Amir Pnueli},
283  year = {2010},
284  pages = {61-71},
285  bibsource = {DBLP, http://dblp.uni-trier.de},
286  crossref = {DBLP:conf/birthday/2010pnueli},
287  ee = {http://dx.doi.org/10.1007/978-3-642-13754-9_4}
288}
289
290@INPROCEEDINGS{DBLP:conf/lics/ClarkeLM89,
291  author = {E.~M.~Clarke and D.~E.~Long and K.~L.~McMillan},
292  title = {Compositional Model Checking},
293  booktitle = {LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer
294        Science},
295  year = {1989},
296  pages = {353-362},
297  bibsource = {DBLP, http://dblp.uni-trier.de},
298  crossref = {DBLP:conf/lics/LICS4},
299  file = {clarke89compo.ps:/dsk/l1/misc/doc/model_check/clarke89compo.ps:PDF},
300  keywords = {composition, model checking, Kripke structure, Moore machine, CTL}
301}
302
303@INPROCEEDINGS{DBLP:conf/sat/ClarkeTVW03,
304  author = {Edmund M. Clarke and Muralidhar Talupur and Helmut Veith and Dong
305        Wang},
306  title = {SAT Based Predicate Abstraction for Hardware Verification},
307  booktitle = {SAT},
308  year = {2003},
309  pages = {78-92},
310  bibsource = {DBLP, http://dblp.uni-trier.de},
311  crossref = {DBLP:conf/sat/2003},
312  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2919{\&}spage=78},
313  file = {:Abstraction/SATBasedPredicateAbstactforHWVerif2004.pdf:PDF},
314  keywords = {SAT, predicate abstraction, hardware}
315}
316
317@INPROCEEDINGS{CouvreurEPPW02,
318  author = {J-M.~Couvreur and E.~Encrenaz and E.~Paviot-Adet and D.~Poitrenaud
319        and P-A.~Wacrenier},
320  title = {Data Decision Diagrams for Petri Net Analysis.},
321  booktitle = {ICATPN'02: Proceedings of the 23rd International Conference on Applications
322        and Theory of Petri Nets},
323  year = {2002},
324  pages = {101-120},
325  bibsource = {DBLP, http://dblp.uni-trier.de},
326  crossref = {DBLP:conf/apn/2002},
327  ee = {http://link.springer.de/link/service/series/0558/bibs/2360/23600101.htm}
328}
329
330@INPROCEEDINGS{couvreur05hierarchie,
331  author = {J-M.~Couvreur and Y.~Thierry-Mieg},
332  title = {{Hierarchical Decision Diagrams to Exploit Model Structure.}},
333  booktitle = {FORTE : Proceedings of the 25th IFIP WG 6.1 International Conference
334        on Formal Techniques for Networked and Distributed Systems},
335  year = {2005},
336  editor = {Farn Wang},
337  volume = {3731},
338  series = {Lecture Notes in Computer Science},
339  pages = {443-457},
340  address = {Taipei, Taiwan},
341  publisher = {Springer},
342  bibsource = {DBLP, http://dblp.uni-trier.de},
343  crossref = {DBLP:conf/forte/2005},
344  ee = {http://dx.doi.org/10.1007/11562436_32}
345}
346
347@INPROCEEDINGS{DBLP:conf/vmcai/DamsN05,
348  author = {D.~Dams and K.~S.~Namjoshi},
349  title = {{Automata as Abstractions.}},
350  booktitle = {VMCAI'05: Proceedings of the 6th International Conference on Verification,
351        Model Checking, and Abstract Interpretation},
352  year = {2005},
353  series = {Lecture Notes in Computer science},
354  pages = {216-232},
355  address = {Paris, France},
356  bibsource = {DBLP, http://dblp.uni-trier.de},
357  crossref = {DBLP:conf/vmcai/2005},
358  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3385{\&}spage=216},
359  file = {automata_aabstr.pdf:/dsk/l1/misc/doc/modular/abstraction/automata_aabstr.pdf:PDF},
360  keywords = {tree automata, CTL, automata approach}
361}
362
363@INPROCEEDINGS{DBLP:conf/lics/DamsN04,
364  author = {D.~Dams and K.~S.~Namjoshi},
365  title = {The Existence of Finite Abstractions for Branching Time Model Checking.},
366  booktitle = {LICS04},
367  year = {2004},
368  pages = {335-344},
369  bibsource = {DBLP, http://dblp.uni-trier.de},
370  crossref = {DBLP:conf/lics/2004},
371  ee = {http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920335abs.htm},
372  file = {abstractforbtl.pdf:/dsk/l1/misc/doc/ctl_auto/abstractforbtl.pdf:PDF},
373  keywords = {CTL, tree automata ,model checking, automata approach}
374}
375
376@INPROCEEDINGS{DBLP:conf/icse/DwyerHJLPRZV01,
377  author = {Matthew B. Dwyer and John Hatcliff and Roby Joehanes and Shawn Laubach
378        and Corina S. Pasareanu and Robby and Hongjun Zheng and Willem Visser},
379  title = {Tool-Supported Program Abstraction for Finite-State Verification.},
380  booktitle = {ICSE},
381  year = {2001},
382  pages = {177-187},
383  bibsource = {DBLP, http://dblp.uni-trier.de},
384  crossref = {DBLP:conf/icse/2001},
385  file = {bandera.pdf:/dsk/l1/misc/doc/softMC/bandera.pdf:PDF},
386  keywords = {software, model-checking, CEGAR}
387}
388
389@INPROCEEDINGS{DBLP:conf/icse/EasterbrookCDGLPTT03,
390  author = {S.M.~Easterbrook and M.~Chechik and B.~Devereux and A.~Gurfinkel
391        and A.~Lai and V.~Petrovykh and A.~Tafliovich and C.~Thompson-Walsh},
392  title = {{$\chi$Chek: A Model Checker for Multi-Valued Reasoning.}},
393  booktitle = {ICSE'03: Proceedings of the 25th International Conference on Software
394        Engineering},
395  year = {2003},
396  pages = {804-805},
397  bibsource = {DBLP, http://dblp.uni-trier.de},
398  crossref = {DBLP:conf/icse/2003},
399  ee = {http://computer.org/proceedings/icse/1877/18770804.pdf}
400}
401
402@INPROCEEDINGS{EasterbrookC01,
403  author = {Steve M. Easterbrook and Marsha Chechik},
404  title = {A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints.},
405  booktitle = {ICSE},
406  year = {2001},
407  pages = {411-420},
408  bibsource = {DBLP,http://dblp.uni-trier.de},
409  crossref = {DBLP:conf/icse/2001},
410  file = {easterbrook01a.pdf:/dsk/l1/misc/doc/multi_valued/easterbrook01a.pdf:PDF},
411  keywords = {abstraction, 3-valued, 4-valued, logic, model checking}
412}
413
414@INPROCEEDINGS{emerson82desision,
415  author = {E.A.~Emerson and J.Y.~Halpern},
416  title = {Decision Procedures and Expressiveness in the Temporal Logic of Branching
417        Time},
418  booktitle = {STOC},
419  year = {1982},
420  pages = {169-180},
421  bibsource = {DBLP, http://dblp.uni-trier.de},
422  crossref = {DBLP:conf/stoc/STOC14},
423  file = {ctl_emerson82.pdf:/dsk/l1/misc/doc/model_check/ctl_emerson82.pdf:PDF},
424  keywords = {CTL, model checking}
425}
426
427@INPROCEEDINGS{DBLP:conf/date/GanaiGA05,
428  author = {Malay K. Ganai and Aarti Gupta and Pranav Ashar},
429  title = {Verification of Embedded Memory Systems using Efficient Memory Modeling},
430  booktitle = {DATE},
431  year = {2005},
432  pages = {1096-1101},
433  bibsource = {DBLP, http://dblp.uni-trier.de},
434  crossref = {DBLP:conf/date/2005},
435  ee = {http://doi.ieeecomputersociety.org/10.1109/DATE.2005.325},
436  file = {:Abstraction/VerifEmbededMemoryusingEMM09.pdf:PDF},
437  keywords = {Abstraction, Memory,},
438  owner = {cecile},
439  timestamp = {2010.06.10}
440}
441
442@INPROCEEDINGS{DBLP:conf/cav/GodefroidJ02,
443  author = {P.~Godefroid and R.~Jagadeesan},
444  title = {Automatic Abstraction Using Generalized Model Checking.},
445  booktitle = {CAV},
446  year = {2002},
447  pages = {137-150},
448  bibsource = {DBLP, http://dblp.uni-trier.de},
449  crossref = {DBLP:conf/cav/2002},
450  ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040137.htm},
451  keywords = {Abstraction}
452}
453
454@INPROCEEDINGS{GrafS97pvs,
455  author = {S.~Graf and H.~Sa\"{\i}di},
456  title = {{Construction of Abstract State Graphs with PVS.}},
457  booktitle = {CAV},
458  year = {1997},
459  pages = {72-83},
460  bibsource = {DBLP, http://dblp.uni-trier.de},
461  crossref = {DBLP:conf/cav/1997},
462  file = {graf97cinstructionpvs.ps:/dsk/l1/misc/doc/abstraction/graf97cinstructionpvs.ps:PDF},
463  keywords = {abstraction, CEGAR}
464}
465
466@INPROCEEDINGS{grumberg05abstraction,
467  author = {Orna Grumberg},
468  title = {{Abstraction and Refinement in Model Checking.}},
469  booktitle = {FMCO'05: 4th International Symposium on Formal Methods for Components
470        and Objects,},
471  year = {2005},
472  pages = {219-242},
473  bibsource = {DBLP, http://dblp.uni-trier.de},
474  crossref = {DBLP:conf/fmco/2005},
475  ee = {http://dx.doi.org/10.1007/11804192_11},
476  keywords = {abstraction, refinement, CEGAR}
477}
478
479@INPROCEEDINGS{DBLP:conf/sfm/GuptaGW06,
480  author = {Aarti Gupta and Malay K. Ganai and Chao Wang},
481  title = {SAT-Based Verification Methods and Applications in Hardware Verification},
482  booktitle = {SFM},
483  year = {2006},
484  pages = {108-143},
485  bibsource = {DBLP, http://dblp.uni-trier.de},
486  crossref = {DBLP:conf/sfm/2006},
487  ee = {http://dx.doi.org/10.1007/11757283_5},
488  file = {:BMC/SATBasedVerifMethodAndApplitoHdw2006.pdf:PDF},
489  keywords = {SAT, verification,}
490}
491
492@INPROCEEDINGS{gurfinkelC06waste,
493  author = {A.~Gurfinkel and M.~Chechik},
494  title = {{Why Waste a Perfectly Good Abstraction?.}},
495  booktitle = {T{ACAS}'06: {P}roceedings of the 12th international conference on
496        {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis of
497        {S}ystems},
498  year = {2006},
499  series = {Lecture Notes in Computer Science},
500  pages = {212-226},
501  address = {Vienna, Austria},
502  bibsource = {DBLP, http://dblp.uni-trier.de},
503  crossref = {DBLP:conf/tacas/2006},
504  ee = {http://dx.doi.org/10.1007/11691372_14},
505  file = {gurfinkel_tacas_06.pdf:/dsk/l1/misc/doc/abstraction/gurfinkel_tacas_06.pdf:PDF},
506  keywords = {abstraction, 3-valued, 4-valued, logic, model checking}
507}
508
509@INPROCEEDINGS{DBLP:conf/vmcai/GurfinkelWC06,
510  author = {Arie Gurfinkel and Ou Wei and Marsha Chechik},
511  title = {Systematic Construction of Abstractions for Model-Checking},
512  booktitle = {VMCAI},
513  year = {2006},
514  pages = {381-397},
515  bibsource = {DBLP, http://dblp.uni-trier.de},
516  crossref = {DBLP:conf/vmcai/2006},
517  ee = {http://dx.doi.org/10.1007/11609773_25}
518}
519
520@INPROCEEDINGS{GurfinkelWC06,
521  author = {Gurfinkel, A. and Wei, O. and Chechik, M.},
522  title = {Systematic {C}onstruction of {A}bstractions for {M}odel-{C}hecking.},
523  booktitle = {V{MCAI}'06: {P}roceedings of the 7th {I}nternational {C}onference
524        on {V}erification, {M}odel {C}hecking, and {A}bstract {I}nterpretation},
525  year = {2006},
526  pages = {381-397},
527  address = {Charleston, USA},
528  bibsource = {DBLP, http://dblp.uni-trier.de},
529  crossref = {DBLP:conf/vmcai/2006},
530  ee = {http://dx.doi.org/10.1007/11609773_25},
531  keywords = {abstraction, abstract interpretation}
532}
533
534@INPROCEEDINGS{JainKSC05,
535  author = {Jain, H. and Kroening, D. and Sharygina, N. and Clarke, E.M.},
536  title = {Word {L}evel {P}redicate {A}bstraction and {R}efinement for {V}erifying
537        {RTL} {V}erilog.},
538  booktitle = {D{AC}'05: {P}roceedings of the 42nd {D}esign {A}utomation {C}onference},
539  year = {2005},
540  editor = {William H. Joyner Jr., Grant Martin, Andrew B. Kahng},
541  series = {ACM},
542  pages = {445-450},
543  address = {San Diego, USA},
544  bibsource = {DBLP, http://dblp.uni-trier.de},
545  crossref = {DBLP:conf/dac/2005},
546  ee = {http://doi.acm.org/10.1145/1065579.1065697}
547}
548
549@INPROCEEDINGS{jhala01microarchi,
550  author = {Jhala, R. and McMillan, K.L.},
551  title = {Microarchitecture {V}erification by {C}ompositional {M}odel {C}hecking.},
552  booktitle = {C{AV}'01: {P}roceedings of the 13th {I}nternational {C}onference
553        on {C}omputer {A}ided {V}erification},
554  year = {2001},
555  editor = {G\'erard Berry, Hubert Comon, Alain Finkel},
556  series = {Lecture Notes in Computer Science},
557  pages = {396-410},
558  address = {Paris, France},
559  bibsource = {DBLP, http://dblp.uni-trier.de},
560  crossref = {DBLP:conf/cav/2001},
561  ee = {http://link.springer.de/link/service/series/0558/bibs/2102/21020396.htm}
562}
563
564@INPROCEEDINGS{Somenzi04Circuscav,
565  author = {HoonSang Jin and Mohammad Awedh and Fabio Somenzi},
566  title = {CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking},
567  booktitle = {CAV'04: Proceedings of the 16th International Conference onComputer
568        Aided Verification },
569  year = {2004},
570  pages = {519-522},
571  bibsource = {DBLP, http://dblp.uni-trier.de},
572  crossref = {DBLP:conf/cav/2004},
573  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3114{\&}spage=519},
574  file = {:SAT/CirCUsToward.pdf:PDF},
575  keywords = {SAT, SAT solver, VIS}
576}
577
578@INPROCEEDINGS{DBLP:conf/tacas/JinHS05,
579  author = {HoonSang Jin and HyoJung Han and Fabio Somenzi},
580  title = {Efficient Conflict Analysis for Finding All Satisfying Assignments
581        of a Boolean Circuit},
582  booktitle = {TACAS'05: Proceedings of 11th International Conference on Tools and
583        Algorithms for the Construction and Analysis of Systems},
584  year = {2005},
585  pages = {287-300},
586  bibsource = {DBLP, http://dblp.uni-trier.de},
587  crossref = {DBLP:conf/tacas/2005},
588  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3440{\&}spage=287},
589  file = {:SAT/efficientConflict05Jin.pdf:PDF},
590  keywords = {SAT, All-sat}
591}
592
593@INPROCEEDINGS{somenzi04Circus,
594  author = {H*.~Jin and F.~Somenzi},
595  title = {CirCUs: A Hybrid Satisfiability Solver},
596  booktitle = {SAT'04: The 7th International Conference on Theory and Applications
597        of Satisfiability Testing},
598  year = {2004},
599  bibsource = {DBLP, http://dblp.uni-trier.de},
600  crossref = {DBLP:conf/sat/2004},
601  ee = {http://www.satisfiability.org/SAT04/programme/24.pdf},
602  owner = {cecile},
603  timestamp = {2009.01.27}
604}
605
606@INPROCEEDINGS{larsen88modal,
607  author = {K.~G.~Larsen and B.~Thomsen},
608  title = {A {M}odal {P}rocess {L}ogic},
609  booktitle = {Third Annual Symposium on Logic in Computer Science},
610  year = {1988},
611  pages = {203-210},
612  bibsource = {DBLP, http://dblp.uni-trier.de},
613  crossref = {DBLP:conf/lics/LICS3}
614}
615
616@INPROCEEDINGS{DBLP:conf/iccad/ManoliosSV06,
617  author = {Panagiotis Manolios and Sudarshan K. Srinivasan and Daron Vroon},
618  title = {Automatic memory reductions for RTL model verification},
619  booktitle = {ICCAD},
620  year = {2006},
621  pages = {786-793},
622  bibsource = {DBLP, http://dblp.uni-trier.de},
623  crossref = {DBLP:conf/iccad/2006},
624  ee = {http://doi.acm.org/10.1145/1233501.1233663},
625  file = {:Abstraction/AutomaticMemoryReductionforRTL06.pdf:PDF},
626  keywords = {Abstraction, memory}
627}
628
629@INPROCEEDINGS{mcmillan98tomasulo,
630  author = {K.L.~McMillan},
631  title = {Verification of an {I}mplementation of {T}omasulo's {A}lgorithm by
632        {C}ompositional {M}odel {C}hecking.},
633  booktitle = {C{AV}'98: {P}roceddings of the 10th {I}nternational {C}onference
634        on {C}omputer {A}ided {V}erification},
635  year = {1998},
636  editor = {Alan J. Hu, Moshe Y. Vardi},
637  volume = {1427},
638  series = {Lecture Notes in Computer Science},
639  pages = {110-121},
640  address = {Vancouver, Canada},
641  bibsource = {DBLP, http://dblp.uni-trier.de},
642  crossref = {DBLP:conf/cav/1998}
643}
644
645@INPROCEEDINGS{mcmillan02applyingSat,
646  author = {Kenneth L. McMillan},
647  title = {Applying SAT Methods in Unbounded Symbolic Model Checking},
648  booktitle = {CAV'02: Proceedings of the 14th International Conference on Computer
649        Aided vVrification},
650  year = {2002},
651  pages = {250-264},
652  bibsource = {DBLP, http://dblp.uni-trier.de},
653  crossref = {DBLP:conf/cav/2002},
654  ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040250.htm},
655  file = {:BMC/Mcmillan02applyingSat.pdf:PDF}
656}
657
658@INPROCEEDINGS{DBLP:conf/cav/McMillan97,
659  author = {Kenneth L. McMillan},
660  title = {{A Compositional Rule for Hardware Design Refinement.}},
661  booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer
662        Aided Verification},
663  year = {1997},
664  volume = {1254},
665  series = {Lecture Notes in Computer Science},
666  pages = {24-35},
667  adress = {Haifa, Israel},
668  bibsource = {DBLP, http://dblp.uni-trier.de},
669  crossref = {DBLP:conf/cav/1997}
670}
671
672@INPROCEEDINGS{Morin-AlloryB06,
673  author = {K.~Morin-Allory and D.~Borrione},
674  title = {Proven {C}orrect {M}onitors from {PSL} {S}pecifications.},
675  booktitle = {D{ATE}'06: {P}roceedings of the {C}onference on {D}esign, {A}utomation
676        and {T}est in {E}urope},
677  year = {2006},
678  editor = {{Georges G. E. Gielen}},
679  pages = {1246-1251},
680  address = {Munich, Germany},
681  organization = {European Design and Automation Association},
682  bibsource = {DBLP, http://dblp.uni-trier.de},
683  crossref = {DBLP:conf/date/2006p},
684  ee = {http://doi.acm.org/10.1145/1131827}
685}
686
687@INPROCEEDINGS{DBLP:conf/dac/MoskewiczMZZM01,
688  author = {M.W.~Moskewicz and C.F.~Madigan and Y.~Zhao and L.~Zhang and S.~Malik},
689  title = {Chaff: Engineering an Efficient SAT Solver},
690  booktitle = {DAC'01: Proceedings of the 38th Design Automation Conference},
691  year = {2001},
692  pages = {530-535},
693  bibsource = {DBLP, http://dblp.uni-trier.de},
694  crossref = {DBLP:conf/dac/2001},
695  ee = {http://jamaica.ee.pitt.edu/Archives/ProceedingArchives/Dac/Dac2001/papers/2001/dac01/pdffiles/33_1.pdf},
696  file = {:SAT/4 - moskewicz01chaff.pdf:PDF}
697}
698
699@INPROCEEDINGS{DBLP:conf/sbmf/MouraB09,
700  author = {Leonardo Mendon\c{c}a de Moura and Nikolaj Bj{\o}rner},
701  title = {Satisfiability Modulo Theories: An Appetizer},
702  booktitle = {SBMF},
703  year = {2009},
704  pages = {23-36},
705  bibsource = {DBLP, http://dblp.uni-trier.de},
706  crossref = {DBLP:conf/sbmf/2009},
707  ee = {http://dx.doi.org/10.1007/978-3-642-10452-7_3}
708}
709
710@INPROCEEDINGS{DBLP:conf/tacas/MouraB08,
711  author = {Leonardo Mendon\c{c}a de Moura and Nikolaj Bj{\o}rner},
712  title = {Z3: An Efficient SMT Solver},
713  booktitle = {TACAS},
714  year = {2008},
715  pages = {337-340},
716  bibsource = {DBLP, http://dblp.uni-trier.de},
717  crossref = {DBLP:conf/tacas/2008},
718  ee = {http://dx.doi.org/10.1007/978-3-540-78800-3_24}
719}
720
721@INPROCEEDINGS{DBLP:conf/cav/Namjoshi03,
722  author = {Kedar S. Namjoshi},
723  title = {Abstraction for Branching Time Properties.},
724  booktitle = {CAV},
725  year = {2003},
726  pages = {288-300},
727  bibsource = {DBLP, http://dblp.uni-trier.de},
728  crossref = {DBLP:conf/cav/2003},
729  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2725{\&}spage=288},
730  file = {abstractforbtl.pdf:/dsk/l1/misc/doc/ctl_auto/abstractforbtl.pdf:PDF},
731  keywords = {abstraction}
732}
733
734@INPROCEEDINGS{DBLP:conf/date/NanshiS08,
735  author = {K.~Nanshi and F.~Somenzi},
736  title = {Improved Visibility in One-to-Many Trace Concretization},
737  booktitle = {DATE},
738  year = {2008},
739  pages = {819-824},
740  bibsource = {DBLP, http://dblp.uni-trier.de},
741  crossref = {DBLP:conf/date/2008},
742  ee = {http://dx.doi.org/10.1109/DATE.2008.4484775}
743}
744
745@INPROCEEDINGS{DBLP:conf/dac/NanshiS06,
746  author = {K.~Nanshi and F.~Somenzi},
747  title = {Guiding simulation with increasingly refined abstract traces},
748  booktitle = {DAC},
749  year = {2006},
750  pages = {737-742},
751  bibsource = {DBLP, http://dblp.uni-trier.de},
752  crossref = {DBLP:conf/dac/2006},
753  ee = {http://doi.acm.org/10.1145/1146909.1147097}
754}
755
756@INPROCEEDINGS{nejati05stutering,
757  author = {Shiva Nejati and Arie Gurfinkel and Marsha Chechik},
758  title = {Stuttering Abstraction for Model Checking},
759  booktitle = {SEFM},
760  year = {2005},
761  pages = {311-320},
762  bibsource = {DBLP, http://dblp.uni-trier.de},
763  crossref = {DBLP:conf/sefm/2005},
764  ee = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.44},
765  file = {nejati05.pdf:/dsk/l1/misc/doc/abstraction/nejati05.pdf:PDF}
766}
767
768@INPROCEEDINGS{DBLP:conf/tcs/Park81,
769  author = {D.~Park},
770  title = {{Concurrency and Automata on Infinite Sequences.}},
771  booktitle = {Proceedings of the 5th GI-Conference on Theoretical Computer Science},
772  year = {1981},
773  pages = {167-183},
774  bibsource = {DBLP, http://dblp.uni-trier.de},
775  crossref = {DBLP:conf/tcs/1981}
776}
777
778@INPROCEEDINGS{peng02tableau,
779  author = {H.~Peng and Y.~Mokhtari and S.~Tahar},
780  title = {Environment {S}ynthesis for {C}ompositional {M}odel {C}hecking.},
781  booktitle = {I{CCD}'02: {P}roceedings of the 20th {I}nternational {C}onference
782        on {C}omputer {D}esign},
783  year = {2002},
784  pages = {70-},
785  address = {Freiburg, Germany},
786  publisher = {IEEE Computer Society},
787  bibsource = {DBLP, http://dblp.uni-trier.de},
788  crossref = {DBLP:conf/iccd/2002},
789  ee = {http://csdl.computer.org/comp/proceedings/iccd/2002/1700/00/17000070abs.htm}
790}
791
792@INPROCEEDINGS{RaviS04MinimalAssig,
793  author = {K.~Ravi and F.~Somenzi},
794  title = {Minimal Assignments for Bounded Model Checking},
795  booktitle = {TACAS'04: Proceedings of 10th International Conference on Tools and
796        Algorithms for the Construction and Analysis of Systems},
797  year = {2004},
798  series = {LNCS},
799  pages = {31-45},
800  bibsource = {DBLP, http://dblp.uni-trier.de},
801  crossref = {DBLP:conf/tacas/2004},
802  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2988{\&}spage=31},
803  file = {:SAT/minimal_assignment_for_bmc.pdf:PDF}
804}
805
806@INPROCEEDINGS{DBLP:conf/cav/RoordaC06,
807  author = {Jan-Willem Roorda and Koen Claessen},
808  title = {SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory
809        Evaluation},
810  booktitle = {CAV},
811  year = {2006},
812  pages = {175-189},
813  bibsource = {DBLP, http://dblp.uni-trier.de},
814  crossref = {DBLP:conf/cav/2006},
815  ee = {http://dx.doi.org/10.1007/11817963_19}
816}
817
818@INPROCEEDINGS{roux03ctl,
819  author = {C.~Roux and E.~Encrenaz},
820  title = {CTL May Be Ambiguous When Model Checking Moore Machines.},
821  booktitle = {CHARME},
822  year = {2003},
823  pages = {164-169},
824  bibsource = {DBLP, http://dblp.uni-trier.de},
825  crossref = {DBLP:conf/charme/2003},
826  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2860{\&}spage=164},
827  file = {rouxctl.pdf:/dsk/l1/misc/doc/modular/model_checking/rouxctl.pdf:PDF},
828  keywords = {CTL},
829  owner = {cecile},
830  timestamp = {2006.02.28},
831  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2860&spage=164}
832}
833
834@INPROCEEDINGS{DBLP:conf/date/RoychoudhuryMK03,
835  author = {Abhik Roychoudhury and Tulika Mitra and S. R. Karri},
836  title = {Using Formal Techniques to Debug the AMBA System-on-Chip Bus Protocol.},
837  booktitle = {DATE},
838  year = {2003},
839  pages = {10828-10833},
840  bibsource = {DBLP, http://dblp.uni-trier.de},
841  crossref = {DBLP:conf/date/2003},
842  ee = {http://csdl.computer.org/comp/proceedings/date/2003/1870/01/187010828abs.htm},
843  keywords = {AMBA}
844}
845
846@INPROCEEDINGS{shohamG04monotonic,
847  author = {S.~Shoham and O.~Grumberg},
848  title = {Monotonic {A}bstraction-{R}efinement for {CTL}.},
849  booktitle = {T{ACAS}'04: {P}roceedings of the 10th {I}nternational {C}onference
850        on {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis
851        of {S}ystems},
852  year = {2004},
853  editor = {Kurt Jensen, Andreas Podelski},
854  volume = {2988},
855  series = {Lecture Notes in Computer Science},
856  pages = {546-560},
857  address = {Barcelona, Spain},
858  bibsource = {DBLP, http://dblp.uni-trier.de},
859  crossref = {DBLP:conf/tacas/2004},
860  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2988{\&}spage=546},
861  file = {monotone-abs-ref.ps:/dsk/l1/misc/doc/ctl_auto/monotone-abs-ref.ps:PDF},
862  keywords = {CTL , abstraction , 3-valued , refinment loop}
863}
864
865@INPROCEEDINGS{somenzi00efficient,
866  author = {F.~Somenzi and R.~Bloem},
867  title = {Efficient B{\"u}chi Automata from LTL Formulae.},
868  booktitle = {CAV},
869  year = {2000},
870  pages = {248-263},
871  bibsource = {DBLP, http://dblp.uni-trier.de},
872  crossref = {DBLP:conf/cav/2000},
873  file = {wring.ps:/dsk/l1/misc/doc/ltl_auto/wring.ps:PDF},
874  keywords = {LTL, automata approach,},
875  owner = {cecile},
876  timestamp = {2006.02.13}
877}
878
879@INPROCEEDINGS{StaberFBD06,
880  author = {Stefan Staber and G{\"o}rschwin Fey and Roderick Bloem and Rolf Drechsler},
881  title = {Automatic Fault Localization for Property Checking},
882  booktitle = {Haifa Verification Conference},
883  year = {2006},
884  pages = {50-64},
885  bibsource = {DBLP, http://dblp.uni-trier.de},
886  crossref = {DBLP:conf/hvc/2006},
887  ee = {http://dx.doi.org/10.1007/978-3-540-70889-6_4},
888  file = {:Debug/FaultLocalizationforpropertychecking-CAD06.pdf:PDF},
889  keywords = {Debug, SAT}
890}
891
892@INPROCEEDINGS{DBLP:conf/date/SulflowFBKD09,
893  author = {Andr{\'e} S{\"u}lflow and G{\"o}rschwin Fey and C{\'e}cile Braunstein
894        and Ulrich K{\"u}hne and Rolf Drechsler},
895  title = {Increasing the accuracy of SAT-based debugging},
896  booktitle = {DATE},
897  year = {2009},
898  pages = {1326-1331},
899  bibsource = {DBLP, http://dblp.uni-trier.de},
900  crossref = {DBLP:conf/date/2009},
901  ee = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?isnumber=5090609{\&}arnumber=5090870{\&}count=326{\&}index=256},
902  file = {:Debug/increasingaccuracy-DATE09.pdf:PDF},
903  keywords = {Debug, SAT, localization reduction, abstraction}
904}
905
906@INPROCEEDINGS{DBLP:conf/tacas/VelevB98,
907  author = {Miroslav N. Velev and Randal E. Bryant},
908  title = {Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation},
909  booktitle = {TACAS},
910  year = {1998},
911  pages = {136-150},
912  bibsource = {DBLP, http://dblp.uni-trier.de},
913  crossref = {DBLP:conf/tacas/1998},
914  ee = {http://link.springer.de/link/service/series/0558/bibs/1384/13840136.htm},
915  file = {:Abstraction/EfficientModelingMemoryArraySymbolicTernarySimulation98.pdf:PDF},
916  keywords = {Abstraction, Memory, STE}
917}
918
919@PROCEEDINGS{DBLP:conf/charme/2003,
920  title = {Correct Hardware Design and Verification Methods CHARME 2003},
921  year = {2003},
922  editor = {Daniel Geist and Enrico Tronci},
923  volume = {2860},
924  series = {Lecture Notes in Computer Science},
925  publisher = {Springer},
926  crossref = {DBLP:conf/charme/2003},
927  owner = {cecile},
928  timestamp = {2006.02.02}
929}
930
931@MANUAL{rulebase06userguide,
932  title = {RuleBase Parallel Edition,User's Guide},
933  author = {Model Checking Systems group},
934  organization = {IBM Labs},
935  address = {Haifa, Israel},
936  year = {2005},
937  note = {verion 1.26},
938  owner = {cecile},
939  timestamp = {2007.03.07}
940}
941
942@INPROCEEDINGS{Vis,
943  author = {The {VIS} group},
944  title = {{VIS} : {A} {S}ystem for {V}erification and {S}ynthesis},
945  booktitle = {CAV'96: Proceedings of the 8th International Conference on Computer
946        Aided Verification},
947  year = {1996},
948  editor = {{Rajeev Alur} and {Thomas A. Henzinger}},
949  volume = {1102},
950  series = {Lecture Notes in Computer Science},
951  pages = {428--432},
952  address = {New Brunswick, NJ, USA},
953  publisher = {Springer-Verlag},
954  abstract = {Manual abstraction can be performed by giving a file containing the
955        names of variables to abstract. For each variable appearing in the
956        file, a new primary input node is created to drive all the nodes
957        that were previously driven by the variable. Abstracting a net effectively
958        allows it to take any value in its range, at every clock cycle. Fair
959        CTL model checking and language emptiness check VIS performs fair
960        CTL model checking under Buchi fairness constraints. In addition,
961        VIS can perform ...},
962  citeseerurl = {citeseer.ist.psu.edu/brayton96vis.html},
963  comment = {Proceedings of the Eighth International Conference on Computer Aided
964        Verification},
965  keywords = {model checker},
966  url = {citeseer.ist.psu.edu/brayton96vis.html}
967}
968
969@ARTICLE{DBLP:journals/fmsd/CohenN09,
970  author = {Ariel Cohen 0002 and Kedar S. Namjoshi},
971  title = {Local proofs for global safety properties},
972  journal = {Formal Methods in System Design},
973  year = {2009},
974  volume = {34},
975  pages = {104-125},
976  number = {2},
977  bibsource = {DBLP, http://dblp.uni-trier.de},
978  ee = {http://dx.doi.org/10.1007/s10703-008-0063-8},
979  keywords = {Refinement}
980}
981
982@ARTICLE{akers78,
983  author = {B.~Akers},
984  title = {Binary Decision Diagrams},
985  journal = {IEEE Transactions on Computers},
986  year = {1978},
987  volume = {27},
988  pages = {509--516},
989  number = {6},
990  abstract = { The seminal paper in which BDD's were introduced. Note that none
991        of the today implementation techniques for BDD package is given in
992        this paper. },
993  keywords = {BDD description}
994}
995
996@INPROCEEDINGS{alfaro01interface,
997  author = {L.~de Alfaro and T.A.~Henzinger},
998  title = {Interface automata},
999  booktitle = {ESEC/FSE-9: Proceedings of the 8th European software engineering
1000        conference held jointly with 9th ACM SIGSOFT international symposium
1001        on Foundations of software engineering},
1002  year = {2001},
1003  pages = {109--120},
1004  address = {New York, NY, USA},
1005  publisher = {ACM Press},
1006  doi = {http://doi.acm.org/10.1145/503209.503226},
1007  isbn = {1-58113-390-1},
1008  location = {Vienna, Austria}
1009}
1010
1011@INPROCEEDINGS{bhdl03,
1012  author = {A.~Aljer and P.~Devienne and S.~Tison and J-L.~Boulanger and G.~Mariano},
1013  title = {{BHDL: Circuit Design in B}},
1014  booktitle = {ACSD '03: Proceedings of the Third International Conference on Application
1015        of Concurrency to System Design},
1016  year = {2003},
1017  editor = {IEEE Computer Society},
1018  pages = {241},
1019  address = {Washington, DC, USA},
1020  isbn = {0-7695-1887-7}
1021}
1022
1023@INPROCEEDINGS{alur99automating,
1024  author = {R. Alur and L.~de Alfaro and T. A. Henzinger and F.~Y.C. Mang},
1025  title = {Automating Modular Verification},
1026  booktitle = {CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven,
1027        The Netherlands, August 24-27, 1999, Proceedings},
1028  year = {1999},
1029  editor = {Jos C. M. Baeten and Sjouke Mauw},
1030  volume = {1664},
1031  series = {Lecture Notes in Computer Science},
1032  pages = {82-97},
1033  address = {Eindhoven, The Netherlands},
1034  publisher = {Springer},
1035  abstract = {Modular techniques for automatic verification attempt to overcome
1036        the state-explosion problem by exploiting the modular structure naturally
1037        present in many system designs. Unlike other tasks in the verification
1038        of finite-state systems, current modular techniques rely heavily
1039        on user guidance. In particular, the user is typically required to
1040        construct module abstractions that are neither too detailed as to
1041        render insufficient benefits in state exploration, nor too coarse
1042        as to invalidate the desired system properties. In this paper, we
1043        construct abstract modules automatically, using reachability and
1044        controllability information about the concrete modules. This allows
1045        us to leverage automatic verification techniques by applying them
1046        in layers: first we compute on the state spaces of system components,
1047        then we use the results for constructing abstractions, and finally
1048        we compute on the abstract state space of the system. Our experimental
1049        results indicate that if reachability and controllabil ity information
1050        is used in the construction of abstractions, the resulting abstract
1051        modules are often significantly smaller than the concrete modules
1052        and can drastically reduce the space and time requirements for verification.},
1053  file = {automatic_modular.pdf:/dsk/l1/misc/doc/modular/modular/automatic_modular.pdf:PDF},
1054  keywords = {modular, abstraction, refinment loop, case study},
1055  owner = {cecile},
1056  timestamp = {2006.02.06},
1057  url = {http://link.springer.de/link/service/series/0558/bibs/1664/16640082.htm}
1058}
1059
1060@ARTICLE{DBLP:journals/fmsd/AlurH99b,
1061  author = {R.~Alur and T.A.~Henzinger},
1062  title = {Reactive Modules.},
1063  journal = {Formal Methods in System Design},
1064  year = {1999},
1065  volume = {15},
1066  pages = {7-48},
1067  number = {1},
1068  bibsource = {DBLP, http://dblp.uni-trier.de},
1069  publisher = {Springer}
1070}
1071
1072@INPROCEEDINGS{alur98mocha,
1073  author = {R.~Alur and T.A.~Henzinger and F.Y. C.~Mang and S.~Qadeer and S.K.~Rajamani
1074        and S.~Tasiran},
1075  title = {{MOCHA}: {M}odularity in {M}odel {C}hecking},
1076  booktitle = {CAV'98: Proceedings of the 10th International Conference on Computer
1077        Aided Verification},
1078  year = {1998},
1079  volume = {1427},
1080  series = {Lecture Notes in Computer Science},
1081  pages = {521-525},
1082  address = {London, UK},
1083  abstract = {We describe a new interactive verification environment called Mocha
1084        for modular verification of heterogeneous systems. Mocha differs
1085        from existing model checkers in three important ways. First, instead
1086        of manipulating unstructured statetransition graphs, it supports
1087        the heterogeneous modeling framework of Reactive Modules. Second,
1088        instead of traditional temporal logics such as CTL, it uses Alternating
1089        Temporal Logic (ATL), a temporal logic that is designed to specify
1090        collaborative as ...},
1091  file = {alur98mocha.ps.gz:/dsk/l1/misc/doc/modular/mocha/alur98mocha.ps.gz:PDF},
1092  keywords = {model checker, atl, modular}
1093}
1094
1095@INPROCEEDINGS{amla01assume,
1096  author = {N.~Amla and E.~A.~Emerson and K.~S.~Namjoshi and R.~J.~Trefler},
1097  title = {Assume-Guarantee Based Compositional Reasoning for Synchronous Timing
1098        Diagrams},
1099  booktitle = {TACAS 2001: Proceedings of the 7th International Conference on Tools
1100        and Algorithms for the Construction and Analysis of Systems},
1101  year = {2001},
1102  pages = {465--479},
1103  address = {London, UK},
1104  publisher = {Springer-Verlag},
1105  isbn = {3-540-41865-2}
1106}
1107
1108@ARTICLE{arieliA98value,
1109  author = {Ofer Arieli and Arnon Avron},
1110  title = {The Value of the Four Values.},
1111  journal = {Artif. Intell.},
1112  year = {1998},
1113  volume = {102},
1114  pages = {97-141},
1115  number = {1},
1116  bibsource = {DBLP, http://dblp.uni-trier.de},
1117  ee = {http://dx.doi.org/10.1016/S0004-3702(98)00032-0},
1118  file = {arieli98four.ps:/dsk/l1/misc/doc/logique/arieli98four.ps:PDF},
1119  keywords = {4-valued, logic}
1120}
1121
1122@BOOK{arnold94finite,
1123  title = {Finite {T}ransition {S}ystems: {S}emantics of {C}ommunicating {S}ystems},
1124  publisher = {Prentice Hall International Ltd.},
1125  year = {1994},
1126  editor = {Translator-John Plaice},
1127  author = {A.~Arnold},
1128  address = {Hertfordshire,UK},
1129  isbn = {0-13-092990-5},
1130  keywords = {simulation}
1131}
1132
1133@ARTICLE{DBLP:journals/entcs/AwedhS06,
1134  author = {M.~Awedh and F.~Somenzi},
1135  title = {Termination Criteria for Bounded Model Checking: Extensions and Comparison},
1136  journal = {Electronic Notes in Theoritical Computer Science.},
1137  year = {2006},
1138  volume = {144},
1139  pages = {51-66},
1140  number = {1},
1141  bibsource = {DBLP, http://dblp.uni-trier.de},
1142  ee = {http://dx.doi.org/10.1016/j.entcs.2005.07.019},
1143  file = {:BMC/TerminationCriteriaForBMC06.pdf:PDF},
1144  keywords = {BMC, VIS}
1145}
1146
1147@MANUAL{bmanual,
1148  title = {{B-Toolkit User's Manual}},
1149  author = {{B-Core(UK) Ltd.}},
1150  edition = {release 3.7},
1151  year = {1997},
1152  keywords = {b method},
1153  owner = {cecile},
1154  timestamp = {2006.07.31},
1155  url = {http://www.b-core.com/downloading.html}
1156}
1157
1158@INPROCEEDINGS{BP-msr03,
1159  author = {M.~Baclet and R.~Pacalet},
1160  title = {V{\'e}rifications du protocole~{VCI}},
1161  booktitle = {{A}ctes du 4{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes
1162        {R}{\'e}actifs ({MSR}'03)},
1163  year = {2003},
1164  editor = {M{\'e}ry, Dominique and Rezg, Nidhal and Xie, Xiaolan},
1165  pages = {431-445},
1166  address = {Metz, France},
1167  month = oct,
1168  publisher = {Herm{\`e}s},
1169  keywords = {protocol},
1170  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/vci-msr03.ps}
1171}
1172
1173@INPROCEEDINGS{broissyval,
1174  author = {F.~Badeau and A.~Amelot},
1175  title = {{Using B as a High Level Programming Language in an Industrial Project:
1176        Roissy VAL}},
1177  booktitle = {ZB 2005: Formal Specification and Development in Z and B},
1178  year = {2005},
1179  volume = {3455/2005},
1180  series = {Lecture Notes in Computer Science},
1181  pages = {334-354},
1182  publisher = {Springer Berlin / Heidelberg},
1183  doi = {10.1007/11415787_20},
1184  keywords = {b method},
1185  owner = {cecile},
1186  timestamp = {2007.01.31},
1187  url = {http://www.springerlink.com/content/x8mcgk2p8r82e2gl/}
1188}
1189
1190@INPROCEEDINGS{503274,
1191  author = {T.~Ball and S.K.~Rajamani},
1192  title = {The {SLAM} project: debugging system software via static analysis},
1193  booktitle = {POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on
1194        Principles of programming languages},
1195  year = {2002},
1196  pages = {1--3},
1197  address = {New York, NY, USA},
1198  doi = {http://doi.acm.org/10.1145/503272.503274},
1199  isbn = {1-58113-450-9},
1200  keywords = {CEGAR, refinment loop, model checking software},
1201  location = {Portland, Oregon},
1202  owner = {cecile},
1203  timestamp = {2007.01.14}
1204}
1205
1206@INPROCEEDINGS{rulebase96,
1207  author = {I.~Beer and S.~Ben-David and C.~Eisner and A.~Landver},
1208  title = {{RuleBase: an industry-oriented formal verification tool}},
1209  booktitle = {DAC '96: Proceedings of the 33rd annual conference on Design automation},
1210  year = {1996},
1211  series = {ACM Press},
1212  pages = {655--660},
1213  address = {New York, NY, USA},
1214  doi = {http://doi.acm.org/10.1145/240518.240642},
1215  isbn = {0-89791-779-0},
1216  location = {Las Vegas, Nevada, United States},
1217  owner = {cecile},
1218  timestamp = {2007.01.31}
1219}
1220
1221@INPROCEEDINGS{1517440,
1222  author = {Bjesse, Per},
1223  title = {Word-level sequential memory abstraction for model checking},
1224  booktitle = {FMCAD '08: Proceedings of the 2008 International Conference on Formal
1225        Methods in Computer-Aided Design},
1226  year = {2008},
1227  pages = {1--9},
1228  address = {Piscataway, NJ, USA},
1229  publisher = {IEEE Press},
1230  file = {:Cegar/worllevelSeqMemAbstrforMCbjesse08.pdf:PDF},
1231  isbn = {978-1-4244-2735-2},
1232  keywords = {Abstractions, Model-checking},
1233  location = {Portland, Oregon}
1234}
1235
1236@TECHREPORT{prosyd05,
1237  author = {R. Bloem and B. Jobstmann and A. Pnueli.},
1238  title = {{Property-based Logic Synthesis for Rapid Design Prototyping}},
1239  institution = {Prosyd Deliverable D2.2/1},
1240  year = {2005},
1241  owner = {cecile},
1242  timestamp = {2007.02.07}
1243}
1244
1245@ARTICLE{bozga97protocol,
1246  author = {M.~Bozga and J-C.~Fernandez and A.~Kerbrat and L.~Mounier},
1247  title = {Protocol {V}erification with the {ALD{\'E}BARAN} {T}oolset.},
1248  journal = {STTT},
1249  year = {1997},
1250  volume = {1},
1251  pages = {166-184},
1252  number = {1-2},
1253  bibsource = {DBLP, http://dblp.uni-trier.de},
1254  ee = {http://link.springer.de/link/service/journals/10009/bibs/7001001/70010166.htm},
1255  keywords = {model checking, model checker},
1256  publisher = {Springer}
1257}
1258
1259@TECHREPORT{Brady:EECS-2008-136,
1260  author = {Brady, Bryan and Bryant, Randal and Seshia, Sanjit A.},
1261  title = {Abstracting RTL Designs to the Term Level},
1262  institution = {EECS Department, University of California, Berkeley},
1263  year = {2008},
1264  number = {UCB/EECS-2008-136},
1265  month = {Oct},
1266  abstract = {Term-level verification is a formal technique that seeks to verify
1267        RTL hardware descriptions by abstracting away details of data representations
1268        and operations. The key to making term-level verification automatic
1269        and efficient is in deciding what to abstract. We investigate this
1270        question in this paper and propose a solution based on the use of
1271        type qualifiers. First, we demonstrate through case studies that
1272        only selective term-level abstraction can be very effective in reducing
1273        the run-time of formal tools while still retaining precision of analysis.
1274        Second, the term-level abstraction process can be guided using lightweight
1275        type qualifiers. We present an annotation language and type inference
1276        scheme that is applied to the formal verification of the Verilog
1277        implementation of a chip multiprocessor router. Experimental results
1278        indicate type-based selective term-level abstraction is effective
1279        at scaling up verification with minimal designer guidance.},
1280  file = {:Abstraction/abstractingRTLtoTermLevel.pdf:PDF},
1281  keywords = {Abstraction, memory},
1282  owner = {cecile},
1283  timestamp = {2010.06.10},
1284  url = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-136.html}
1285}
1286
1287@PHDTHESIS{braunstein_phd07,
1288  author = {C.~Braunstein},
1289  title = {"Conception Incrémentale, Vérification de Composants Matériels et
1290        Méthode d'abstraction pour la Vérification de SystÚmes Intégrés sur
1291        Puce"},
1292  school = {{Universitée Pierre et Marie Curie (Paris 6)}},
1293  year = {2007},
1294  address = {LIP6/SOC},
1295  owner = {cecile},
1296  timestamp = {2007.04.16}
1297}
1298
1299@TECHREPORT{cecile03dea,
1300  author = {C.~Braunstein},
1301  title = {{Transformation de propri\'et\'es CTL lors d'une m\'ethode de conception
1302        incr\'ementale des wrappers {VCI/PI}}},
1303  institution = {LIP6/ASIM},
1304  year = {2003},
1305  type = {Rapport de {DEA}},
1306  owner = {cecile},
1307  timestamp = {2006.09.07}
1308}
1309
1310@ARTICLE{braunstein06sttt,
1311  author = {C.~Braunstein and E.~Encrenaz},
1312  title = {{CTL}-property {T}ransformations along an {I}ncremental {D}esign
1313        {P}rocess},
1314  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
1315  year = {2007},
1316  volume = {9},
1317  pages = {77--88},
1318  number = {1},
1319  note = {A long version including the proof is available at www-asim.lip6.fr/~cecile},
1320  owner = {cecile},
1321  publisher = {Springer},
1322  timestamp = {2006.09.05}
1323}
1324
1325@INPROCEEDINGS{braunstein07acsd,
1326  author = {C.~Braunstein and E.~Encrenaz},
1327  title = {Using CTL formulae as Component Abstraction in a Design and Verification
1328        Flow},
1329  booktitle = {ACSD'07: Proceedings of the 7th International Conference on Application
1330        of Concurrency to System Design},
1331  year = {2007},
1332  note = {accepted},
1333  keywords = {Abstraction, CEGAR, CTL},
1334  owner = {cecile},
1335  timestamp = {2007.03.27}
1336}
1337
1338@INPROCEEDINGS{braunstein06lpar,
1339  author = {C.~Braunstein and E.~Encrenaz},
1340  title = {A Further Step in the Incremental Design Process: Incorporation of
1341        an Increment Specification},
1342  booktitle = {LPAR'06: Proceeding of the 13th International Conference on Logic
1343        for Programming, Artificial Intelligence, and Reasoning},
1344  year = {2006},
1345  note = {{\it short paper}, proceedings online \url{http://www.lix.polytechnique.fr/~hermann/LPAR2006/}},
1346  owner = {cecile},
1347  timestamp = {2007.03.27}
1348}
1349
1350@TECHREPORT{Braunstein_Encrenaz_RR_LIP6_07_2006,
1351  author = {C.~Braunstein and E.~Encrenaz},
1352  title = {Using CTL formulae as component abstraction},
1353  institution = {UPMC/LIP6},
1354  year = {2006},
1355  type = {Research report},
1356  owner = {cecile},
1357  timestamp = {2006.09.29}
1358}
1359
1360@INPROCEEDINGS{pipeline06,
1361  author = {C.~Braunstein and E.~Encrenaz},
1362  title = {Formalizing the Incremental Design and Verification Process of a
1363        Pipelined Protocol Converter},
1364  booktitle = {RSP '06: Proceedings of the Seventeenth IEEE International Workshop
1365        on Rapid System Prototyping (RSP'06)},
1366  year = {2006},
1367  pages = {103--109},
1368  address = {Washington, DC, USA},
1369  publisher = {IEEE Computer Society},
1370  doi = {http://dx.doi.org/10.1109/RSP.2006.19},
1371  isbn = {0-7695-2580-6},
1372  owner = {cecile},
1373  timestamp = {2006.08.31}
1374}
1375
1376@ARTICLE{avocs_incr,
1377  author = {C.~Braunstein and E.~Encrenaz},
1378  title = {{CTL}-{P}roperty {T}ransformations along an {I}ncremental {D}esign
1379        {P}rocess},
1380  journal = {Electronic Notes in Theoretical Computer Science},
1381  year = {2005},
1382  volume = {128},
1383  pages = {263--278},
1384  number = {6},
1385  file = {braunstein_avocs_o4.pdf:/dsk/l1/misc/Article/Concep_incr/Avocs/Avocs_paper/braunstein_avocs_o4.pdf:PDF},
1386  issue = {6},
1387  publisher = {Elsevier},
1388  series = {AVOCS'04~-~Proceedings of the 4th International Workshop on Automated
1389        Verification of Critical Systems}
1390}
1391
1392@ARTICLE{browneclarkegrum88,
1393  author = {M.C.~Browne and E.M.~Clarke and O.~Grumberg},
1394  title = {Characterizing {F}inite {K}ripke {S}tructures in {P}ropositional
1395        {T}emporal {L}ogic},
1396  journal = {Theoritical Computer Science},
1397  year = {1988},
1398  volume = {59},
1399  pages = {115--131},
1400  number = {1-2},
1401  doi = {http://dx.doi.org/10.1016/0304-3975(88)90098-9},
1402  issn = {0304-3975},
1403  publisher = {Elsevier Science Publishers Ltd.}
1404}
1405
1406@ARTICLE{Bryant86,
1407  author = {R.E.~Bryant},
1408  title = {{Graph-Based Algorithms for Boolean Function Manipulation}},
1409  journal = {IEEE Transactions on Computers},
1410  year = {1986},
1411  volume = {35},
1412  pages = {677-691},
1413  number = {8},
1414  bibsource = {DBLP, http://dblp.uni-trier.de},
1415  keywords = {BDD},
1416  owner = {cecile},
1417  timestamp = {2006.11.07}
1418}
1419
1420@INPROCEEDINGS{bunker:idpt02,
1421  author = {A.~Bunker and G.~Gopalakrishnan},
1422  title = {{Verifying a VCI Bus Interface Model Using an LSC-based Specification}},
1423  booktitle = {Proceedings of the Sixth Biennial World Conference on Integrated
1424        Design and Process Technology},
1425  year = {2002},
1426  editor = {H. Ehrig and B. J. Kr\"amer and A. Ertas},
1427  pages = {48},
1428  month = {June},
1429  organization = {Society of Design and Process Science},
1430  keywords = {protocol},
1431  url = {http://www.engineering.usu.edu/ece/faculty/bunker/pubs/idpt02.pdf}
1432}
1433
1434@ARTICLE{macmillan,
1435  author = {J.R.~Burch and E.M.~Clarke and K.L.~McMillan and D.L.~Dill and L.J.~Hwang},
1436  title = {Symbolic {M}odel {C}hecking: $10^{20}$ {S}tates and {B}eyond},
1437  journal = {{I}nformation and {C}omputation },
1438  year = {1992},
1439  volume = {98},
1440  pages = {142--170},
1441  number = {2},
1442  note = {Special issue for best papers from LICS'90},
1443  address = {Duluth, MN, USA},
1444  publisher = {Academic Press, Inc.}
1445}
1446
1447@INPROCEEDINGS{burch94automatic,
1448  author = {J.R.~Burch and D.L.~Dill},
1449  title = {Automatic {V}erification of {P}ipelined {M}icroprocessors {C}ontrol},
1450  booktitle = {Proceedings of the sixth International Conference on Computer-Aided
1451        Verification {CAV'94}},
1452  year = {1994},
1453  editor = {{D.L.~Dill}},
1454  volume = {LNCS 818},
1455  pages = {68--80},
1456  address = {Standford, California, USA},
1457  publisher = {Springer-Verlag},
1458  citeseerurl = {citeseer.ist.psu.edu/burch94automatic.html},
1459  keywords = {model checking, pipeline, archi},
1460  url = {citeseer.ist.psu.edu/burch94automatic.html}
1461}
1462
1463@ARTICLE{bryant82,
1464  author = {J.R.~Burch and D.L.~Dill},
1465  title = {Graph-Based Algorithms for Boolean Function Manipulation},
1466  journal = {IEEE Transactions on Computers},
1467  year = {1982},
1468  volume = {35},
1469  pages = {677--691},
1470  number = {8},
1471  month = {August},
1472  abstract = {Available}
1473}
1474
1475@INPROCEEDINGS{Cabodi09Speeding,
1476  author = {G. Cabodi and P. Camurati and L. Garcia and M. Murciano and S. Nocco
1477        and S. Quer},
1478  title = {Speeding up Model Checking by Exploiting Explicit and Hidden Verification
1479        Constraints},
1480  booktitle = {DATE '09: Proceedings of the conference on Design, Automation and
1481        Test in Europe},
1482  year = {2009},
1483  pages = {1686-1691},
1484  file = {:Composition/Speeding up MC by exploiting Explicit09.PDF:PDF},
1485  keywords = {Composition , model checking},
1486  owner = {cecile},
1487  timestamp = {2009.04.30}
1488}
1489
1490@INCOLLECTION{Cansell2001AbstractionandRefinementofFeatures,
1491  author = {D.~Cansell and D.~M{\'e}ry},
1492  title = {Abstraction and {R}efinement of {F}eatures},
1493  booktitle = {{Language Constructs for Designing Features}},
1494  publisher = {Springer-Verlag},
1495  year = {2001},
1496  editor = {S.~Gilmore and M.~Ryan},
1497  pages = {65--84},
1498  abstract = {The composition of services and features often leads to unwanted situations,
1499        because it is a non-monotonic operation over services and features.
1500        When a new service is added to an existing system, conditions have
1501        to be checked to ensure that the resulting system satisfies a list
1502        of required properties. Following the system approach of Abrial,
1503        we develop services and features in an incremental way and use refinement
1504        to model the composition of services and features. Proof obligations
1505        state the preservation or the non-preservation of properties, namely
1506        invariant or more generally safety properties. The method helps us
1507        in understanding when a service is interfering with another, and
1508        allows us to give multiple views of each service according to the
1509        level of its refinement. Finally, we validate our method with the
1510        Atelier B tool.}
1511}
1512
1513@INCOLLECTION{cassez-proving,
1514  author = {F.~Cassez and M.~Ryan and P-Y.~Schobbens},
1515  title = {Proving {F}eature {N}on-{I}nteraction with {A}lternating-{T}ime {T}emporal
1516        {L}ogic},
1517  booktitle = {{Language Constructs for Describing Features}},
1518  publisher = {Springer Verlag},
1519  year = {2001},
1520  editor = {S.~Gilmore and M.~Ryan},
1521  pages = {85--104}
1522}
1523
1524@ARTICLE{chechik03multi,
1525  author = {M.~Chechik and B.~Devereux and S.~M.~Easterbrook and A.~Gurfinkel},
1526  title = {{Multi-Valued Symbolic Model-Checking}},
1527  journal = {ACM Transactions on Software Engineering and Methodology},
1528  year = {2003},
1529  volume = {12},
1530  pages = {371-408},
1531  number = {4},
1532  bibsource = {DBLP, http://dblp.uni-trier.de},
1533  ee = {http://doi.acm.org/10.1145/990010.990011},
1534  file = {chechik03a.pdf:/dsk/l1/misc/doc/abstraction/chechik03a.pdf:PDF},
1535  keywords = {abstraction, 3-valued, 4-valued, logic, model checking}
1536}
1537
1538@INPROCEEDINGS{846816,
1539  author = {Hoon Choi and Myung-Kyoon Yim and Jae-Young Lee and Byeong-Whee Yun
1540        and Yun-Tae Lee},
1541  title = {Formal Verification of an Industrial System-on-a-Chip},
1542  booktitle = {ICCD '00: Proceedings of the 2000 IEEE International Conference on
1543        Computer Design},
1544  year = {2000},
1545  pages = {453},
1546  address = {Washington, DC, USA},
1547  publisher = {IEEE Computer Society},
1548  isbn = {0-7695-0801-4},
1549  keywords = {AMBA}
1550}
1551
1552@INPROCEEDINGS{CLS00,
1553  author = {G. Ciardo and G. L\"uttgen and R. Siminiceanu},
1554  title = {Efficient Symbolic State-Space Construction for Asynchronous Systems},
1555  booktitle = {Proc. of ICATPN'2000},
1556  year = {2000},
1557  volume = {1825},
1558  series = {Lecture Notes in Computer Science},
1559  pages = {103--122},
1560  publisher = {Springer Verlag}
1561}
1562
1563@ARTICLE{cimatti00nusmv,
1564  author = {A.~Cimatti and E.M.~Clarke and F.~Giunchiglia and M.~Roveri},
1565  title = {NUSMV: A New Symbolic Model Checker.},
1566  journal = {STTT},
1567  year = {2000},
1568  volume = {2},
1569  pages = {410-425},
1570  number = {4},
1571  bibsource = {DBLP, http://dblp.uni-trier.de},
1572  ee = {http://link.springer.de/link/service/journals/10009/bibs/0002004/00020410.htm}
1573}
1574
1575@ARTICLE{DBLP:journals/tocl/CimattiGS10,
1576  author = {Alessandro Cimatti and Alberto Griggio and Roberto Sebastiani},
1577  title = {Efficient generation of craig interpolants in satisfiability modulo
1578        theories},
1579  journal = {ACM Trans. Comput. Log.},
1580  year = {2010},
1581  volume = {12},
1582  pages = {7},
1583  number = {1},
1584  bibsource = {DBLP, http://dblp.uni-trier.de},
1585  ee = {http://doi.acm.org/10.1145/1838552.1838559}
1586}
1587
1588@ARTICLE{Clarke1986,
1589  author = {E.M.~Clarke and E.A.~Emerson and A.P.~Sistla},
1590  title = {Automatic verification of finite-state concurrent systems using temporal
1591        logic specifications},
1592  journal = {ACM Transactions on Programming Languages and Systems},
1593  year = {1986},
1594  volume = {8},
1595  pages = {244--263},
1596  number = {2},
1597  booktitle = {ICATPN'02: Proceedings of the 23rd International Conference on Applications
1598        and Theory of Petri Nets},
1599  doi = {http://doi.acm.org/10.1145/5397.5399},
1600  issn = {0164-0925},
1601  publisher = {ACM Press}
1602}
1603
1604@ARTICLE{clarke94model,
1605  author = {E.M.~Clarke and O.~Grumberg and D.E.~Long},
1606  title = {{Model Checking and Abstraction}},
1607  journal = {ACM Transactions on Programming Languages and Systems},
1608  year = {1994},
1609  volume = {16},
1610  pages = {1512--1542},
1611  number = {5},
1612  address = {New York, NY, USA},
1613  doi = {http://doi.acm.org/10.1145/186025.186051},
1614  issn = {0164-0925},
1615  keywords = {model cheking, abstraction, CTL, preservation},
1616  publisher = {ACM Press}
1617}
1618
1619@BOOK{clarke99model,
1620  title = {Model Checking},
1621  publisher = {The {MIT} {P}ress},
1622  year = {1999},
1623  author = {E.M.~Clarke and O.~Grumberg and D.A.~Peled},
1624  address = {Cambridge, Massachusetts},
1625  isbn = {0-262-03270-8},
1626  keywords = {CTL,LTL, model checking,kripke structure, simulation}
1627}
1628
1629@ARTICLE{Clarke03cegarsymbolic,
1630  author = {E.~M. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith},
1631  title = {Counterexample-guided bstraction refinement for symbolic model checking.},
1632  journal = {Journal of the ACM},
1633  year = {2003},
1634  volume = {50},
1635  pages = {752-794},
1636  number = {5},
1637  bibsource = {DBLP, http://dblp.uni-trier.de},
1638  ee = {http://doi.acm.org/10.1145/876638.876643},
1639  file = {:Cegar/Counterexample-guided abstraction refinement.pdf:PDF},
1640  keywords = {abstraction, CEGAR},
1641  owner = {cecile},
1642  timestamp = {2006.06.27}
1643}
1644
1645@INPROCEEDINGS{DBLP:conf/dac/ClarkeGMZ95,
1646  author = {Edmund M. Clarke and Orna Grumberg and Kenneth L. McMillan and Xudong
1647        Zhao},
1648  title = {Efficient Generation of Counterexamples and Witnesses in Symbolic
1649        Model Checking},
1650  booktitle = {DAC},
1651  year = {1995},
1652  pages = {427-432},
1653  bibsource = {DBLP, http://dblp.uni-trier.de},
1654  ee = {http://doi.acm.org/10.1145/217474.217565}
1655}
1656
1657@ARTICLE{DBLP:journals/tcad/ClarkeGS04,
1658  author = {Edmund M. Clarke and Anubhav Gupta and Ofer Strichman},
1659  title = {SAT-based counterexample-guided abstraction refinement},
1660  journal = {IEEE Trans. on CAD of Integrated Circuits and Systems},
1661  year = {2004},
1662  volume = {23},
1663  pages = {1113-1123},
1664  number = {7},
1665  bibsource = {DBLP, http://dblp.uni-trier.de},
1666  ee = {http://doi.ieeecomputersociety.org/10.1109/TCAD.2004.829807},
1667  file = {:Cegar/SATBasedCegar2004Clarke.pdf:PDF},
1668  keywords = {CEGAR,SAT},
1669  owner = {cecile},
1670  timestamp = {2010.06.03}
1671}
1672
1673@MISC{tata97,
1674  author = {H. Comon and M. Dauchet and R. Gilleron and F. Jacquemard and D.
1675        Lugiez and S. Tison and M. Tommasi},
1676  title = {Tree Automata Techniques and Applications},
1677  howpublished = {Available on: \url{http://www.grappa.univ-lille3.fr/tata}},
1678  year = {1997},
1679  note = {release October, 1rst 2002},
1680  file = {tata.pdf:/dsk/l1/misc/doc/automate/tata.pdf:PDF},
1681  keywords = {tree automata}
1682}
1683
1684@INPROCEEDINGS{madre,
1685  author = {O.~Coudert and J.-C.~Madre},
1686  title = {A New Method to Compute Prime and Essential Prime Implicants of Boolean
1687        Functions},
1688  booktitle = {Advanced Research in VLSI and Parallel Systems},
1689  year = {1992},
1690  editor = {T.~Knight and J.~Savage},
1691  pages = {113--128},
1692  month = {March},
1693  abstract = { This paper presents how prime implicants and essential prime implicants
1694        can be computed by means of meta-products encoded with of BDD's.
1695        It gives the equations that mimic the definitions, but it does not
1696        propose a recursive algorithm. The variable ordering is discussed
1697        and experimental results are provided that come from a benchmark
1698        of circuits. },
1699  keywords = {Prime Implicants}
1700}
1701
1702@INPROCEEDINGS{DBLP:conf/popl/CousotC77,
1703  author = {P.~Cousot and R.~Cousot},
1704  title = {Abstract Interpretation: A Unified Lattice Model for Static Analysis
1705        of Programs by Construction or Approximation of Fixpoints.},
1706  booktitle = {POPL'77: Proceedings of the 14th Annual ACM Symposium on Principles
1707        of Programming Languages},
1708  year = {1977},
1709  pages = {238-252},
1710  address = {Munich, Germany},
1711  bibsource = {DBLP, http://dblp.uni-trier.de},
1712  keywords = {abstraction},
1713  owner = {cecile},
1714  timestamp = {2007.01.13}
1715}
1716
1717@INPROCEEDINGS{jmc-ag-djs:ddd,
1718  author = {J.M.~Couvreur and A.~Griffault and D.J.~Sherman},
1719  title = {Diagrammes de d\'ecision pour la v\'erification de r\'eseaux \`a
1720        files},
1721  booktitle = {Mod\'elisation de syst\`emes r\'eactifs (MSR'99)},
1722  year = {1999},
1723  address = {ENS Cachan},
1724  month = {March}
1725}
1726
1727@INPROCEEDINGS{CA94,
1728  author = {J.M. Couvreur and E. Paviot-Adet},
1729  title = {New Structural Invariants for {P}etri Nets Analysis},
1730  booktitle = {Proc. of ICATPN'94},
1731  year = {1994},
1732  volume = {815},
1733  series = {Lecture Notes in Computer Science},
1734  pages = {199--218},
1735  publisher = {Springer Verlag}
1736}
1737
1738@ARTICLE{dams97abstract,
1739  author = {D.~Dams and R.~Gerth and O.~Grumberg},
1740  title = {Abstract interpretation of reactive systems},
1741  journal = {ACM Transactions on Programming Languages and Systems},
1742  year = {1997},
1743  volume = {19},
1744  pages = {253--291},
1745  number = {2},
1746  address = {New York, NY, USA},
1747  doi = {http://doi.acm.org/10.1145/244795.244800},
1748  issn = {0164-0925},
1749  keywords = {abstraction},
1750  publisher = {ACM Press}
1751}
1752
1753@INPROCEEDINGS{Darbari08transient,
1754  author = {Darbari, A. and Al Hashimi, B. and Harrod, P. and Bradley, D.},
1755  title = {A New Approach for Transient Fault Injection Using Symbolic Simulation},
1756  booktitle = {IEEE International Symposium On-line Testing Symposium},
1757  year = {2008},
1758  pages = {93-98},
1759  month = {July},
1760  doi = {10.1109/IOLTS.2008.59},
1761  journal = {On-Line Testing Symposium, 2008. IOLTS '08. 14th IEEE International},
1762  keywords = {fault tolerance, fault trees, reduced instruction set computing, temporal
1763        logicbinary image, multicycle RISC processor, program image. shadow,
1764        symbolic simulation, transient fault injection}
1765}
1766
1767@MISC{duret03dea,
1768  author = {A.~Duret-Lutz and R.~Rebiha},
1769  title = {SPOT : Une bibliothÚque de vérificaion de propriétés de logique
1770        temporelle à temps linéaire},
1771  year = {2003},
1772  file = {rap_stage_duret_lutz_2003.pdf:/dsk/l1/misc/doc/ltl_auto/rap_stage_duret_lutz_2003.pdf:PDF},
1773  keywords = {LTL, automata approach},
1774  owner = {cecile},
1775  timestamp = {2006.02.13}
1776}
1777
1778@INPROCEEDINGS{dwyer99patterns,
1779  author = {M. B. Dwyer and G. S. Avrunin and J. C. Corbett},
1780  title = {{Patterns in Property Specifications for Finite-State Verification.}},
1781  booktitle = {ICSE' 99. Proceedings of the 1999 International Conference on Software
1782        Engineering},
1783  year = {1999},
1784  editor = {ACM},
1785  pages = {411-420},
1786  address = {Los Angeles, CA, USA},
1787  bibsource = {DBLP, http://dblp.uni-trier.de},
1788  ee = {http://portal.acm.org/citation.cfm?id=302405.302672},
1789  keywords = {CTL , patterns , Specification},
1790  url = {http://patterns.projects.cis.ksu.edu/collaborations/papers.shtml}
1791}
1792
1793@INPROCEEDINGS{6128043,
1794  author = {Yuzhang Feng and Veeramani, A. and Kanagasabai, R. and Seungmin Rho},
1795  title = {Automatic Service Composition via Model Checking},
1796  booktitle = {Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific},
1797  year = {2011},
1798  pages = {477 -482},
1799  month = {dec.},
1800  abstract = {Web service composition is the process of constructing a set of Web
1801        services which, when invoked with some user input in a particular
1802        order, can produce the output to the user's requirements. This paper
1803        proposes a novel model checking based approach for automated service
1804        composition. Modeling services as a set of interleaved processes
1805        in a class of process algebra, we formulate service composition as
1806        model checking asserted on a specific type of property on the model.
1807        We show that, under this formulation, correct composition workflows
1808        can be constructed from the counter-examples provided by model checking.
1809        With a case study on online hotel booking services, we demonstrate
1810        that the proposed approach can support directed a cyclic composition
1811        graphs and the generated composition graphs are automatically verified.},
1812  doi = {10.1109/APSCC.2011.54},
1813  file = {:/users/outil/verif/biblio/Composition/AutomaticServiceCompositionViaModelChecking2011.pdf:PDF},
1814  keywords = {Web service composition;automated service composition;directed acyclic
1815        composition graph;interleaved process;model checking;online hotel
1816        booking services;process algebra;user requirements;Web services;directed
1817        graphs;formal verification;hotel industry;process algebra;},
1818  owner = {cecile},
1819  timestamp = {2012.03.07}
1820}
1821
1822@ARTICLE{DBLP:journals/tcad/FeySBD08,
1823  author = {G{\"o}rschwin Fey and Stefan Staber and Roderick Bloem and Rolf Drechsler},
1824  title = {Automatic Fault Localization for Property Checking},
1825  journal = {IEEE Trans. on CAD of Integrated Circuits and Systems},
1826  year = {2008},
1827  volume = {27},
1828  pages = {1138-1149},
1829  number = {6},
1830  bibsource = {DBLP, http://dblp.uni-trier.de},
1831  ee = {http://dx.doi.org/10.1109/TCAD.2008.923234}
1832}
1833
1834@ARTICLE{fitting91bilattices,
1835  author = {M.~Fitting},
1836  title = {{Bilattices and the Semantics of Logic Programming.}},
1837  journal = {Journal of Logic Programming},
1838  year = {1991},
1839  volume = {11},
1840  pages = {91-116},
1841  number = {1{\&}2},
1842  bibsource = {DBLP, http://dblp.uni-trier.de},
1843  file = {BilSemLP.pdf:/dsk/l1/misc/doc/logique/BilSemLP.pdf:PDF},
1844  keywords = {4-valued, logic, 3-valued},
1845  owner = {cecile},
1846  timestamp = {2006.04.05}
1847}
1848
1849@INPROCEEDINGS{godefroid03expressiveness,
1850  author = {Patrice Godefroid and Radha Jagadeesan},
1851  title = {On the Expressiveness of 3-Valued Models},
1852  booktitle = {VMCAI 2003: Proceedings of the 4th International Conference on Verification,
1853        Model Checking, and Abstract Interpretation},
1854  year = {2003},
1855  pages = {206--222},
1856  address = {London, UK},
1857  publisher = {Springer-Verlag},
1858  file = {vmcai2003.ps:/dsk/l1/misc/doc/logique/vmcai2003.ps:PDF},
1859  isbn = {3-540-00348-7},
1860  keywords = {3-valued, logic, model checking, Kripke structure}
1861}
1862
1863@INPROCEEDINGS{goelL00formal,
1864  author = {A.~Goel and W.~R.~Lee},
1865  title = {{{F}ormal {V}erification of an {IBM} {C}ore{C}onnect {P}rocessor
1866        {L}ocal {B}us {A}rbiter {C}ore}},
1867  booktitle = {DAC'00: Proceedings of the 37th Conference on Design Automation},
1868  year = {2000},
1869  editor = {ACM},
1870  pages = {196-200},
1871  address = {Los Angeles, CA, USA},
1872  bibsource = {DBLP, http://dblp.uni-trier.de},
1873  ee = {http://doi.acm.org/10.1145/337292.337384},
1874  file = {p196-goel.pdf:/dsk/l1/misc/doc/verif_archi/rulebase/p196-goel.pdf:PDF},
1875  keywords = {CTL, model checking, Rulebase},
1876  owner = {cecile},
1877  timestamp = {2006.06.29}
1878}
1879
1880@INPROCEEDINGS{GL91,
1881  author = {O.~Grumberg and D.E.~Long},
1882  title = {Model {C}hecking and {M}odular {V}erification},
1883  booktitle = {International Conference on Concurrency Theory},
1884  year = {1991},
1885  volume = {527},
1886  series = {Lecture Notes in Computer Science},
1887  pages = {250--263},
1888  publisher = {Springer Verlag},
1889  file = {p843-grumberg.pdf:/dsk/l1/misc/doc/modular/model_checking/p843-grumberg.pdf:PDF},
1890  keywords = {simulation,CTL, modular}
1891}
1892
1893@ARTICLE{Gupta92syrvey,
1894  author = {A.~Gupta},
1895  title = {{Formal Hardware Verification Methods: A Survey.}},
1896  journal = {Formal Methods in System Design},
1897  year = {1992},
1898  volume = {1},
1899  pages = {151-238},
1900  number = {2/3},
1901  bibsource = {DBLP, http://dblp.uni-trier.de},
1902  keywords = {survey, hardware, formal verification}
1903}
1904
1905@INPROCEEDINGS{henzinger99dsp,
1906  author = {T.~A.~Henzinger and X.~Liu and S.~Qadeer and S.~K.~Rajamani},
1907  title = {Formal {S}pecification and {V}erification of a {D}ataflow {P}rocessor
1908        {A}rray.},
1909  booktitle = {I{CCAD}'99: {P}roceedings of the 1999 {IEEE}/{ACM} {I}nternational
1910        {C}onference on {C}omputer-{A}ided {D}esign},
1911  year = {1999},
1912  editor = {Jacob K. White, Ellen Sentovich},
1913  pages = {494-499},
1914  address = {San Jose, USA},
1915  bibsource = {DBLP, http://dblp.uni-trier.de},
1916  ee = {http://portal.acm.org/citation.cfm?id=339492.340066},
1917  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},
1918  keywords = {abstraction, assume-guarantee, ATL, modular, archi, MOCHA}
1919}
1920
1921@INPROCEEDINGS{henzinger00decomposing,
1922  author = {Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani},
1923  title = {Decomposing refinement proofs using assume-guarantee reasoning},
1924  booktitle = {ICCAD '00: Proceedings of the 2000 IEEE/ACM international conference
1925        on Computer-aided design},
1926  year = {2000},
1927  pages = {245--253},
1928  address = {San Jose, California},
1929  publisher = {IEEE Press},
1930  file = {decomposing00henzinger.pdf:/dsk/l1/misc/doc/modular/assume/decomposing00henzinger.pdf:PDF},
1931  isbn = {0-7803-6448-1}
1932}
1933
1934@INPROCEEDINGS{C:HJMS03,
1935  author = {Henzinger, T.A. and Jhala, R. and Majumdar, R. and Sutre, G.},
1936  title = {Software {V}erification with {BLAST}},
1937  booktitle = {SPIN'2003: Proceedings of the 10th International SPIN Workshop},
1938  year = {2003},
1939  volume = {2648},
1940  series = {Lecture Notes in Computer Science},
1941  pages = {235--239},
1942  address = {USA},
1943  publisher = {Springer},
1944  note = {Tool paper},
1945  keywords = {software, model-checking},
1946  url = {http://www.labri.fr/publications/mvtsi/2003/HJMS03}
1947}
1948
1949@INPROCEEDINGS{henzinger98you,
1950  author = {T.A.~Henzinger and S.~Qadeer and S.K.~Rajamani},
1951  title = {{Y}ou {A}ssume, {W}e {G}uarantee: {M}ethodology and {C}ase {S}tudies},
1952  booktitle = {C{AV}'98: {P}roceedings of the 10th {I}nternational {C}onference
1953        on {C}omputer {A}ided {V}erification},
1954  year = {1998},
1955  editor = {Alan J. Hu, Moshe Y. Vardi},
1956  volume = {1427},
1957  series = {Lecture Notes in Computer Science},
1958  pages = {440--451},
1959  address = {Vancouver, Canada},
1960  publisher = {Springer-Verlag},
1961  file = {henzinger98you.ps.gz:/dsk/l1/misc/doc/modular/assume/henzinger98you.ps.gz:PDF}
1962}
1963
1964@ARTICLE{henzinger02anassume,
1965  author = {T.A.~Henzinger and S.~Qadeer and S.K.~Rajamani and S.~Tasiran},
1966  title = {An {A}ssume-{G}uarantee {R}ule for {C}hecking {S}imulation},
1967  journal = {ACM Transactions on Programming Languages Systems},
1968  year = {2002},
1969  volume = {24},
1970  pages = {51--64},
1971  number = {1},
1972  address = {New York, NY, USA},
1973  doi = {http://doi.acm.org/10.1145/509705.509707},
1974  file = {henzinger98assumeguarantee.ps:/dsk/l1/misc/doc/modular/assume/henzinger98assumeguarantee.ps:PDF},
1975  issn = {0164-0925},
1976  publisher = {ACM Press}
1977}
1978
1979@ARTICLE{Holzmann97e,
1980  author = {G.J.~Holzmann},
1981  title = {{The Model Checker Spin}},
1982  journal = {IEEE Transactions on Software Engineering},
1983  year = {1997},
1984  volume = {23},
1985  pages = {279--295},
1986  number = {5},
1987  month = {May},
1988  note = {Special issue on Formal Methods in Software Practice}
1989}
1990
1991@INPROCEEDINGS{hosabettu98decomposing,
1992  author = {R.~Hosabettu and M.~Srivas and G.~Gopalakrishnan},
1993  title = {Decomposing the {P}roof of {C}orrectness of {P}ipelined {M}icroprocessors},
1994  booktitle = {Computer-Aided Verification, {CAV'98}},
1995  year = {1998},
1996  editor = {Alan J. Hu and Moshe Y. Vardi},
1997  volume = {1427},
1998  pages = {122--134},
1999  address = {Vancouver, Canada},
2000  publisher = {Springer-Verlag},
2001  url = {citeseer.ist.psu.edu/208243.html}
2002}
2003
2004@ARTICLE{huggins98spec,
2005  author = {J.K.~Huggins and D.~Van Campenhout},
2006  title = {Specification and {V}erification of {P}ipelining in the {ARM2 RISC}
2007        {M}icroprocessor},
2008  journal = {ACM Transactions on Design Automation of Electronic Systems},
2009  year = {1998},
2010  volume = {3},
2011  pages = {563--580},
2012  number = {4},
2013  address = {New York, NY, USA},
2014  doi = {http://doi.acm.org/10.1145/296333.296345},
2015  issn = {1084-4309},
2016  publisher = {ACM Press}
2017}
2018
2019@ARTICLE{HWA99,
2020  author = {H.~Hulgaard and P.~F.~Williams and H.~R.~Andersen},
2021  title = {Equivalence Checking of Combinational Circuits using Boolean Expression
2022        Diagrams},
2023  journal = {{IEEE} Transactions of Computer-Aided Design},
2024  year = {1999},
2025  volume = {18},
2026  pages = {903-917},
2027  number = {7},
2028  month = {July}
2029}
2030
2031@ARTICLE{DBLP:journals/tcad/JainKSC08,
2032  author = {H.~Jain and D.~Kroening and N.~Sharygina and E.M.~Clarke},
2033  title = {Word-Level Predicate-Abstraction and Refinement Techniques for Verifying
2034        RTL Verilog},
2035  journal = {IEEE Transaction on CAD of Integrated Circuits and Systems},
2036  year = {2008},
2037  volume = {27},
2038  pages = {366-379},
2039  number = {2},
2040  bibsource = {DBLP, http://dblp.uni-trier.de},
2041  ee = {http://dx.doi.org/10.1109/TCAD.2007.907270},
2042  file = {:Cegar/WLPredicateAbstractionRefinment08.pdf:PDF},
2043  keywords = {Cegar, predicate abstraction, SAT}
2044}
2045
2046@INPROCEEDINGS{kroening07vcegar,
2047  author = {H.~Jain and D.~Kroening and N.~Sharygina and E.~Clarke},
2048  title = {{{VCEGAR}: Verilog CounterExample Guided Abstraction Refinement}},
2049  booktitle = {T{ACAS}'07: {P}roceedings of the 13th {I}nternational {C}onference
2050        on {T}ools and {A}lgorithms for the {C}onstruction and {A}nalysis
2051        of {S}ystems},
2052  year = {2007},
2053  note = {Accepted paper},
2054  owner = {cecile},
2055  timestamp = {2007.02.07}
2056}
2057
2058@INPROCEEDINGS{JainNFS97survey,
2059  author = {J.~Jain and A.~Narayan and M.~Fujita and A.L.~Sangiovanni-Vincentelli},
2060  title = {A Survey of Techniques for Formal Verification of Combinational Circuits.},
2061  booktitle = {ICCD},
2062  year = {1997},
2063  pages = {445-454},
2064  bibsource = {DBLP, http://dblp.uni-trier.de},
2065  keywords = {survey, hadware, formal veriication}
2066}
2067
2068@ARTICLE{kalushy93knowledge,
2069  author = {Yuri Kaluzhny and Alexei Yu. Muravitsky},
2070  title = {A knowledge representation based on the Belnap's four-valued logic},
2071  journal = {Journal of Applied Non-Classical Logics},
2072  year = {1993},
2073  volume = {3},
2074  pages = {189-203},
2075  number = {2},
2076  bibsource = {DBLP, http://dblp.uni-trier.de},
2077  file = {kaluzhny93knowledge.pdf:/dsk/l1/misc/doc/logique/kaluzhny93knowledge.pdf:PDF},
2078  keywords = {CTL , abstraction , 3-valued , refinment loop},
2079  owner = {cecile},
2080  timestamp = {2006.04.03}
2081}
2082
2083@INPROCEEDINGS{park03satunbounded,
2084  author = {H.-J.~Kang and I.-C.~Park},
2085  title = {SAT-based Unbounded Symbolic Model Checking},
2086  booktitle = {DAC'03: Proceedings of the 40th conference on Design automation},
2087  year = {2003},
2088  pages = {840--843},
2089  address = {New York,USA},
2090  publisher = {ACM},
2091  doi = {http://doi.acm.org/10.1145/775832.776043},
2092  file = {:BMC/kang03satunbounded.pdf:PDF;:BMC/Park05satUnbound.pdf:PDF},
2093  isbn = {1-58113-688-9},
2094  keywords = {SAT, all-sat},
2095  location = {Anaheim, CA, USA}
2096}
2097
2098@ARTICLE{Kern99survey,
2099  author = {C.~Kern and M.R.~Greenstreet},
2100  title = {Formal {V}erification in {H}ardware {D}esign: a {S}urvey},
2101  journal = {ACM Transactions on Design Automation of Electronic Systems},
2102  year = {1999},
2103  volume = {4},
2104  pages = {123--193},
2105  number = {2},
2106  address = {New York, NY, USA},
2107  doi = {http://doi.acm.org/10.1145/307988.307989},
2108  issn = {1084-4309},
2109  keywords = {survey, hadware, formal veriication},
2110  publisher = {ACM Press}
2111}
2112
2113@BOOK{kleene52introduction,
2114  title = {Introduction to Metamathematics},
2115  publisher = {North-Holland},
2116  year = {1952},
2117  author = {Kleene, S.},
2118  series = {Bibliotheca mathematica},
2119  owner = {cecile},
2120  timestamp = {2006.04.27}
2121}
2122
2123@INPROCEEDINGS{KLM93,
2124  author = {T. Kolks and B. Lin and H. De Man},
2125  title = {Sizing and Verification of Communication Buffers for Communicating
2126        Processes},
2127  booktitle = {Proc. of IEEE International Conference on Computer-Aided Design},
2128  year = {1993},
2129  volume = {1825},
2130  pages = {660--664},
2131  address = {Santa Clara, USA}
2132}
2133
2134@INPROCEEDINGS{kroening01automated,
2135  author = {D.~Kroening and W.J.~Paul},
2136  title = {Automated {P}ipeline {D}esign},
2137  booktitle = {DAC '01: Proceedings of the 38th conference on Design Automation},
2138  year = {2001},
2139  pages = {810--815},
2140  publisher = {ACM Press},
2141  doi = {http://doi.acm.org/10.1145/378239.379071},
2142  isbn = {1-58113-297-2},
2143  location = {Las Vegas, Nevada, United States}
2144}
2145
2146@BOOK{kropf99introduction,
2147  title = {Introduction to Formal Hardware Verification},
2148  publisher = {Springer Verlag},
2149  year = {1999},
2150  author = {T.~Kropf},
2151  address = {Secaucus, NJ, USA},
2152  isbn = {3540654453},
2153  keywords = {survey, hardware},
2154  owner = {cecile},
2155  timestamp = {2006.11.07}
2156}
2157
2158@ARTICLE{KupfermanG96branching,
2159  author = {O.~Kupferman and O.~Grumberg},
2160  title = {Branching-Time Temporal Logic and Tree Automata.},
2161  journal = {Information and Computation},
2162  year = {1996},
2163  volume = {125},
2164  pages = {62-69},
2165  number = {1},
2166  bibsource = {DBLP, http://dblp.uni-trier.de},
2167  file = {branchingand automata.ps:/dsk/l1/misc/doc/ctl_auto/branchingand automata.ps:PDF},
2168  keywords = {CTL, tree automata ,model checking, automata approach}
2169}
2170
2171@ARTICLE{KupfermanVW00automata,
2172  author = {O.~Kupferman and M.Y.~Vardi and P.~Wolper},
2173  title = {An {A}utomata-{T}heoretic {A}pproach to {B}ranching-{T}ime {M}odel
2174        {C}hecking.},
2175  journal = {Journal of the ACM},
2176  year = {2000},
2177  volume = {47},
2178  pages = {312-360},
2179  number = {2},
2180  bibsource = {DBLP, http://dblp.uni-trier.de},
2181  ee = {http://doi.acm.org/10.1145/333979.333987},
2182  file = {an-automata-theoretic-approach.pdf:/dsk/l1/misc/doc/automate/an-automata-theoretic-approach.pdf:PDF},
2183  keywords = {tree automata, CTL, automata approach},
2184  owner = {cecile},
2185  timestamp = {2006.06.27}
2186}
2187
2188@INPROCEEDINGS{lamp83,
2189  author = {L.~Lamport},
2190  title = {Information Processing},
2191  booktitle = {What good is in temporal logic},
2192  year = {1983},
2193  pages = {657--668},
2194  publisher = {Elsevier}
2195}
2196
2197@BOOK{Lano,
2198  title = {The {B} {L}anguage and {M}ethod, {A} {G}uide to {P}ractical {F}ormal
2199        {D}evelopment},
2200  publisher = {Springer-Verlag},
2201  year = {1996},
2202  author = {K.~Lano},
2203  series = {FACIT},
2204  address = {UK},
2205  keywords = {b method}
2206}
2207
2208@INPROCEEDINGS{693769,
2209  author = {K.G~Larsen and B.~Steffen and C.~Weise},
2210  title = {A Constraint Oriented Proof Methodology Based on Modal Transition
2211        Systems},
2212  booktitle = {TACAS '95: Proceedings of the First International Workshop on Tools
2213        and Algorithms for Construction and Analysis of Systems},
2214  year = {1995},
2215  pages = {17--40},
2216  address = {London, UK},
2217  publisher = {Springer-Verlag},
2218  isbn = {3-540-60630-0}
2219}
2220
2221@ARTICLE{LiWS05PureSat,
2222  author = {B.~Li and C.~Wang and F.~Somenzi},
2223  title = {Abstraction Refinement in Symbolic Model Checking using Satisfiability
2224        as the Only Decision Procedure},
2225  journal = {STTT},
2226  year = {2005},
2227  volume = {7},
2228  pages = {143-155},
2229  number = {2},
2230  bibsource = {DBLP, http://dblp.uni-trier.de},
2231  ee = {http://dx.doi.org/10.1007/s10009-004-0169-2},
2232  file = {:Cegar/Li04PureSatSTTT.pdf:PDF},
2233  keywords = {CEGAR, SAT}
2234}
2235
2236@INCOLLECTION{springerlink:10.1007/978-3-540-68073-4_4,
2237  author = {Li, Juncao and Sun, Xiuli and Xie, Fei and Song, Xiaoyu},
2238  title = {Component-Based Abstraction and Refinement},
2239  booktitle = {High Confidence Software Reuse in Large Systems},
2240  publisher = {Springer Berlin / Heidelberg},
2241  year = {2008},
2242  editor = {Mei, Hong},
2243  volume = {5030},
2244  series = {Lecture Notes in Computer Science},
2245  pages = {39-51},
2246  note = {10.1007/978-3},
2247  affiliation = {Portland State University Dept. of Computer Science Portland OR 97207},
2248  file = {:/users/outil/verif/biblio/Composition/Compponent-Based AbstractionRefinement2008.pdf:PDF},
2249  isbn = {978-3-540-68062-8},
2250  keyword = {Computer Science},
2251  keywords = {Composition, Abstraction, Refinement, verified component, Hardware/software
2252        coverification},
2253  url = {http://dx.doi.org/10.1007/978-3-540-68073-4_4}
2254}
2255
2256@INPROCEEDINGS{lin91implicit,
2257  author = {B.~Lin and A.R.~Newton},
2258  title = {Implicit Manipulation of Equivalence Classes Using Binary Decision
2259        Diagrams},
2260  booktitle = {ICCD '91: Proceedings of the 1991 IEEE International Conference on
2261        Computer Design on VLSI in Computer \& Processors},
2262  year = {1991},
2263  pages = {81--85},
2264  address = {Washington, DC, USA},
2265  publisher = {IEEE Computer Society},
2266  isbn = {0-8186-2270-9}
2267}
2268
2269@ARTICLE{Loiseaux,
2270  author = {C.~Loiseaux and S.~Graf and J.~Sifakis and A.~Bouajjani and S.~Bensalem},
2271  title = {Property {P}reserving {A}bstractions for the {V}erification of {C}oncurrent
2272        {S}ystems},
2273  journal = {Formal Methods in System Design},
2274  year = {1995},
2275  volume = {6},
2276  pages = {11--44},
2277  number = {1},
2278  address = {Hingham, MA, USA},
2279  publisher = {Kluwer Academic Publisher}
2280}
2281
2282@INCOLLECTION{springerlink:10.1007/978-3-642-16901-4_15,
2283  author = {Lomuscio, Alessio and Strulo, Ben and Walker, Nigel and Wu, Peng},
2284  title = {Assume-Guarantee Reasoning with Local Specifications},
2285  booktitle = {Formal Methods and Software Engineering},
2286  publisher = {Springer Berlin / Heidelberg},
2287  year = {2010},
2288  editor = {Dong, Jin and Zhu, Huibiao},
2289  volume = {6447},
2290  series = {Lecture Notes in Computer Science},
2291  pages = {204-219},
2292  note = {10.1007/978-3-642-16901-4_15},
2293  abstract = {We investigate assume-guarantee reasoning for global specifications
2294        consisting of conjunctions of local specifications. We present a
2295        sound and complete assume-guarantee rule that permits reasoning about
2296        individual modules for local specifications and draws conclusions
2297        on global specifications. We illustrate our approach with an example
2298        from the field of network congestion control, where different agents
2299        are responsible for controlling packet flow across a shared infrastructure.
2300        In this context, we derive an assume-guarantee rule for system stability,
2301        and show that this rule is valuable to reason about any number of
2302        agents, any initial flow configuration, and any topology of bounded
2303        degree.},
2304  affiliation = {Department of Computing, Imperial College London, UK},
2305  file = {:/users/outil/verif/biblio/Composition/AGRwithLocalSpecification2010.pdf:PDF},
2306  isbn = {978-3-642-16900-7},
2307  keyword = {Computer Science},
2308  keywords = {Compositional reasoning, composition},
2309  owner = {cecile},
2310  timestamp = {2012.03.07},
2311  url = {http://dx.doi.org/10.1007/978-3-642-16901-4_15}
2312}
2313
2314@PHDTHESIS{long93thesis,
2315  author = {D.~E.~Long},
2316  title = {Model {C}hecking, {A}bstraction, and {C}ompositional {V}erification},
2317  school = {Carnegie Mellon University},
2318  year = {1993},
2319  file = {long93model.ps.gz:/dsk/l1/misc/doc/modular/model_checking/long93model.ps.gz:PDF},
2320  keywords = {abstraction, CTL, modular, simulation, model checking},
2321  owner = {cecile},
2322  timestamp = {2006.03.08}
2323}
2324
2325@INPROCEEDINGS{santo,
2326  author = {S.~Malik and A.R.~Wang and R.K~Brayton and A.~Sangiovanni-Vincentelli},
2327  title = {Logic Verification using Binary Decision Diagrams in Logic Synthesis
2328        Environment},
2329  booktitle = {Proceedings of the IEEE International Conference on Computer Aided
2330        Design, ICCAD'88},
2331  year = {1988},
2332  pages = {6--9},
2333  month = {November},
2334  note = {Santa Clara CA, USA},
2335  abstract = { This paper proposes two heuristics for variable ordering based on
2336        the topology of the circuit under study. \begin{enumerate} \item
2337        One defines the level of a variable or a gate as follows: $level(root)=0$
2338        and $level(f)=max(level(g))+1$, where the $g$'s are the fathers of
2339        $f$. The first heuristics consists in indexing the variables according
2340        to the decreasing order of their levels. The justification is that
2341        the influence of variables high in the circuit must be computed as
2342        soon as possible. \item Same as the previous heuristics but respecting
2343        modules. Modules are treated in the decreasing order of their depths.
2344        The depth of a formula being the maximum depth of its variables.
2345        \end{enumerate} Experimental results are reported, showing that the
2346        second heuristics is very good (on the ICSAS'85 benchmark). Lu },
2347  keywords = {Variable ordering heuristics, Combinatorial Circuits}
2348}
2349
2350@INPROCEEDINGS{manolios00correctness,
2351  author = {P.~Manolios},
2352  title = {Correctness of Pipelined Machines},
2353  booktitle = {FMCAD '00: Proceedings of the Third International Conference on Formal
2354        Methods in Computer-Aided Design},
2355  year = {2000},
2356  pages = {161--178},
2357  publisher = {Springer-Verlag},
2358  url = {citeseer.ist.psu.edu/426677.html}
2359}
2360
2361@INPROCEEDINGS{manolios04web,
2362  author = {P.~Manolios and S.K.~Srinivasan},
2363  title = {Automatic {V}erification of {S}afety and {L}iveness for {XS}cale-{L}ike
2364        {P}rocessor {M}odels {U}sing {WEB} Refinements},
2365  booktitle = {DATE '04: Proceedings of the conference on Design, Automation and
2366        Test in Europe},
2367  year = {2004},
2368  pages = {168-174},
2369  address = {Washington, DC, USA},
2370  publisher = {IEEE Computer Society},
2371  isbn = {0-7695-2085-5-1}
2372}
2373
2374@INPROCEEDINGS{Mariano2002formalization,
2375  author = {G.~Mariano and J-L.~Boulanger and A. Aljer},
2376  title = {Formalization of {D}igital {C}ircuits {U}sing the {B} {M}ethod},
2377  booktitle = {Comp{R}ail {VIII}: 8th {I}nternational {C}onference on {C}omputer
2378        {A}ided {D}esign, {M}anufacture and {O}peration in the {R}ailway
2379        and other {A}dvanced {M}ass {T}ransit {S}ystems},
2380  year = {2002},
2381  address = {Lemnos, Greece},
2382  month = {12 - 14 } # jun,
2383  keywords = {B method, formal development, software verification, safety-critical
2384        applications, VHDL, BHDL, Hardware},
2385  url = {http://www.wessex.ac.uk/conferences/2002/cr02/}
2386}
2387
2388@INPROCEEDINGS{Silva00Sat,
2389  author = {Marques-Silva, Jo\, {a}o P. and Sakallah, Karem A.},
2390  title = {Boolean satisfiability in electronic design automation},
2391  booktitle = {DAC '00: Proceedings of the 37th Annual Design Automation Conference},
2392  year = {2000},
2393  pages = {675--680},
2394  address = {New York, NY, USA},
2395  publisher = {ACM},
2396  doi = {http://doi.acm.org/10.1145/337292.337611},
2397  file = {:SAT/p675-marques-silva.pdf:PDF},
2398  isbn = {1-58113-187-9},
2399  keywords = {SAT, circuit},
2400  location = {Los Angeles, California, United States},
2401  owner = {cecile},
2402  timestamp = {2009.11.30}
2403}
2404
2405@ARTICLE{mcmillan00methodology,
2406  author = {K.L. McMillan},
2407  title = {A {M}ethodology for {H}ardware {V}erification {U}sing {C}ompositional
2408        {M}odel {C}hecking},
2409  journal = {Science of Computer Programming},
2410  year = {2000},
2411  volume = {37},
2412  pages = {279--309},
2413  number = {1--3},
2414  file = {mcmillan99methodology.pdf:/dsk/l1/misc/doc/modular/assume/mcmillan99methodology.pdf:PDF},
2415  keywords = {CTL, LTL, model checking, modular, composition, assume-guarantee},
2416  url = {citeseer.ist.psu.edu/mcmillan99methodology.html}
2417}
2418
2419@BOOK{mcmillanSMV,
2420  title = {Symbolic Model Checking},
2421  publisher = {Kluwer Academics Publishers},
2422  year = {1993},
2423  author = {K.L.~McMillan}
2424}
2425
2426@PHDTHESIS{memmi:thesis,
2427  author = {G.~Memmi},
2428  title = {M\'ethodes d'analyse des r\'eseaux de Petri, r\'eseaux \`a files
2429        et application aux syst\`emes temps-r\'eel},
2430  school = {Universit\'e Paris-6},
2431  year = {1983}
2432}
2433
2434@BOOK{Mil89,
2435  title = {Communication and {C}oncurrency},
2436  publisher = {Prentice Hall},
2437  year = {1989},
2438  author = {R.~Milner},
2439  series = {International series in computer science},
2440  address = {Upper Saddle River, USA},
2441  isbn = {0-13-115007-3}
2442}
2443
2444@INPROCEEDINGS{DBLP:conf/ijcai/Milner71,
2445  author = {R.~Milner},
2446  title = {{An Algebraic Definition of Simulation Between
2447       
2448         Programs.}},
2449  booktitle = {IJCAI'71: Proceedings of the 2nd International Joint Conference on
2450        Artificial Intelligence},
2451  year = {1971},
2452  pages = {481-489},
2453  adress = {London, UK},
2454  bibsource = {DBLP, http://dblp.uni-trier.de},
2455  editors = {D. C. Cooper},
2456  keywords = {simulation, bisimulation}
2457}
2458
2459@INPROCEEDINGS{minato,
2460  author = {S.~Minato and N.~Ishiura and S.~Yajima},
2461  title = {Shared Binary Decision Diagrams with Attributed Edges for Efficient
2462        Boolean Function Manipulation},
2463  booktitle = {Proceedings of the 27th ACM/IEEE Design Automation Conference, DAC'90},
2464  year = {1990},
2465  editor = {L.J.M Claesen},
2466  pages = {52--57},
2467  month = {June},
2468  abstract = { This paper is the first one in which management of BDD nodes via
2469        a hash table is proposed (and thus the reduction operation is suppressed).
2470        Then, various labelling of edges are discussed: first, the flag $+/-$
2471        already proposed by Billon and Madre \cite{Bil87,MB88}. Second, another
2472        flag so-called input inverter, is proposed. It transforms $ite(x,F,G)$
2473        into $ite(\neg x,F,G)=ite(x,G,F)$. Canonicity is maintained by keeping
2474        only nodes such that $F<G$ (for say the memory order). Third, labelling
2475        edges with shifts between variable indices is proposed. Fourth, it
2476        is proposed to encode small BDD's (with only two variables) by means
2477        of a single word. Then, a variable ordering heuristics is proposed.
2478        It consists in propagating a flow from the outputs to the inputs
2479        of the circuits and labelling inputs by the order of their flow values.
2480        The flow at each input is $1.0$, the flow at a gate is the sum of
2481        its in-flow. Its is shared equally by its parents. Then, A way to
2482        manage {\em don't care} parts of circuits is proposed. It consists
2483        in using a second variable $\neg x_1 \wedge \neg x_2 \rightarrow
2484        \neg x$, $x_1 \wedge x_2 \rightarrow x$, otherwise {\em don't care}.
2485        Finally, experimental results are reported. },
2486  keywords = {BDD encoding, Heuristics for variable ordering}
2487}
2488
2489@INPROCEEDINGS{MC99,
2490  author = {A.S. Miner and G. Ciardo},
2491  title = {Efficient Reachability Set Generation and Storage Using Decision
2492        Diagrams},
2493  booktitle = {Proc. of ICATPN'99},
2494  year = {1999},
2495  volume = {1639},
2496  series = {Lecture Notes in Computer Science},
2497  pages = {6--25},
2498  publisher = {Springer Verlag}
2499}
2500
2501@ARTICLE{Miskov-ZivanovM06,
2502  author = {N.~Miskov-Zivanov and D.~Marculescu},
2503  title = {Circuit Reliability Analysis Using Symbolic Techniques},
2504  journal = {IEEE Transaction on CAD of Integrated Circuits and Systems},
2505  year = {2006},
2506  volume = {25},
2507  pages = {2638-2649},
2508  number = {12},
2509  bibsource = {DBLP, http://dblp.uni-trier.de},
2510  ee = {http://dx.doi.org/10.1109/TCAD.2006.882592}
2511}
2512
2513@ARTICLE{mooremachine,
2514  author = {E.F.~Moore},
2515  title = {Gedanken-experiments on Sequential Machines},
2516  journal = {Automata Studies, Annals of Mathematical Studies},
2517  year = {1956},
2518  volume = {34},
2519  pages = {129 – 153},
2520  eid = {Princeton University Press},
2521  owner = {cecile},
2522  timestamp = {2006.09.04}
2523}
2524
2525@ARTICLE{DBLP:journals/tc/MoundanosAH98,
2526  author = {D.~Moundanos and J.A.~Abraham and Y.V.~Hoskote},
2527  title = {Abstraction Techniques for Validation Coverage Analysis and Test
2528        Generation},
2529  journal = {IEEE Trans. Computers},
2530  year = {1998},
2531  volume = {47},
2532  pages = {2-14},
2533  number = {1},
2534  bibsource = {DBLP, http://dblp.uni-trier.de},
2535  keywords = {Abstraction}
2536}
2537
2538@ARTICLE{moy06lussy,
2539  author = {M.~Moy and F.~Maraninchi and L.~Maillet},
2540  title = {LusSy: An open tool for the analysis of systems-on-a-chip at the
2541        transaction level},
2542  journal = {Design Automation for Embedded Systems},
2543  year = {2006},
2544  volume = {10},
2545  pages = {73--104},
2546  number = {2-3},
2547  doi = {10.1007/s10617-006-9044-6},
2548  owner = {cecile},
2549  timestamp = {2007.01.31}
2550}
2551
2552@ARTICLE{namjoshi97simple,
2553  author = {K.S.~Namjoshi},
2554  title = {A Simple Characterization of Stuttering Bisimulation},
2555  journal = {LNCS, Proceedings of the 17th Conference on Foundations of Software
2556        Technology an Theoretical Computer Science},
2557  year = {1997},
2558  volume = {1346},
2559  pages = {284--296},
2560  url = {citeseer.ist.psu.edu/namjoshi97simple.html}
2561}
2562
2563@INPROCEEDINGS{namjoshiK00syntactic,
2564  author = {K.~S.~Namjoshi and R.~P.~Kurshan},
2565  title = {Syntactic Program Transformations for Automatic Abstraction},
2566  booktitle = {Proceedings of the 12th International Conference on Computer Aided
2567        Verification},
2568  year = {2000},
2569  volume = {1855},
2570  series = {Lecture Notes In Computer Science},
2571  pages = {435--449},
2572  address = {London, UK},
2573  publisher = {Springer-Verlag},
2574  file = {auto_abstra.ps:/dsk/l1/misc/doc/ctl_auto/auto_abstra.ps:PDF},
2575  keywords = {abstraction, model checking},
2576  owner = {cecile},
2577  timestamp = {2006.02.03}
2578}
2579
2580@ARTICLE{nicolaV95,
2581  author = {R.~De~Nicola and F.W.~Vaandrager},
2582  title = {Three Logics for Branching Bisimulation.},
2583  journal = {Journal of the ACM},
2584  year = {1995},
2585  volume = {42},
2586  pages = {458-487},
2587  number = {2},
2588  bibsource = {DBLP, http://dblp.uni-trier.de},
2589  ee = {http://doi.acm.org/10.1145/201019.201032}
2590}
2591
2592@MANUAL{VCI_spec,
2593  title = {{Virtual Component Interface Standard (VCI).}},
2594  author = {{On-Chip Bus Development Working Group}},
2595  organization = {{VSI Alliance}},
2596  year = {2000},
2597  key = VCI,
2598  volume = {version 2}
2599}
2600
2601@MANUAL{PI_proto,
2602  title = {{OMI324: {PI}-{B}us {S}tandard {S}pecification}},
2603  author = {{Open Microprocessors System Initiatives}},
2604  organization = {Siemens},
2605  address = {Munich, Germany},
2606  year = {1994},
2607  file = {Pidoc31.pdf:/dsk/l1/misc/doc/archi/Pidoc31.pdf:PDF}
2608}
2609
2610@TECHREPORT{specamba03,
2611  author = {J.~{Ossima Kh\'eba}},
2612  title = {Sp\'ecification des {W}rappers {AHB}/{VCI}},
2613  institution = {LIP6 dept. ASIM},
2614  year = {2003},
2615  type = {Rapport de {DEA}},
2616  owner = {cecile},
2617  school = {{Universit\'ee} {Pierre} et {Marie} {Curie}},
2618  timestamp = {2006.09.07}
2619}
2620
2621@TECHREPORT{joel02,
2622  author = {J.~{Ossima Kh\'eba}},
2623  title = {Les {W}rappers {PI}/{VCI} et {E}tude de {F}aisabilit\'e des {W}rappers
2624        {AMBA}/{VCI}},
2625  institution = {LIP6 dept. ASIM},
2626  year = {2002},
2627  type = {Rapport de stage},
2628  owner = {cecile},
2629  school = {{Universit\'ee} {Pierre} et {Marie} {Curie}},
2630  timestamp = {2006.09.07}
2631}
2632
2633@INPROCEEDINGS{cade92-pvs,
2634  author = {{S.} Owre and {J.} {M.} Rushby and and {N.} Shankar},
2635  title = {{PVS:} {A} Prototype Verification System},
2636  booktitle = {11th International Conference on Automated Deduction (CADE)},
2637  year = {1992},
2638  editor = {Deepak Kapur},
2639  volume = {607},
2640  series = {Lecture Notes in Artificial Intelligence},
2641  pages = {748--752},
2642  address = {Saratoga, {NY}},
2643  month = {jun},
2644  publisher = {Springer-Verlag},
2645  url = {http://www.csl.sri.com/papers/cade92-pvs/}
2646}
2647
2648@INCOLLECTION{springerlink:10.1007/3-540-63166-6_5,
2649  author = {Pardo, Abelardo and Hachtel, Gary},
2650  title = {Automatic abstraction techniques for propositional $\mu$-calculus
2651        model checking},
2652  booktitle = {Computer Aided Verification},
2653  publisher = {Springer Berlin / Heidelberg},
2654  year = {1997},
2655  editor = {Grumberg, Orna},
2656  volume = {1254},
2657  series = {Lecture Notes in Computer Science},
2658  pages = {12-23},
2659  note = {10.1007/3-540-63166-6_5},
2660  abstract = {An abstraction/refinement paradigm for the full propositional $\mu$-calculus
2661        is presented. No distinction is made between universal or existential
2662        fragments. Necessary conditions for conservative verification are
2663        provided, along with a fully automatic symbolic model checking abstraction
2664        algorithm. The algorithm begins with conservative verification of
2665        an initial abstraction. If the conclusion is negative, it derives
2666        a ldquogoal setrdquo of states which require further resolution.
2667        It then successively refines, with respect to this goal set, the
2668        approximations made in the subformulas, until the given formula is
2669        verified or computational resources are exhausted.},
2670  affiliation = {University of Colorado ECEN Campus Box 425 80309 Boulder CO USA ECEN
2671        Campus Box 425 80309 Boulder CO USA},
2672  file = {:/users/outil/verif/biblio/Cegar/CAV97_Automatic_Abstraction_Tech_for_Propositional_uCalc_MC.ps:PostScript},
2673  isbn = {978-3-540-63166-8},
2674  keywords = {Computer Science, Abstraction, model checking, mu-calculus, refinement},
2675  owner = {cecile},
2676  timestamp = {2012.03.07},
2677  url = {http://dx.doi.org/10.1007/3-540-63166-6_5}
2678}
2679
2680@INPROCEEDINGS{Pardo:1998:ICM:277044.277171,
2681  author = {Pardo, Abelardo and Hachtel, Gary D.},
2682  title = {Incremental CTL model checking using BDD subsetting},
2683  booktitle = {Proceedings of the 35th annual Design Automation Conference},
2684  year = {1998},
2685  series = {DAC '98},
2686  pages = {457--462},
2687  address = {New York, NY, USA},
2688  publisher = {ACM},
2689  abstract = {An automatic abstraction/refinement algorithm for symbolic CTL model
2690        checking is presented. Conservative model checking is thus done for
2691        the full CTL language-no restriction is made to the universal or
2692        existen tial fragments. The algorithm begins with conserv ativ everification
2693        of an initial abstraction. If the conclusion is negativ e,it deriv
2694        es a ¿goal set¿ of states which require further resolution. It then
2695        successiv ely refines, with respect to this goal set, the appro ximations
2696        made in the sub-formulas, until the giv en form ula is v erified
2697        or computational resources are exhausted. This method applies uniformly
2698        to the abstractions based in over-appro ximation as well as under-approximations
2699        of the model. Both the refinement and the abstraction procedures
2700        are based in BDD-subsetting. Note that refinement procedures which
2701        are based on error traces, are limited to over-appro ximation on
2702        the universal fragment (or for language con tainment), whereas the
2703        goal set method is applicable to all consisten t appro ximations,
2704        and for all CTL formulas.},
2705  acmid = {277171},
2706  doi = {10.1145/277044.277171},
2707  file = {:/users/outil/verif/biblio/Cegar/DAC98_Incremental CTL Model Checking Using BDD Subsetting.pdf:PDF},
2708  isbn = {0-89791-964-5},
2709  keywords = {CTL, model checking, Abstraction},
2710  location = {San Francisco, California, United States},
2711  numpages = {6},
2712  url = {http://doi.acm.org/10.1145/277044.277171}
2713}
2714
2715@INPROCEEDINGS{pasareanu99assume,
2716  author = {C.S.~Pasareanu and M.B.~Dwyer and M.~Huth},
2717  title = {Assume-{G}uarantee {M}odel {C}hecking of {S}oftware: {A} {C}omparative
2718        {C}ase {S}tudy},
2719  booktitle = {Proceedings of the 5th and 6th International SPIN Workshops on Theoretical
2720        and Practical Aspects of SPIN Model Checking},
2721  year = {1999},
2722  pages = {168--183},
2723  address = {London, UK},
2724  publisher = {Springer-Verlag},
2725  isbn = {3-540-66499-8}
2726}
2727
2728@INPROCEEDINGS{passerone02convertibility,
2729  author = {R.~Passerone and L.~de Alfaro and T.A.~Henzinger and A.L.~Sangiovanni-Vincentelli},
2730  title = {Convertibility {V}erification and {C}onverter {S}ynthesis: {T}wo
2731        {F}aces of {T}he {S}ame {C}oin},
2732  booktitle = {I{CCAD} '02: {P}roceedings of the 2002 {IEEE}/{ACM} {I}nternational
2733        {C}onference on {C}omputer-{A}ided {D}esign},
2734  year = {2002},
2735  pages = {132--139},
2736  address = {New York, USA},
2737  publisher = {ACM Press},
2738  doi = {http://doi.acm.org/10.1145/774572.774592},
2739  file = {samecoin.pdf:/dsk/l1/misc/doc/interface/samecoin.pdf:PDF},
2740  isbn = {0-7803-7607-2},
2741  location = {San Jose, California}
2742}
2743
2744@INPROCEEDINGS{DBLP:conf/dac/PasseroneRS98,
2745  author = {R.~Passerone and J.A.~Rowson and A.L.~Sangiovanni-Vincentelli},
2746  title = {{Automatic Synthesis of Interfaces Between
2747       
2748         Incompatible Protocols.}},
2749  booktitle = {DAC'98: Proceedings of the 35th Conference on Design Automation},
2750  year = {1998},
2751  pages = {8-13},
2752  adress = {San Francico, USA},
2753  bibsource = {DBLP, http://dblp.uni-trier.de},
2754  ee = {http://doi.acm.org/10.1145/277044.277047},
2755  file = {samecoin.pdf:/dsk/l1/misc/doc/interface/samecoin.pdf:PDF},
2756  keywords = {interface, wrapper}
2757}
2758
2759@INPROCEEDINGS{PRCB94,
2760  author = {E. Pastor and O. Roig and J. Cortadella and R.M. Badia},
2761  title = {Petri Net analysis using Boolean manipulation},
2762  booktitle = {Proc. of ICATPN'94},
2763  year = {1994},
2764  volume = {815},
2765  series = {Lecture Notes in Computer Science},
2766  pages = {416--435},
2767  publisher = {Springer Verlag}
2768}
2769
2770@BOOK{hennessypattersonbook,
2771  title = {Computer Organization and Design: The Hardware/Software Interface,
2772        Third Edition (The Morgan Kaufmann Series in Computer Architecture
2773        and Design) (The ... Series in Computer Architecture and Design)},
2774  publisher = {{Morgan Kaufmann}},
2775  year = {2004},
2776  author = {D.A.~Patterson and J.L~Hennessy},
2777  edition = {third},
2778  month = {August},
2779  abstract = {{In addition to thoroughly updating every aspect of the text to reflect
2780        the most current computing technology, the third edition<br><br>*Uses
2781        standard 32-bit MIPS 32 as the primary teaching ISA.<br>*Presents
2782        the assembler-to-HLL translations in both C and Java.<br>*Highlights
2783        the latest developments in architecture in Real Stuff sections:<br><br>+
2784        Intel IA-32<br>+ Power PC 604<br>+ Googles PC cluster<br>+ Pentium
2785        P4<br>+ SPEC CPU2000 benchmark suite for processors<br>+ SPEC Web99
2786        benchmark for web servers<br>+ EEMBC benchmark for embedded systems<br>+
2787        AMD Opteron memory hierarchy<br>+ AMD vs. 1A-64<br><br><br><b>New
2788        support for distinct course goals</b><br><br>Many of the adopters
2789        who have used our book throughout its two editions are refining their
2790        courses with a greater hardware or software focus. We have provided
2791        new material to support these course goals:<br><br><i>New material
2792        to support a Hardware Focus</i><br><br>+Using logic design conventions<br>+Designing
2793        with hardware description languages<br>+Advanced pipelining<br>+Designing
2794        with FPGAs<br>+HDL simulators and tutorials<br>+Xilinx CAD tools<br><br><i>New
2795        material to support a Software Focus</i><br><br>+How compilers Work<br>+How
2796        to optimize compilers<br>+How to implement object oriented languages<br>+MIPS
2797        simulator and tutorial<br>+History sections on programming languages,
2798        compilers, operating systems and databases<br><br><i><b>Whats New
2799        in the Third Edition</b></i><br><br><b>New pedagogical features</b><br><br><i>Understanding
2800        Program Performance</i> <br>-Analyzes key performance issues from
2801        the programmers perspective <br><br><i>Check Yourself Questions</i>
2802        <br>-Helps students assess their understanding of key points of a
2803        section <br><br><i>Computers In the Real World</i> <br>-Illustrates
2804        the diversity of applications of computing technology beyond traditional
2805        desktop and servers<br><br><i>For More Practice</i><br>-Provides
2806        students with additional problems they can tackle<br><br><i>In More
2807        Depth</i> <br>-Presents new information and challenging exercises
2808        for the advanced student<br><br><br><b>New reference features</b><br><br>Highlighted
2809        glossary terms and definitions appear on the book page, as bold-faced
2810        entries in the index, and as a separate and searchable reference
2811        on the CD.<br><br>A complete index of the material in the book and
2812        on the CD appears in the printed index and the CD includes a fully
2813        searchable version of the same index.<br><br>Historical Perspectives
2814        and Further Readings have been updated and expanded to include the
2815        history of software R\&D.<br><br>CD-Library provides materials collected
2816        from the web which directly support the text.<br><br><b>On the CD</b><br><br>CD-Bars:
2817        Full length sections that are introduced in the book and presented
2818        on the CD<br><br>CD-Appendixes: The entire set of appendixes<br><br>CD-Library:
2819        Materials collected from the web which directly support the text<br><br>CD-Exercises:
2820        <i>For More Practice</i> provides exercises and solutions for self-study<br><i>In
2821        More Depth</i> presents new information and challenging exercises
2822        for the advanced or curious student<br> <br>Glossary: Terms that
2823        are defined in the text are collected in this searchable reference<br><br>Further
2824        Reading: References are organized by the chapter they support<br><br>Software:
2825        HDL simulators, MIPS simulators, and FPGA design tools<br><br>Tutorials:
2826        SPIM, Verilog, and VHDL<br><br>Additional Support: Processor Models,
2827        Labs, Homeworks, Index covering the book and CD contents<br><br><b>Instructor
2828        Support</b><br><br>+ Instructor Support is provided in a password-protected
2829        site to adopters who request the password from our sales representative<br>+
2830        Solutions to all the exercises <br>+ Figures from the book in a number
2831        of formats<br>+ Lecture slides prepared by the authors and other
2832        instructors<br>+ Lecture notes<br><br><b>For instructor resources
2833        click on the grey "companion site" button found on the right side
2834        of this page.</B><br>This new edition represents a major revision.
2835        <br>New to this edition:<br><br>* Entire Text has been updated to
2836        reflect new technology<br>* 70% new exercises.<br>* Includes a CD
2837        loaded with software, projects and exercises to support courses using
2838        a number of tools <br>* A new interior design presents defined terms
2839        in the margin for quick reference <br>* A new feature, Understanding
2840        Program Performance focuses on performance from the programmers perspective
2841        <br>* Two sets of exercises and solutions, For More Practice and
2842        In More Depth, are included on the CD <br>* Check Yourself questions
2843        help students check their understanding of major concepts <br>* Computers
2844        In the Real World feature illustrates the diversity of uses for information
2845        technology <br>*More detail below...}},
2846  citeulike-article-id = {808853},
2847  howpublished = {Paperback},
2848  isbn = {1558606041},
2849  keywords = {pipeline,processor},
2850  priority = {2},
2851  url = {http://www.amazon.co.uk/exec/obidos/ASIN/1558606041/citeulike-21}
2852}
2853
2854@PHDTHESIS{peng02thesis,
2855  author = {H.~Peng},
2856  title = {Improving Compositional Verification through Environment Synthesis
2857        and Syntactic Model Reduction},
2858  school = {Dept. of Electrical and Computer Engenering, Concordia University,
2859        Montreal, Quebec, Canada},
2860  year = {2002},
2861  owner = {cecile},
2862  timestamp = {2007.01.09}
2863}
2864
2865@ARTICLE{peng03comparison,
2866  author = {H.~Peng and S.~Tahar and F.~Khendek},
2867  title = {Comparison of {SPIN} and {VIS} for {P}rotocol {V}erification.},
2868  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
2869  year = {2003},
2870  volume = {4},
2871  pages = {234-245},
2872  number = {2},
2873  bibsource = {DBLP, http://dblp.uni-trier.de},
2874  ee = {http://dx.doi.org/10.1007/s100090200073},
2875  publisher = {Springer}
2876}
2877
2878@INPROCEEDINGS{omi95rsp,
2879  author = {V. Pevtschin},
2880  title = {The {O}pen {M}icroprocessor {S}ystems {I}nitiative: {A} {S}trategy
2881        {T}owards {I}ntegrated {S}ystem {D}esign},
2882  booktitle = {R{SP}'95: {P}roceddings of the 6th {IEEE} {I}nternational {W}orkshop
2883        on {R}apid {S}ystem {P}rototyping},
2884  year = {1995},
2885  pages = {2--11},
2886  doi = {http://doi.ieeecomputersociety.org/10.1109/IWRSP.1995.518564},
2887  owner = {cecile},
2888  timestamp = {2007.02.19}
2889}
2890
2891@INPROCEEDINGS{plath99sfi,
2892  author = {M.C.~Plath and M.D.~Ryan},
2893  title = {S{FI}: a {F}eature {I}ntegration {T}ool},
2894  booktitle = {Tool Support for System Specification, Development and Verification},
2895  year = {1999},
2896  editor = {R. Berghammer and Y. Lakhnech},
2897  series = {Advances in Computing Science},
2898  pages = {201--216},
2899  publisher = {Springer},
2900  file = {plath99sfi.ps:/dsk/l1/misc/doc/telecom/plath99sfi.ps:PDF},
2901  keywords = {feature}
2902}
2903
2904@ARTICLE{plath01feature,
2905  author = {M.~Plath and M.~Ryan},
2906  title = {Feature {I}ntegration using a {F}eature {C}onstruct},
2907  journal = {Science of Computer Programming},
2908  year = {2001},
2909  volume = {41},
2910  pages = {53--84},
2911  number = {1},
2912  address = {Amsterdam, The Netherlands},
2913  doi = {http://dx.doi.org/10.1016/S0167-6423(00)00018-6},
2914  issn = {0167-6423},
2915  publisher = {Elsevier North-Holland, Inc.}
2916}
2917
2918@INPROCEEDINGS{plath98feature,
2919  author = {M.C.~Plath and M.D.~Ryan},
2920  title = {A feature construct for Promela},
2921  booktitle = {SPIN'98: Proceedings of the 4th SPIN workshop},
2922  year = {1998},
2923  url = {citeseer.ist.psu.edu/plath98feature.html}
2924}
2925
2926@INPROCEEDINGS{Purandare09Strengthening,
2927  author = {M. Purandare and T. Wahl and D. Kroening},
2928  title = {Strengthening Properties Using on Refinement},
2929  booktitle = {DATE '09: Proceedings of the conference on Design, Automation and
2930        Test in Europe},
2931  year = {2009},
2932  pages = {1692-1697},
2933  file = {:Cegar/Strenghtening Properties Using AR 09.PDF:PDF},
2934  owner = {cecile},
2935  timestamp = {2009.04.30}
2936}
2937
2938@MASTERSTHESIS{fredHDR,
2939  author = {P{\'e}trot, F.},
2940  title = {Int{\'e}gration des syst{\`e}mes mat{\'e}riel/logiciel},
2941  school = {Universit{\'e}e Pierre et Marie Curie},
2942  year = {2003},
2943  type = {Habilitation {\`a} Diriger des Recherches},
2944  owner = {cecile},
2945  timestamp = {2007.02.03}
2946}
2947
2948@BOOK{rasiowa78algebra,
2949  title = {An Algebraic Approach to Non-Classicals Logis},
2950  year = {1978},
2951  editor = {Studies in Logics and the Foundations of Mathematics},
2952  author = {H.~Rasiowa},
2953  address = {Amsterdam},
2954  owner = {cecile},
2955  timestamp = {2006.05.15}
2956}
2957
2958@INPROCEEDINGS{sawada97trace,
2959  author = {J.~Sawada and W.A.~Hunt},
2960  title = {Trace {T}able {B}ased {A}pproach for {P}ipeline {M}icroprocessor
2961        {V}erification},
2962  booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer
2963        Aided Verification},
2964  year = {1997},
2965  pages = {364--375},
2966  address = {London, UK},
2967  publisher = {Springer-Verlag LNCS 1254},
2968  isbn = {3-540-63166-6}
2969}
2970
2971@INPROCEEDINGS{eveking06fdl,
2972  author = {M.~Schickel and V.~Nimbler and M.~Braun and H.~Eveking},
2973  title = {On {C}onsistency and {C}ompletness of {P}roperty-{S}ets~: {Exploiting
2974        the {P}roperty-{B}ased {D}esign {P}rocess}},
2975  booktitle = {FDL'06: Proceeding of Forum on specification and Design Languages},
2976  year = {2006},
2977  keywords = {Property-based design}
2978}
2979
2980@ARTICLE{DBLP:journals/fmsd/SegerB95,
2981  author = {Carl-Johan H. Seger and Randal E. Bryant},
2982  title = {Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories},
2983  journal = {Formal Methods in System Design},
2984  year = {1995},
2985  volume = {6},
2986  pages = {147-189},
2987  number = {2},
2988  bibsource = {DBLP, http://dblp.uni-trier.de}
2989}
2990
2991@ARTICLE{Sharygin2012,
2992  author = {Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich},
2993  title = {An abstraction refinement approach combining precise and approximated
2994        techniques},
2995  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
2996  year = {2012},
2997  volume = {14},
2998  pages = {1-14},
2999  file = {:/users/outil/verif/biblio/Cegar/A_framework_forCVofMVviaAR-ATVA09.pdf:PDF},
3000  keywords = {Predicate abstraction, Precise abstraction, Approximated abstraction,
3001        CEGAR},
3002  publisher = {Springer},
3003  url = {http://dx.doi.org/10.1007/s10009-011-0185-y}
3004}
3005
3006@INPROCEEDINGS{magnier-sherman:factotum,
3007  author = {D.J Sherman and N. Magnier},
3008  title = {Factotum: Automatic and Systematic Sharing Support for Systems Analyzers},
3009  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
3010        (TACAS'98)},
3011  year = {1982},
3012  editor = {Bernhard Steffen},
3013  address = {Lisbon, Portugal},
3014  month = {March-April},
3015  publisher = {Springer-Verlag LNCS 1384}
3016}
3017
3018@INPROCEEDINGS{shoham06precision,
3019  author = {S.~Shoham and O.~Grumberg},
3020  title = {3-Valued Abstraction: More Precision at Less Cost},
3021  booktitle = {LICS '06: proceedings of the 21st Annual IEEE Symposium on Logic
3022        in Computer Science},
3023  year = {2006},
3024  pages = {399--410},
3025  address = {Washington, DC, USA},
3026  publisher = {IEEE Computer Society},
3027  doi = {http://dx.doi.org/10.1109/LICS.2006.5},
3028  keywords = {Abstraction, 3-valued},
3029  owner = {cecile},
3030  timestamp = {2007.01.14}
3031}
3032
3033@ARTICLE{DBLP:journals/tcad/SmithVAV05,
3034  author = {Alexander Smith and Andreas G. Veneris and Moayad Fahim Ali and Anastasios
3035        Viglas},
3036  title = {Fault diagnosis and logic debugging using Boolean satisfiability},
3037  journal = {IEEE Trans. on CAD of Integrated Circuits and Systems},
3038  year = {2005},
3039  volume = {24},
3040  pages = {1606-1621},
3041  number = {10},
3042  bibsource = {DBLP, http://dblp.uni-trier.de},
3043  ee = {http://dx.doi.org/10.1109/TCAD.2005.852031}
3044}
3045
3046@INCOLLECTION{IMM2001-0855,
3047  author = {J. Spars{\o}},
3048  title = {Asynchronous {C}ircuit {D}esign - {A} {T}utorial},
3049  booktitle = {Chapters {1-}8 in {''}Principles of asynchronous circuit design -
3050        A systems Perspective''},
3051  publisher = {Kluwer Academic Publishers},
3052  year = {2001},
3053  pages = {1-152},
3054  address = {London},
3055  month = {dec},
3056  isbn_issn = {0-7923-7613-7},
3057  url = {http://www2.imm.dtu.dk/pubdb/p.php?855}
3058}
3059
3060@MANUAL{AtelierB,
3061  title = {{A}telier {B}, {M}anuel {U}tilisateur},
3062  author = {{{STERIA} Technologie de l'information}},
3063  address = {Aix-en-Provence, France},
3064  year = {1998},
3065  keywords = {theorem prover, b},
3066  series = {version 3.5}
3067}
3068
3069@PHDTHESIS{turk05thesis,
3070  author = {T\"urk, T.},
3071  title = {A Hierarchy for Accellera's Property Specification Language},
3072  school = {University of Kaiserslautern},
3073  year = {2005},
3074  comment = {Je l'ai en papier},
3075  keywords = {automata approach, PSL},
3076  owner = {cecile},
3077  timestamp = {2006.02.13},
3078  url = {http://thomas-tuerk.de/dokumente/Diplomarbeit.pdf}
3079}
3080
3081@MANUAL{vismanual,
3082  title = {VIS User's Manual},
3083  author = {{The VIS Group}},
3084  year = {1996},
3085  file = {vis_user.ps:/dsk/l1/misc/doc/checker/vis_user.ps:PDF},
3086  key = VIS,
3087  keywords = {model checker},
3088  owner = {cecile},
3089  timestamp = {2006.02.09}
3090}
3091
3092@INPROCEEDINGS{Tripakis201,
3093  author = {Tripakis, Stavros and Andrade, Hugo and Ghosal, Arkadeb and Limaye,
3094        Rhishikesh and Ravindran, Kaushik and Wang, Guoqiang and Yang, Guang
3095        and Kormerup, Jacob and Wong, Ian},
3096  title = {Correct and non-defensive glue design using abstract models},
3097  booktitle = {Proceedings of the seventh IEEE/ACM/IFIP international conference
3098        on Hardware/software codesign and system synthesis},
3099  year = {2011},
3100  series = {CODES+ISSS '11},
3101  pages = {59--68},
3102  address = {New York, NY, USA},
3103  publisher = {ACM},
3104  abstract = { Current hardware design practice often relies on integration of components,
3105        some of which may be IP or legacy blocks. While integration eases
3106        design by allowing modularization and component reuse, it is still
3107        done in a mostly ad hoc manner. Designers work with descriptions
3108        of components that are either informal or incomplete (e.g., documents
3109        in English, structural but non-behavioral specifications in IP-XACT)
3110        or too low-level (e.g., HDL code), and have little to no automatic
3111        support for stitching the components together. Providing such support
3112        is the glue design problem.
3113       
3114        This paper addresses this problem using a model-based approach. The
3115        key idea is to use high-level models, such as dataflow graphs, that
3116        enable efficient automated analysis. The analysis can be used to
3117        derive performance properties of the system (e.g., component compatibility,
3118        throughput, etc.), optimize resource usage (e.g., buffer sizes),
3119        and even synthesize low-level code (e.g., control logic). However,
3120        these models are only abstractions of the real system, and often
3121        omit critical information. As a result, the analysis outcomes may
3122        be defensive (e.g., buffers that are too big) or even incorrect (e.g.,
3123        buffers that are too small). The paper examines these situations
3124        and proposes a correct and non-defensive design methodology that
3125        employs the right models to explore accurate performance and resource
3126        trade-offs. },
3127  acmid = {2039382},
3128  doi = {http://doi.acm.org/10.1145/2039370.2039382},
3129  isbn = {978-1-4503-0715-4},
3130  keywords = {abstraction, data flow, glue design, non-defensiveness, composition},
3131  location = {Taipei, Taiwan},
3132  numpages = {10},
3133  owner = {cecile},
3134  timestamp = {2012.03.07},
3135  url = {http://doi.acm.org/10.1145/2039370.2039382}
3136}
3137
3138@MISC{m106archi,
3139  author = {{Universit\'e Pierre et Marie Curie (UPMC), Paris 6}},
3140  title = {{{UE} : Achitecture des syst\`emes int\'egr\'es, {M1}}},
3141  note = {\url{http://www-master.ufr-info-p6.jussieu.fr/ue/archi/}},
3142  owner = {cecile},
3143  timestamp = {2006.10.05}
3144}
3145
3146@ARTICLE{fms,
3147  author = {D.M.~Upton},
3148  title = {A {F}lexible {S}tructure for {C}omputer-{C}ontrolled {M}anufacturing
3149        {S}ystems},
3150  journal = {Manufacturing Review},
3151  year = {1992},
3152  volume = {5},
3153  pages = {58--74},
3154  number = {1},
3155  keywords = {FMS},
3156  owner = {cecile},
3157  timestamp = {2007.01.22}
3158}
3159
3160@INPROCEEDINGS{Valk93,
3161  author = {R. Valk},
3162  title = {Bridging the Gap between Place- and Floyd-Invariants with Applications
3163        to Preemptive Scheduling},
3164  booktitle = {Proc. of ICATPN'93},
3165  year = {1993},
3166  volume = {691},
3167  series = {Lecture Notes in Computer Science},
3168  pages = {432--452},
3169  publisher = {Springer Verlag}
3170}
3171
3172@INPROCEEDINGS{xie03verified,
3173  author = {F.~Xie and J.C.~Browne},
3174  title = {Verified {S}ystems by {C}omposition from {V}erified {C}omponents},
3175  booktitle = {E{SEC}/{FSE} 2003 : {P}roceedings of the 11th {ACM} {SIGSOFT} {S}ymposium
3176        on {F}oundations of {S}oftware {E}ngineering 2003 held jointly with
3177        9th {E}uropean {S}oftware {E}ngineering {C}onference},
3178  year = {2003},
3179  pages = {277--286},
3180  address = {Helsinki, Finland},
3181  publisher = {ACM Press},
3182  comment = {: Proceedings of the 9th European software engineering conference
3183        held jointly with 11th ACM SIGSOFT international symposium on Foundations
3184        of software engineering},
3185  doi = {http://doi.acm.org/10.1145/940071.940109},
3186  isbn = {1-58113-743-5},
3187  location = {Helsinki, Finland}
3188}
3189
3190@PHDTHESIS{Yadgar10thesis,
3191  author = {Avi Yadgar},
3192  title = {New Approaches to Model Checking and to 3-Valued Abstraction and
3193        Refinement},
3194  school = {Technion - Israel Institute of Technology},
3195  year = {2010},
3196  file = {:/users/outil/verif/biblio/Cegar/AviYadgarPhDThesisReport.pdf:PDF},
3197  keywords = {Cegar, BMC, 3-valued, Abstraction},
3198  owner = {verif},
3199  timestamp = {2010.06.15}
3200}
3201
3202@TECHREPORT{cegarhwcasestudy07,
3203  author = {Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah},
3204  title = {CEGAR-Based Formal Hardware Verification: A Case Study},
3205  institution = {Department of Electrical Engineering and Computer Science
3206       
3207        University of Michigan},
3208  year = {2007},
3209  file = {:Cegar/CEGARHWVerifCaseStudy07.pdf:PDF},
3210  keywords = {CEGAR,hardware},
3211  owner = {cecile},
3212  timestamp = {2010.06.10}
3213}
3214
3215@ARTICLE{Zaki08analogformalsurvey,
3216  author = {M.H~Zaki and S.~Tahar and G.~Bois},
3217  title = {Formal verification of analog and mixed signal designs: A survey},
3218  journal = {Microelectronics Journal},
3219  year = {2008},
3220  volume = {39},
3221  pages = {1395--1404},
3222  number = {12},
3223  address = {Amsterdam, The Netherlands, The Netherlands},
3224  doi = {http://dx.doi.org/10.1016/j.mejo.2008.05.013},
3225  file = {:Analog/surveyZaki08.pdf:PDF},
3226  issn = {0026-2692},
3227  publisher = {Elsevier Science Publishers B. V.}
3228}
3229
3230@ARTICLE{5374376,
3231  author = {Hao Zheng and Haiqiong Yao and Yoneda, T.},
3232  title = {Modular Model Checking of Large Asynchronous Designs with Efficient
3233        Abstraction Refinement},
3234  journal = {Computers, IEEE Transactions on},
3235  year = {2010},
3236  volume = {59},
3237  pages = {561 -573},
3238  number = {4},
3239  month = {april },
3240  abstract = {Divide-and-conquer is essential to address state explosion in model
3241        checking. Verifying each individual component in a system, in isolation,
3242        efficiently requires an appropriate context, which traditionally
3243        is obtained by hand. This paper presents an efficient modular model
3244        checking approach for asynchronous design verification. It is equipped
3245        with a novel abstraction refinement method that can refine a component
3246        abstraction to be accurate enough for successful verification. It
3247        is fully automated, and eliminates the need of finding an accurate
3248        context when verifying each individual component, although such a
3249        context is still highly desirable. This method is also enhanced with
3250        additional state space reduction techniques. The experiments on several
3251        nontrivial asynchronous designs show that this method efficiently
3252        removes impossible behaviors from each component including ones violating
3253        correctness requirements.},
3254  doi = {10.1109/TC.2009.187},
3255  file = {:/users/outil/verif/biblio/Composition/ModularMCLargeAsynchronousDesignwithAR2010.pdf:PDF},
3256  issn = {0018-9340},
3257  keywords = {abstraction refinement;abstraction refinement method;large asynchronous
3258        designs;modular model checking;state explosion;state space reduction
3259        techniques;formal verification;state-space methods; composition},
3260  owner = {cecile},
3261  review = {Verification of a whole system by verifying each components. When
3262        verifying each components individually assumptions has to be made
3263        on the environnment ot avoid false counter-examples. Use component
3264        abstraction to over-approximated the environment. This abastraction
3265        must be refined to obtain only the behavior allowed at the interface.
3266        They propose :
3267       
3268        <ul>
3269       
3270        <li>     to identify and remove unsynchronized behavior.
3271       
3272         <li> to extend the refinement to more than two components itemize
3273       
3274       
3275        </ul>
3276       
3277       
3278        Main contribution : Local synchronization detection method for component
3279        based on parallel composition and an AR methof for modular MC.
3280       
3281        <br>
3282       
3283        Circuit class : Asynchronous</td>},
3284  timestamp = {2012.03.07}
3285}
3286
3287@PROCEEDINGS{DBLP:conf/fmcad/2002,
3288  title = {Formal Methods in Computer-Aided Design, 4th International Conference,
3289        FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings},
3290  year = {2002},
3291  editor = {Mark Aagaard and John W. O'Leary},
3292  volume = {2517},
3293  series = {Lecture Notes in Computer Science},
3294  publisher = {Springer},
3295  bibsource = {DBLP, http://dblp.uni-trier.de},
3296  booktitle = {FMCAD},
3297  isbn = {3-540-00116-6}
3298}
3299
3300@PROCEEDINGS{DBLP:conf/sefm/2005,
3301  title = {Third IEEE International Conference on Software Engineering and Formal
3302        Methods (SEFM 2005), 7-9 September 2005, Koblenz, Germany},
3303  year = {2005},
3304  editor = {Bernhard K. Aichernig and Bernhard Beckert},
3305  publisher = {IEEE Computer Society},
3306  bibsource = {DBLP, http://dblp.uni-trier.de},
3307  booktitle = {SEFM},
3308  isbn = {0-7695-2435-4}
3309}
3310
3311@PROCEEDINGS{DBLP:conf/cav/2004,
3312  title = {Computer Aided Verification, 16th International Conference, CAV 2004,
3313        Boston, MA, USA, July 13-17, 2004, Proceedings},
3314  year = {2004},
3315  editor = {Rajeev Alur and Doron Peled},
3316  volume = {3114},
3317  series = {Lecture Notes in Computer Science},
3318  publisher = {Springer},
3319  bibsource = {DBLP, http://dblp.uni-trier.de},
3320  booktitle = {CAV},
3321  isbn = {3-540-22342-8}
3322}
3323
3324@PROCEEDINGS{DBLP:conf/cav/2006,
3325  title = {CAV'06: Proceedings of 18th International Conference of Computer
3326        Aided Verification},
3327  year = {2006},
3328  editor = {Thomas Ball and Robert B. Jones},
3329  volume = {4144},
3330  series = {Lecture Notes in Computer Science},
3331  address = {Seattle, WA, USA},
3332  bibsource = {DBLP, http://dblp.uni-trier.de},
3333  booktitle = {CAV},
3334  isbn = {3-540-37406-X}
3335}
3336
3337@PROCEEDINGS{DBLP:conf/sfm/2006,
3338  title = {Formal Methods for Hardware Verification, 6th International School
3339        on Formal Methods for the Design of Computer, Communication, and
3340        Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced
3341        Lectures},
3342  year = {2006},
3343  editor = {Marco Bernardo and Alessandro Cimatti},
3344  volume = {3965},
3345  series = {Lecture Notes in Computer Science},
3346  publisher = {Springer},
3347  bibsource = {DBLP, http://dblp.uni-trier.de},
3348  booktitle = {SFM},
3349  isbn = {978-3-540-34304-2}
3350}
3351
3352@PROCEEDINGS{DBLP:conf/cav/2001,
3353  title = {Computer Aided Verification, 13th International Conference, CAV 2001,
3354        Paris, France, July 18-22, 2001, Proceedings},
3355  year = {2001},
3356  editor = {G{\'e}rard Berry and Hubert Comon and Alain Finkel},
3357  volume = {2102},
3358  series = {Lecture Notes in Computer Science},
3359  publisher = {Springer},
3360  bibsource = {DBLP, http://dblp.uni-trier.de},
3361  booktitle = {CAV},
3362  isbn = {3-540-42345-1}
3363}
3364
3365@PROCEEDINGS{DBLP:conf/hvc/2006,
3366  title = {Hardware and Software, Verification and Testing, Second International
3367        Haifa Verification Conference, HVC 2006, Haifa, Israel, October 23-26,
3368        2006. Revised Selected Papers},
3369  year = {2007},
3370  editor = {Eyal Bin and Avi Ziv and Shmuel Ur},
3371  volume = {4383},
3372  series = {Lecture Notes in Computer Science},
3373  publisher = {Springer},
3374  bibsource = {DBLP, http://dblp.uni-trier.de},
3375  booktitle = {Haifa Verification Conference},
3376  isbn = {978-3-540-70888-9}
3377}
3378
3379@PROCEEDINGS{DBLP:conf/fmco/2005,
3380  title = {Formal Methods for Components and Objects, 4th International Symposium,
3381        FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised
3382        Lectures},
3383  year = {2006},
3384  editor = {Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem
3385        P. de Roever},
3386  volume = {4111},
3387  series = {Lecture Notes in Computer Science},
3388  publisher = {Springer},
3389  bibsource = {DBLP, http://dblp.uni-trier.de},
3390  booktitle = {FMCO},
3391  isbn = {3-540-36749-7}
3392}
3393
3394@PROCEEDINGS{DBLP:conf/charme/2005,
3395  title = {Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5
3396        Advanced Research Working Conference, CHARME 2005, Saarbr{\"u}cken,
3397        Germany, October 3-6, 2005, Proceedings},
3398  year = {2005},
3399  editor = {Dominique Borrione and Wolfgang J. Paul},
3400  volume = {3725},
3401  series = {Lecture Notes in Computer Science},
3402  publisher = {Springer},
3403  bibsource = {DBLP, http://dblp.uni-trier.de},
3404  booktitle = {CHARME},
3405  isbn = {3-540-29105-9},
3406  owner = {cecile},
3407  timestamp = {2006.06.27}
3408}
3409
3410@PROCEEDINGS{DBLP:conf/cav/2002,
3411  title = {Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen,
3412        Denmark, July 27-31, 2002, Proceedings},
3413  year = {2002},
3414  editor = {Ed Brinksma and Kim Guldstrand Larsen},
3415  volume = {2404},
3416  series = {Lecture Notes in Computer Science},
3417  publisher = {Springer},
3418  bibsource = {DBLP, http://dblp.uni-trier.de},
3419  booktitle = {CAV},
3420  isbn = {3-540-43997-8}
3421}
3422
3423@PROCEEDINGS{DBLP:conf/fase/2005,
3424  title = {Fundamental Approaches to Software Engineering, 8th International
3425        Conference, FASE 2005, Held as Part of the Joint European Conferences
3426        on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April
3427        4-8, 2005, Proceedings},
3428  year = {2005},
3429  editor = {Maura Cerioli},
3430  volume = {3442},
3431  series = {Lecture Notes in Computer Science},
3432  publisher = {Springer},
3433  bibsource = {DBLP, http://dblp.uni-trier.de},
3434  booktitle = {FASE},
3435  isbn = {3-540-25420-X}
3436}
3437
3438@PROCEEDINGS{DBLP:conf/lpar/2008,
3439  title = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th
3440        International Conference, LPAR 2008, Doha, Qatar, November 22-27,
3441        2008. Proceedings},
3442  year = {2008},
3443  editor = {Iliano Cervesato and Helmut Veith and Andrei Voronkov},
3444  volume = {5330},
3445  series = {Lecture Notes in Computer Science},
3446  publisher = {Springer},
3447  bibsource = {DBLP, http://dblp.uni-trier.de},
3448  booktitle = {LPAR},
3449  isbn = {978-3-540-89438-4}
3450}
3451
3452@PROCEEDINGS{DBLP:conf/vmcai/2005,
3453  title = {Verification, Model Checking, and Abstract Interpretation, 6th International
3454        Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings},
3455  year = {2005},
3456  editor = {Radhia Cousot},
3457  volume = {3385},
3458  series = {Lecture Notes in Computer Science},
3459  publisher = {Springer},
3460  bibsource = {DBLP, http://dblp.uni-trier.de},
3461  booktitle = {VMCAI},
3462  isbn = {3-540-24297-X}
3463}
3464
3465@PROCEEDINGS{DBLP:conf/tcs/1981,
3466  title = {Theoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany,
3467        March 23-25, 1981, Proceedings},
3468  year = {1981},
3469  editor = {Peter Deussen},
3470  volume = {104},
3471  series = {Lecture Notes in Computer Science},
3472  publisher = {Springer},
3473  bibsource = {DBLP, http://dblp.uni-trier.de},
3474  booktitle = {Theoretical Computer Science},
3475  isbn = {3-540-10576-X}
3476}
3477
3478@PROCEEDINGS{DBLP:conf/vmcai/2006,
3479  title = {Verification, Model Checking, and Abstract Interpretation, 7th International
3480        Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006,
3481        Proceedings},
3482  year = {2006},
3483  editor = {E. Allen Emerson and Kedar S. Namjoshi},
3484  volume = {3855},
3485  series = {Lecture Notes in Computer Science},
3486  publisher = {Springer},
3487  bibsource = {DBLP, http://dblp.uni-trier.de},
3488  booktitle = {VMCAI},
3489  isbn = {3-540-31139-4}
3490}
3491
3492@PROCEEDINGS{DBLP:conf/cav/2000,
3493  title = {Computer Aided Verification, 12th International Conference, CAV 2000,
3494        Chicago, IL, USA, July 15-19, 2000, Proceedings},
3495  year = {2000},
3496  editor = {E.A.~Emerson and A.P.~Sistla},
3497  volume = {1855},
3498  series = {Lecture Notes in Computer Science},
3499  publisher = {Springer},
3500  bibsource = {DBLP, http://dblp.uni-trier.de},
3501  booktitle = {CAV},
3502  isbn = {3-540-67770-4},
3503  owner = {cecile},
3504  timestamp = {2006.02.13}
3505}
3506
3507@PROCEEDINGS{DBLP:conf/apn/2002,
3508  title = {Applications and Theory of Petri Nets 2002, 23rd International Conference,
3509        ICATPN 2002, Adelaide, Australia, June 24-30, 2002, Proceedings},
3510  year = {2002},
3511  editor = {Javier Esparza and Charles Lakos},
3512  volume = {2360},
3513  series = {Lecture Notes in Computer Science},
3514  publisher = {Springer},
3515  bibsource = {DBLP, http://dblp.uni-trier.de},
3516  booktitle = {ICATPN},
3517  isbn = {3-540-43787-8}
3518}
3519
3520@PROCEEDINGS{DBLP:conf/date/2006p,
3521  title = {Proceedings of the Conference on Design, Automation and Test in Europe,
3522        DATE 2006, Munich, Germany, March 6-10, 2006},
3523  year = {2006},
3524  editor = {Georges G. E. Gielen},
3525  publisher = {European Design and Automation Association, Leuven, Belgium},
3526  bibsource = {DBLP, http://dblp.uni-trier.de},
3527  booktitle = {DATE},
3528  isbn = {3-9810801-0-6}
3529}
3530
3531@PROCEEDINGS{DBLP:conf/sat/2003,
3532  title = {Theory and Applications of Satisfiability Testing, 6th International
3533        Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003
3534        Selected Revised Papers},
3535  year = {2004},
3536  editor = {Enrico Giunchiglia and Armando Tacchella},
3537  volume = {2919},
3538  series = {Lecture Notes in Computer Science},
3539  publisher = {Springer},
3540  bibsource = {DBLP, http://dblp.uni-trier.de},
3541  booktitle = {SAT},
3542  isbn = {3-540-20851-8}
3543}
3544
3545@PROCEEDINGS{DBLP:conf/frocos/2005,
3546  title = {Frontiers of Combining Systems, 5th International Workshop, FroCoS
3547        2005, Vienna, Austria, September 19-21, 2005, Proceedings},
3548  year = {2005},
3549  editor = {Bernhard Gramlich},
3550  volume = {3717},
3551  series = {Lecture Notes in Computer Science},
3552  publisher = {Springer},
3553  bibsource = {DBLP, http://dblp.uni-trier.de},
3554  booktitle = {FroCoS},
3555  isbn = {3-540-29051-6}
3556}
3557
3558@PROCEEDINGS{DBLP:conf/cav/1997,
3559  title = {Computer Aided Verification, 9th International Conference, CAV '97,
3560        Haifa, Israel, June 22-25, 1997, Proceedings},
3561  year = {1997},
3562  editor = {Orna Grumberg},
3563  volume = {1254},
3564  series = {Lecture Notes in Computer Science},
3565  publisher = {Springer},
3566  bibsource = {DBLP, http://dblp.uni-trier.de},
3567  booktitle = {CAV},
3568  isbn = {3-540-63166-6}
3569}
3570
3571@PROCEEDINGS{DBLP:conf/cav/1999,
3572  title = {Computer Aided Verification, 11th International Conference, CAV '99,
3573        Trento, Italy, July 6-10, 1999, Proceedings},
3574  year = {1999},
3575  editor = {Nicolas Halbwachs and Doron Peled},
3576  volume = {1633},
3577  series = {Lecture Notes in Computer Science},
3578  publisher = {Springer},
3579  bibsource = {DBLP, http://dblp.uni-trier.de},
3580  booktitle = {CAV},
3581  isbn = {3-540-66202-2},
3582  owner = {cecile},
3583  timestamp = {2006.04.25}
3584}
3585
3586@PROCEEDINGS{DBLP:conf/tacas/2005,
3587  title = {Tools and Algorithms for the Construction and Analysis of Systems,
3588        11th International Conference, TACAS 2005, Held as Part of the Joint
3589        European Conferences on Theory and Practice of Software, ETAPS 2005,
3590        Edinburgh, UK, April 4-8, 2005, Proceedings},
3591  year = {2005},
3592  editor = {Nicolas Halbwachs and Lenore D. Zuck},
3593  volume = {3440},
3594  series = {Lecture Notes in Computer Science},
3595  publisher = {Springer},
3596  bibsource = {DBLP, http://dblp.uni-trier.de},
3597  booktitle = {TACAS},
3598  isbn = {3-540-25333-5}
3599}
3600
3601@PROCEEDINGS{DBLP:conf/iccad/2006,
3602  title = {2006 International Conference on Computer-Aided Design (ICCAD'06),
3603        November 5-9, 2006, San Jose, CA, USA},
3604  year = {2006},
3605  editor = {Soha Hassoun},
3606  publisher = {ACM},
3607  bibsource = {DBLP, http://dblp.uni-trier.de},
3608  booktitle = {ICCAD},
3609  isbn = {1-59593-389-1}
3610}
3611
3612@PROCEEDINGS{DBLP:conf/tacas/2006,
3613  title = {Tools and Algorithms for the Construction and Analysis of Systems,
3614        12th International Conference, TACAS 2006 Held as Part of the Joint
3615        European Conferences on Theory and Practice of Software, ETAPS 2006,
3616        Vienna, Austria, March 25 - April 2, 2006, Proceedings},
3617  year = {2006},
3618  editor = {Holger Hermanns and Jens Palsberg},
3619  volume = {3920},
3620  series = {Lecture Notes in Computer Science},
3621  publisher = {Springer},
3622  bibsource = {DBLP, http://dblp.uni-trier.de},
3623  booktitle = {TACAS},
3624  isbn = {3-540-33056-9}
3625}
3626
3627@PROCEEDINGS{DBLP:conf/cav/1998,
3628  title = {Computer Aided Verification, 10th International Conference, CAV '98,
3629        Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings},
3630  year = {1998},
3631  editor = {Alan J. Hu and Moshe Y. Vardi},
3632  volume = {1427},
3633  series = {Lecture Notes in Computer Science},
3634  publisher = {Springer},
3635  bibsource = {DBLP, http://dblp.uni-trier.de},
3636  booktitle = {CAV},
3637  isbn = {3-540-64608-6}
3638}
3639
3640@PROCEEDINGS{DBLP:conf/tacas/2004,
3641  title = {Tools and Algorithms for the Construction and Analysis of Systems,
3642        10th International Conference, TACAS 2004, Held as Part of the Joint
3643        European Conferences on Theory and Practice of Software, ETAPS 2004,
3644        Barcelona, Spain, March 29 - April 2, 2004, Proceedings},
3645  year = {2004},
3646  editor = {Kurt Jensen and Andreas Podelski},
3647  volume = {2988},
3648  series = {Lecture Notes in Computer Science},
3649  publisher = {Springer},
3650  bibsource = {DBLP, http://dblp.uni-trier.de},
3651  booktitle = {TACAS},
3652  isbn = {3-540-21299-X}
3653}
3654
3655@PROCEEDINGS{DBLP:conf/vmcai/2011,
3656  title = {Verification, Model Checking, and Abstract Interpretation - 12th
3657        International Conference, VMCAI 2011, Austin, TX, USA, January 23-25,
3658        2011. Proceedings},
3659  year = {2011},
3660  editor = {Ranjit Jhala and David A. Schmidt},
3661  volume = {6538},
3662  series = {Lecture Notes in Computer Science},
3663  publisher = {Springer},
3664  bibsource = {DBLP, http://dblp.uni-trier.de},
3665  booktitle = {VMCAI},
3666  ee = {http://dx.doi.org/10.1007/978-3-642-18275-4},
3667  isbn = {978-3-642-18274-7}
3668}
3669
3670@PROCEEDINGS{DBLP:conf/cav/2003,
3671  title = {Computer Aided Verification, 15th International Conference, CAV 2003,
3672        Boulder, CO, USA, July 8-12, 2003, Proceedings},
3673  year = {2003},
3674  editor = {Warren A. Hunt Jr. and Fabio Somenzi},
3675  volume = {2725},
3676  series = {Lecture Notes in Computer Science},
3677  publisher = {Springer},
3678  bibsource = {DBLP, http://dblp.uni-trier.de},
3679  booktitle = {CAV},
3680  isbn = {3-540-40524-0}
3681}
3682
3683@PROCEEDINGS{DBLP:conf/dac/2005,
3684  title = {Proceedings of the 42nd Design Automation Conference, DAC 2005, San
3685        Diego, CA, USA, June 13-17, 2005},
3686  year = {2005},
3687  editor = {William H. Joyner Jr. and Grant Martin and Andrew B. Kahng},
3688  publisher = {ACM},
3689  bibsource = {DBLP, http://dblp.uni-trier.de},
3690  booktitle = {DAC},
3691  isbn = {1-59593-058-2}
3692}
3693
3694@PROCEEDINGS{DBLP:conf/lop/1981,
3695  title = {Logic of Programs, Workshop},
3696  year = {1982},
3697  editor = {Dexter Kozen},
3698  volume = {131},
3699  series = {Lecture Notes in Computer Science},
3700  publisher = {Springer},
3701  bibsource = {DBLP, http://dblp.uni-trier.de},
3702  booktitle = {Logic of Programs},
3703  isbn = {3-540-11212-X}
3704}
3705
3706@PROCEEDINGS{DBLP:conf/dac/2004,
3707  title = {Proceedings of the 41th Design Automation Conference, DAC 2004, San
3708        Diego, CA, USA, June 7-11, 2004},
3709  year = {2004},
3710  editor = {Sharad Malik and Limor Fix and Andrew B. Kahng},
3711  publisher = {ACM},
3712  bibsource = {DBLP, http://dblp.uni-trier.de},
3713  booktitle = {DAC},
3714  isbn = {1-58113-828-8}
3715}
3716
3717@PROCEEDINGS{DBLP:conf/birthday/2010pnueli,
3718  title = {Time for Verification, Essays in Memory of Amir Pnueli},
3719  year = {2010},
3720  editor = {Zohar Manna and Doron Peled},
3721  volume = {6200},
3722  series = {Lecture Notes in Computer Science},
3723  publisher = {Springer},
3724  bibsource = {DBLP, http://dblp.uni-trier.de},
3725  booktitle = {Essays in Memory of Amir Pnueli},
3726  ee = {http://dx.doi.org/10.1007/978-3-642-13754-9},
3727  isbn = {978-3-642-13753-2}
3728}
3729
3730@PROCEEDINGS{DBLP:conf/tacas/2001,
3731  title = {Tools and Algorithms for the Construction and Analysis of Systems,
3732        7th International Conference, TACAS 2001 Held as Part of the Joint
3733        European Conferences on Theory and Practice of Software, ETAPS 2001
3734        Genova, Italy, April 2-6, 2001, Proceedings},
3735  year = {2001},
3736  editor = {Tiziana Margaria and Wang Yi},
3737  volume = {2031},
3738  series = {Lecture Notes in Computer Science},
3739  publisher = {Springer},
3740  bibsource = {DBLP, http://dblp.uni-trier.de},
3741  booktitle = {TACAS},
3742  isbn = {3-540-41865-2}
3743}
3744
3745@PROCEEDINGS{DBLP:conf/sbmf/2009,
3746  title = {Formal Methods: Foundations and Applications, 12th Brazilian Symposium
3747        on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009,
3748        Revised Selected Papers},
3749  year = {2009},
3750  editor = {Marcel Vinicius Medeiros Oliveira and Jim Woodcock},
3751  volume = {5902},
3752  series = {Lecture Notes in Computer Science},
3753  publisher = {Springer},
3754  bibsource = {DBLP, http://dblp.uni-trier.de},
3755  booktitle = {SBMF},
3756  ee = {http://dx.doi.org/10.1007/978-3-642-10452-7},
3757  isbn = {978-3-642-10451-0}
3758}
3759
3760@PROCEEDINGS{DBLP:conf/concur/2000,
3761  title = {CONCUR 2000 - Concurrency Theory, 11th International Conference,
3762        University Park, PA, USA, August 22-25, 2000, Proceedings},
3763  year = {2000},
3764  editor = {Catuscia Palamidessi},
3765  volume = {1877},
3766  series = {Lecture Notes in Computer Science},
3767  publisher = {Springer},
3768  bibsource = {DBLP, http://dblp.uni-trier.de},
3769  booktitle = {CONCUR},
3770  isbn = {3-540-67897-2}
3771}
3772
3773@PROCEEDINGS{DBLP:conf/tacas/2008,
3774  title = {Tools and Algorithms for the Construction and Analysis of Systems,
3775        14th International Conference, TACAS 2008, Held as Part of the Joint
3776        European Conferences on Theory and Practice of Software, ETAPS 2008,
3777        Budapest, Hungary, March 29-April 6, 2008. Proceedings},
3778  year = {2008},
3779  editor = {C. R. Ramakrishnan and Jakob Rehof},
3780  volume = {4963},
3781  series = {Lecture Notes in Computer Science},
3782  publisher = {Springer},
3783  bibsource = {DBLP, http://dblp.uni-trier.de},
3784  booktitle = {TACAS},
3785  isbn = {978-3-540-78799-0}
3786}
3787
3788@PROCEEDINGS{DBLP:conf/compos/1997,
3789  title = {Compositionality: The Significant Difference, International Symposium,
3790        COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures},
3791  year = {1998},
3792  editor = {Willem P. de Roever and Hans Langmaack and Amir Pnueli},
3793  volume = {1536},
3794  series = {Lecture Notes in Computer Science},
3795  publisher = {Springer},
3796  bibsource = {DBLP, http://dblp.uni-trier.de},
3797  booktitle = {COMPOS},
3798  isbn = {3-540-65493-3}
3799}
3800
3801@PROCEEDINGS{DBLP:conf/dac/2006,
3802  title = {Proceedings of the 43rd Design Automation Conference, DAC 2006, San
3803        Francisco, CA, USA, July 24-28, 2006},
3804  year = {2006},
3805  editor = {Ellen Sentovich},
3806  publisher = {ACM},
3807  bibsource = {DBLP, http://dblp.uni-trier.de},
3808  booktitle = {DAC},
3809  isbn = {1-59593-381-6}
3810}
3811
3812@PROCEEDINGS{DBLP:conf/tacas/1998,
3813  title = {Tools and Algorithms for Construction and Analysis of Systems, 4th
3814        International Conference, TACAS '98, Held as Part of the European
3815        Joint Conferences on the Theory and Practice of Software, ETAPS'98,
3816        Lisbon, Portugal, March 28 - April 4, 1998, Proceedings},
3817  year = {1998},
3818  editor = {Bernhard Steffen},
3819  volume = {1384},
3820  series = {Lecture Notes in Computer Science},
3821  publisher = {Springer},
3822  bibsource = {DBLP, http://dblp.uni-trier.de},
3823  booktitle = {TACAS},
3824  isbn = {3-540-64356-7}
3825}
3826
3827@PROCEEDINGS{DBLP:conf/forte/2005,
3828  title = {Formal Techniques for Networked and Distributed Systems - FORTE 2005,
3829        25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October
3830        2-5, 2005, Proceedings},
3831  year = {2005},
3832  editor = {Farn Wang},
3833  volume = {3731},
3834  series = {Lecture Notes in Computer Science},
3835  publisher = {Springer},
3836  bibsource = {DBLP, http://dblp.uni-trier.de},
3837  booktitle = {FORTE},
3838  isbn = {3-540-29189-X}
3839}
3840
3841@PROCEEDINGS{DBLP:conf/fm/1999-1,
3842  title = {FM'99 - Formal Methods, World Congress on Formal Methods in the Development
3843        of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings,
3844        Volume I},
3845  year = {1999},
3846  editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
3847  volume = {1708},
3848  series = {Lecture Notes in Computer Science},
3849  publisher = {Springer},
3850  bibsource = {DBLP, http://dblp.uni-trier.de},
3851  booktitle = {World Congress on Formal Methods},
3852  isbn = {3-540-66587-0}
3853}
3854
3855@MISC{alliance,
3856  title = {Alliance, a free {VLSI} cad system},
3857  note = {\\\url{http://www-asim.lip6.fr/recherche/alliance/}},
3858  owner = {cecile},
3859  timestamp = {2007.02.01}
3860}
3861
3862@MISC{onespin,
3863  title = {OneSpin Solutions},
3864  note = {\url{http://www.onespin-solutions.com/}},
3865  key = OneS,
3866  owner = {cecile},
3867  timestamp = {2007.03.07}
3868}
3869
3870@MISC{prosyd,
3871  title = {The Prosyd Project on Property-Based System Design},
3872  note = {{\url{http://www.prosyd.org/}}},
3873  owner = {cecile},
3874  timestamp = {2007.02.07}
3875}
3876
3877@MISC{soclib,
3878  title = {The {S}o{CL}ib {P}roject},
3879  note = {\url{http://soclib.lip6.fr/}},
3880  key = SoC,
3881  owner = {cecile},
3882  timestamp = {2006.09.07},
3883  url = {http://soclib.lip6.fr/}
3884}
3885
3886@MISC{texas97bench,
3887  title = {Texas-97 {V}erification {B}enchmarks},
3888  note = {\\\url{http://www.cad.eecs.berkeley.edu/Respep/Research/vis/texas-97/}},
3889  key = TEXAS,
3890  keywords = {protocol, PIbus},
3891  owner = {cecile},
3892  timestamp = {2006.11.30}
3893}
3894
3895@MISC{vsia,
3896  title = {{VSI A}lliance},
3897  note = {\url{http://www.vsi.org/}},
3898  key = VSI,
3899  owner = {cecile},
3900  timestamp = {2006.09.13}
3901}
3902
3903@PROCEEDINGS{DBLP:conf/date/2009,
3904  title = {Design, Automation and Test in Europe, DATE 2009, Nice, France, April
3905        20-24, 2009},
3906  year = {2009},
3907  publisher = {IEEE},
3908  bibsource = {DBLP, http://dblp.uni-trier.de},
3909  booktitle = {DATE}
3910}
3911
3912@PROCEEDINGS{DBLP:conf/fmcad/2009,
3913  title = {Proceedings of 9th International Conference on Formal Methods in
3914        Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas,
3915        USA},
3916  year = {2009},
3917  publisher = {IEEE},
3918  bibsource = {DBLP, http://dblp.uni-trier.de},
3919  booktitle = {FMCAD},
3920  isbn = {978-1-4244-4966-8}
3921}
3922
3923@PROCEEDINGS{DBLP:conf/lics/2004,
3924  title = {19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17
3925        July 2004, Turku, Finland, Proceedings},
3926  year = {2004},
3927  publisher = {IEEE Computer Society},
3928  bibsource = {DBLP, http://dblp.uni-trier.de},
3929  booktitle = {LICS},
3930  isbn = {0-7695-2192-4}
3931}
3932
3933@PROCEEDINGS{DBLP:conf/sat/2004,
3934  title = {SAT 2004 - The Seventh International Conference on Theory and Applications
3935        of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada,
3936        Online Proceedings},
3937  year = {2004},
3938  bibsource = {DBLP, http://dblp.uni-trier.de},
3939  booktitle = {SAT},
3940  owner = {cecile},
3941  timestamp = {2009.01.27}
3942}
3943
3944@PROCEEDINGS{DBLP:conf/date/2003,
3945  title = {2003 Design, Automation and Test in Europe Conference and Exposition
3946        (DATE 2003), 3-7 March 2003, Munich, Germany},
3947  year = {2003},
3948  publisher = {IEEE Computer Society},
3949  bibsource = {DBLP, http://dblp.uni-trier.de},
3950  booktitle = {DATE},
3951  isbn = {0-7695-1870-2}
3952}
3953
3954@PROCEEDINGS{DBLP:conf/icse/2003,
3955  title = {Proceedings of the 25th International Conference on Software Engineering,
3956        May 3-10, 2003, Portland, Oregon, USA},
3957  year = {2003},
3958  publisher = {IEEE Computer Society},
3959  bibsource = {DBLP, http://dblp.uni-trier.de},
3960  booktitle = {ICSE}
3961}
3962
3963@PROCEEDINGS{DBLP:conf/time/2003,
3964  title = {10th International Symposium on Temporal Representation and Reasoning
3965        / 4th International Conference on Temporal Logic (TIME-ICTL 2003),
3966        8-10 July 2003, Cairns, Queensland, Australia},
3967  year = {2003},
3968  publisher = {IEEE Computer Society},
3969  bibsource = {DBLP, http://dblp.uni-trier.de},
3970  booktitle = {TIME},
3971  isbn = {0-7695-1912-1}
3972}
3973
3974@PROCEEDINGS{DBLP:conf/iccd/2002,
3975  title = {20th International Conference on Computer Design (ICCD 2002), VLSI
3976        in Computers and Processors, 16-18 September 2002, Freiburg, Germany,
3977        Proceedings},
3978  year = {2002},
3979  publisher = {IEEE Computer Society},
3980  bibsource = {DBLP, http://dblp.uni-trier.de},
3981  booktitle = {ICCD},
3982  isbn = {0-7695-1700-5},
3983  keywords = {3-valued, logic, model checking, Kripke structure}
3984}
3985
3986@PROCEEDINGS{DBLP:conf/dac/2001,
3987  title = {Proceedings of the 38th Design Automation Conference, DAC 2001, Las
3988        Vegas, NV, USA, June 18-22, 2001},
3989  year = {2001},
3990  publisher = {ACM},
3991  bibsource = {DBLP, http://dblp.uni-trier.de},
3992  booktitle = {DAC},
3993  isbn = {1-58113-297-2}
3994}
3995
3996@PROCEEDINGS{DBLP:conf/icse/2001,
3997  title = {Proceedings of the 23rd International Conference on Software Engineering,
3998        ICSE 2001, 12-19 May 2001, Toronto, Ontario, Canada},
3999  year = {2001},
4000  publisher = {IEEE Computer Society},
4001  bibsource = {DBLP, http://dblp.uni-trier.de},
4002  booktitle = {ICSE},
4003  isbn = {0-7695-1050-7}
4004}
4005
4006@MANUAL{amba,
4007  title = {AMBA Specification},
4008  organization = {ARM limited},
4009  edition = {2.0},
4010  year = {1999},
4011  note = {ARM Limited \copyright. All right reserved},
4012  file = {IHI0011A_AMBA_SPEC.pdf:/dsk/l1/misc/doc/amba/IHI0011A_AMBA_SPEC.pdf:PDF},
4013  key = AMBA,
4014  owner = {cecile},
4015  timestamp = {2006.09.07}
4016}
4017
4018@MANUAL{formalcheck,
4019  title = {Formal Verification Using Affirma {FormalCheck}},
4020  organization = {Cadence},
4021  month = {October},
4022  year = {1999}
4023}
4024
4025@PROCEEDINGS{DBLP:conf/lics/LICS4,
4026  title = {Proceedings, Fourth Annual Symposium on Logic in Computer Science,
4027        5-8 June, 1989, Asilomar Conference Center, Pacific Grove, California,
4028        USA},
4029  year = {1989},
4030  publisher = {IEEE Computer Society},
4031  bibsource = {DBLP, http://dblp.uni-trier.de},
4032  booktitle = {LICS}
4033}
4034
4035@PROCEEDINGS{DBLP:conf/lics/LICS3,
4036  title = {Proceedings, Third Annual Symposium on Logic in Computer Science},
4037  year = {1988},
4038  address = {Edinburgh, Scotland, UK},
4039  publisher = {IEEE Computer Society},
4040  bibsource = {DBLP, http://dblp.uni-trier.de},
4041  booktitle = {LICS}
4042}
4043
4044@PROCEEDINGS{DBLP:conf/stoc/STOC14,
4045  title = {Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing,
4046        5-7 May 1982, San Francisco, California, USA},
4047  year = {1982},
4048  publisher = {ACM},
4049  bibsource = {DBLP, http://dblp.uni-trier.de},
4050  booktitle = {STOC}
4051}
4052
Note: See TracBrowser for help on using the repository browser.