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