source: papers/FDL2012/myBib.bib @ 104

Last change on this file since 104 was 101, checked in by syed, 12 years ago

final

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