source: papers/FDL2012/myBib.bib @ 78

Last change on this file since 78 was 76, checked in by ema, 13 years ago
  • Property svn:executable set to *
File size: 11.9 KB
Line 
1@article{ bryant92bdd,
2    author = "Randal E. Bryant",
3    title = "Symbolic {Boolean} Manipulation with Ordered Binary-Decision Diagrams",
4    journal = {ACM Computing Surveys},
5    volume = 24,
6    number = 3,
7    pages = {293-318},
8    year = 1992
9}
10
11@ARTICLE{clarke94model,
12  author = {E.M.~Clarke and O.~Grumberg and D.E.~Long},
13  title = {{Model Checking and Abstraction}},
14  journal = {ACM Transactions on Programming Languages and Systems},
15  year = {1994},
16  volume = {16},
17  pages = {1512--1542},
18  number = {5},
19  address = {New York, NY, USA},
20  doi = {http://doi.acm.org/10.1145/186025.186051},
21  issn = {0164-0925},
22  keywords = {model cheking, abstraction, CTL, preservation},
23  publisher = {ACM Press}
24}
25@PHDTHESIS{braunstein_phd07,
26  author = {C.~Braunstein},
27  title = {"Conception Incrémentale, Vérification de Composants Matériels et
28        Méthode d'abstraction pour la Vérification de SystÚmes Intégrés sur
29        Puce"},
30  school = {{Universitée Pierre et Marie Curie (Paris 6)}},
31  year = {2007},
32  address = {LIP6/SOC},
33  owner = {cecile},
34  timestamp = {2007.04.16}
35}
36
37
38@article{ mcMillan93symbolic_mc,
39    author = "K. McMillan",
40    title = "{Symbolic Model-checking}",
41    journal = {Kluwer Academic Publisher},
42    year =  1993
43}
44
45
46@conference{ ClarkeEmerson81temporal_logic,
47   author = "E. M. Clarke and  E. A. Emerson",
48   title = "Design and systhesis of synchronization  skeletons using branching time temporal logic",
49   booktitle = "In Logic of Programs Workshop",
50   volume = 131,
51   address = "Yorktown Heights, New York",
52   year = 1981,
53   month = May,
54   publisher = "LNCS 131, Springer "
55}
56
57@article{ ClarkeEmersonSistla86verif_temporal,
58   author = "E. M. Clarke and  E. A. Emerson and A. P. Sistla",
59   title = "Automatic verification of finite-state concurrent systems using temporal logic specifications",
60   journal = "ACM Transactions on Programming Languages and Systems",
61   volume = 8,
62   number = 2,
63   pages = {244-263},
64   year = 1986,
65   month = Apr
66}
67
68@conference{ clarke00cegar,
69   author = "E. M. Clarke and  O. Grumberg and S. Jha and Y. Lu and H. Veith",
70   title = "{Counterexample-guided Abstraction Refinement}",
71   booktitle = "Computer Aided Verification (CAV '00)",
72   address = "Chicago, IL",
73   year = 2000,
74   publisher = "Lecture Notes in Computer Science"
75}
76
77@conference{ QuielleSifakis82spec_verif,
78   author = "J. P. Queille and J. Sifakis",
79   title = "Specification and verification of concurrent systems in CESAR",
80   booktitle = "In Proceedings of the 5th International Symposium on Programming",
81   volume = 137,
82   address = "Turin, Italy",
83   year = 1982,
84   month = April,
85   publisher = "LNCS 137, Springer "
86}
87
88
89
90@conference{ BCCFZ04SMC_with_SAT,
91    author = "A. Biere and A. Cimatti and E. Clarke and M.Fujita and Y. Zhu",
92    title = "{ Symbolic Model  Checking using SAT procedures instead of BDDs}",
93     booktitle = {Proceedings: Design Automation Conference (DAC '99)},
94    pages = {317-320},
95    year = 1999,
96    month = February,
97}
98
99
100@article{ ucberkeley96vis,
101    author = "The VIS Group",
102    title = "{VIS: A system for Verification and Synthesis}",
103    journal = {Springer Lecture Notes in Computer Science},
104    volume = 1102,
105    number = 1102,
106    pages = {428-432},
107    year = 1996
108}
109
110
111@conference{ ucolorado04circus,
112    author = "H. S. Jin and M. Awedh and F. Somenzi",
113    title = "{CirCUs: A Satisfiablilty Solver Geared Towards Bounded Model Checking}",
114     booktitle = {16th Conference on Computer Aided Verification (CAV '04)},
115    pages = {519-522},
116    year = 2004,
117    month = Jul,
118    publisher = "LNCS 3114"
119}
120
121@article{ clarke95counterexamples,
122    author = "E. M. Clarke and O. Grumberg and K. L. McMillan and X. Zhao",
123    title = "{Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking}",
124    journal = {32nd ACM/IEEE Design Automation Conference},
125    year = 1995
126}
127
128@article{ braunstein07ctl_abstraction,
129    author = "C. Braunstein and E. Encrenaz",
130    title = "{Using CTL Formulae as Component Abstraction in a Design Verification Flow}",
131    journal = {ACSD IEEE Computer Society Press},
132    pages = {80-89},
133    year = 2007
134}
135
136@article{ belnap77,
137    author = "N. Belnap",
138    title = "{A useful four-valued logic}",
139    journal = {Modern Uses of Multiple-Valued Logic},
140    pages = {8-37},
141    year = 1977
142}
143
144
145@article{ bara08abs_composant,
146    author = "A. Bara",
147    title = "{Abstraction de Composant pour la Vérification par Model-Checking}",
148    journal = {Mémoire de DiplÃŽme Universitaire OMP - LIP6-SOC},
149    year =  2008
150}
151
152
153@conference{ emma03ctl_ambigous,
154   author = "C. Roux and  E. Encrenaz ",
155   title = "{CTL} may be ambigous when model-checking {Moore Machines} ",
156   booktitle = " IFIP WG 10.5 12th International Advance Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)",
157   volume = 2860,
158   address = "Italy",
159   year = 2003,
160   month = Nov,
161   publisher = "Lecture Notes in Computer Science"
162}
163
164
165@conference{ XieBrowne03composition_soft,
166   author = "F. Xie and J.C. Browne ",
167   title = "{Verified Systems by Composition from Verified Components} ",
168   booktitle = " In ESEC/FSE 2003: Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering Conference",
169    pages = {227-286},
170   address = "Helsinki, Finland",
171   year = 2003,
172   publisher = "ACM Press"
173}
174
175
176@conference{ PMT02compositional_MC,
177   author = "H. Peng and Y. Mokhtari and S. Tahar ",
178   title = "{Environment Synthesis for Compositional Model Checking} ",
179   booktitle = "In ICCD’02 : Proceedings of the 20th International Conference on Computer Design",
180   pages = {70-75},
181   address = "Freiburg, Germany",
182   year = 2002,
183   publisher = "IEEE Computer Society"
184}
185
186
187@conference{ SNBE06property_based,
188   author = "M. Schickel  and V. Nimbler and M. Braun and H. Eveking ",
189   title = "{On Consistency and Completeness of Property-Sets: Exploiting the Property-Based Design Process} ",
190   booktitle = "In FDL’06: Proceedings of  Forum on specification and Design Languages",
191   year = 2006
192}
193
194
195@conference{ CiardoLS00mdd_async,
196   author = "G.Ciardo and G. LÃŒttgen and R. Siminiceanu",
197   title = "{ Efficient symbolic state-space construction for asynchronous systems} ",
198   booktitle = "In Proc. of ICATPN '2000",
199   volume = 1825,
200   pages = {103-122},
201   year = 2000,
202   publisher = "Lecture Notes in Computer Science, Springer Verlag"
203}
204
205@conference{ CTM05hdd,
206   author = "J-M. Couvreur and Y. Thierry-Mieg",
207   title = "{ Hierarchical Decision Diagrams to Exploit Model Structure} ",
208   booktitle = "In FORTE : Proceedings of the 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked  and Distributed Systems",
209   volume = 3731,
210   pages = {443-457},
211   address = "Taipei, Taiwan",
212   year = 2005,
213   publisher = "Lecture Notes in Computer Science, Springer"
214}
215
216
217@conference{ HQR98assume_guarantee,
218   author = "T. A. Henzinger and S. Qadeer and S. K. Rajamani",
219   title = "{ You Assume, We Guarantee : Methodology and Case Studies} ",
220   booktitle = "CAV ’98 : Proceedings of the 10th International Conference on Computer Aided Verification",
221   volume = 1427,
222   pages = {440-451},
223   address = "Vancouver, Canada",
224   year = 1998,
225   publisher = " Lecture Notes in Computer Science, Springer-Verlag"
226}
227
228
229@conference{ GrumbergLong91assume_guarantee,
230   author = " O. Grumberg and D. E. Long",
231   title = "{  Model Checking and Modular Verification} ",
232   booktitle = " In International Conference on Concurency Theory",
233   volume = 527,
234   pages = {250-263},
235   year = 1991,
236   publisher = " Lecture Notes in Computer Science, Springer-Verlag"
237}
238
239
240@conference{ GrafSaidi97abstract_construct,
241   author = "  S. Graf and H. Saïdi",
242   title = "{ Construction of Abstract State Graphs with PVS} ",
243   booktitle = " In CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification",
244   volume = 1254,
245   year = 1997,
246   publisher = " Lecture Notes in Computer Science, Springer"
247}
248
249
250
251@conference{ PardoHachtel97autoAbsMC,
252   author = "  S. Pardo and G. Hachtel",
253   title = "{ Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ",
254   booktitle = " In CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification",
255   volume = 1254,
256   pages = {12-23},
257   year = 1997,
258   publisher = " Lecture Notes in Computer Science, Springer-Verlag"
259}
260
261
262@conference{ PardoHachtel98incremCTLMC,
263   author = "  S. Pardo and G. Hachtel",
264   title = "{ Incremental CTL Model Checking Using BDD Subsetting} ",
265   booktitle = " In DAC ’98: 35th Design Automation Conference ",
266   pages = {457-462},
267   year = 1998,
268}
269
270
271@conference{ Burch_al91smc_part_transition,
272   author = " J. R. Burch and E. M. Clarke and D. E. Long",
273   title = "{ Symbolic Model Checking with Partitioned Transition Relations} ",
274   booktitle = "Proceedings of the 1991 International Conference on VLSI",
275   pages = {49-58},
276   month = August,
277   year = 1991,
278}
279
280
281@conference{ Burch_al93smc_circuit_verif,
282   author = " J. R. Burch and E. M. Clarke and D. E. Long and K. L. Mcmillan and D.L. Dilli",
283   title = "{ Symbolic Model Checking for Sequential Circuit Verification} ",
284   booktitle = " IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",
285   volume = {13(4)},
286   pages = {401-424},
287   year = 1993,
288}
289
290
291@conference{ Kroening_al07vcegar,
292   author = " Himanshu Jain and Daniel Kroening and Natasha Sharygina and Edmund Clarke",
293   title = "{ VCEGAR: Verilog CounterExample Guided Abstraction Refinement} ",
294   booktitle = " In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)",
295   year = 2007,
296}
297
298
299@conference{ microsoft04SLAM,
300   author = " Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani",
301   title = "{ SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft} ",
302   booktitle = " Fourth International Conference on Integrated Formal Methods (IFM 2004)",
303   volume = 2999,
304   pages = {1-20},
305   year = 2004,
306   publisher = " Lecture Notes in Computer Science, Springer"
307}
308
309
310@conference{ berkeley07BLAST,
311   author = "  Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
312   title = "{ The Software Model Checker Blast: Applications to software engineering.} ",
313   booktitle = " International Journal on Software Tools for Technology Transfer",
314   volume = {9 (5-6)},
315   pages = {505-525},
316   year = 2007,
317}
318
319
320@inproceedings{pwk2009-date,
321  AUTHOR    = { Mitra Purandare and Thomas Wahl and Daniel Kroening },
322  TITLE     = { Strengthening Properties using Abstraction Refinement },
323  BOOKTITLE = { Proceedings of DATE 2009 },
324  YEAR      = { 2009 },
325  PUBLISHER = { ACM },
326  PAGES     = { 1692--1697 },
327}
328
329
330@conference{ Kunz_al11ipc_abs,
331   author = " Minh D. Nguyen and Markus Wedler and Dominik Stoffel and Wolfgang Kunz ",
332   title = "{ Formal Hardware/Software Co-Verification by Interval Property Checking with Abstraction}",
333   booktitle = "48th Proc. Design Automation Conference (DAC '11)",
334   address = "San Diego, USA",
335   year = 2011,
336}
337
338
339@book{ knuth94tex,
340 author    = "Donald E. Knuth",
341 publisher = "Addison-Wesley",
342 title     = "The {\TeX}book",
343 year      =  1984,
344 isbn      = ""
345}
346
347
348@misc{ patanshnik88bibtex,
349 author    = "Oren Patashnik",
350 title     = "Using {BibTeX}. {D}ocumentation for general {B}ib{\TeX} users",
351 year      =  1988,
352 month     =  jan
353}
354
355
356@article{ etessami_yannakakis09recursive,
357    author = "Kousha Etassami and Mihalis Yannakakis",
358    title = "Recursive Markov chains, sto-chastic grammars, and monotone systems of nonlinear equations",
359    journal = {Journals of the ACM},
360    volume = 56,
361    number = 1,
362    pages = {1-66},
363    year = 2009
364}
Note: See TracBrowser for help on using the repository browser.