docs/papers/references.bib

   1 @article{visser:2003,
   2  author = {Visser, Willem and Havelund, Klaus and Brat, Guillaume and Park, Seungjoon and Lerda, Flavio},
   3  title = "{M}odel {C}hecking {P}rograms",
   4  journal = {Automated Software Engineering},
   5  volume = {10},
   6  number = {2},
   7  month = {April},
   8  year = {2003},
   9  pages = {203--232},
  10  publisher = {Kluwer Academic Publishers},
  11  url = "http://dl.acm.org/citation.cfm?id=641186"
  12  }
  13
  14 @inproceedings{lerda:2001,
  15  author = {Lerda, Flavio and Visser, Willem},
  16  title = {Addressing Dynamic Issues of Program Model Checking},
  17  booktitle = {Proceedings of the 8th International SPIN Workshop on Model Checking of Software},
  18  year = {2001},
  19  pages = {80--102},
  20  publisher = {Springer},
  21  url = "http://dl.acm.org/citation.cfm?id=380921.380931",
  22 }
  23
  24 @inproceedings{khurshid:2003,
  25     author = {Sarfraz Khurshid and Corina S. P\v{a}s\v{a}reanu and Willem Visser},
  26     title = {Generalized Symbolic Execution for Model Checking and Testing},
  27     booktitle = {Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  28     year = {2003},
  29     pages = {553--568},
  30     publisher = {Springer},
  31     url = "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.8862"
  32 }
  33
  34 @article{visser:2004,
  35  author = {Visser, Willem and P\v{a}s\v{a}reanu, Corina S. and Khurshid, Sarfraz},
  36  title = {Test Input Generation with Java PathFinder},
  37  journal = {Proceedings of International Symposium on Software Testing and Analysis},
  38  volume = {29},
  39  number = {4},
  40  month = jul,
  41  year = {2004},
  42  pages = {97--107},
  43  publisher = {ACM},
  44  url = "http://dl.acm.org/citation.cfm?id=1007526",
  45 }
  46
  47 @article{pasareanu:2004,
  48 year={2004},
  49 volume={2989},
  50 series={Lecture Notes in Computer Science},
  51 title={Verification of Java Programs Using Symbolic Execution and Invariant Generation},
  52 url={http://link.springer.com/chapter/10.1007%2F978-3-540-24732-6_13#},
  53 publisher={Springer},
  54 author={Păsăreanu, Corina S. and Visser, Willem},
  55 pages={164-181},
  56 }
  57
  58 @inproceedings{person:2008,
  59  author = {Person, Suzette and Dwyer, Matthew B. and Elbaum, Sebastian and P\v{a}s\v{a}reanu, Corina S.},
  60  title = {Differential Symbolic Execution},
  61  booktitle = {Proceedings of the 16th {ACM} {SIGSOFT} International Symposium on Foundations of Software Engineering},
  62  year = {2008},
  63  pages = {226--237},
  64  url = {http://doi.acm.org/10.1145/1453101.1453131},
  65  publisher = {ACM},
  66  }
  67
  68 @inproceedings{pasareanu:2008,
  69   author    = {Corina S. P\v{a}s\v{a}reanu and
  70                Peter C. Mehlitz and
  71                David H. Bushnell and
  72                Karen Gundy{-}Burlet and
  73                Michael R. Lowry and
  74                Suzette Person and
  75                Mark Pape},
  76   title     = {Combining unit-level symbolic execution and system-level concrete
  77                execution for testing {NASA} software},
  78   booktitle = {Proceedings of the {ACM} {SIGSOFT} International Symposium on Software
  79                Testing and Analysis},
  80   pages     = {15--26},
  81   year      = {2008},
  82   url       = {http://doi.acm.org/10.1145/1390630.1390635},
  83 }
  84
  85 @inproceedings{pasareanu:2007,
  86   author    = {Corina S. P\v{a}s\v{a}reanu and
  87                Willem Visser},
  88   title     = {Symbolic Execution and Model Checking for Testing},
  89   booktitle = {Hardware and Software: Verification and Testing, Third International
  90                Haifa Verification Conference},
  91   pages     = {17--18},
  92   year      = {2007},
  93   url       = {http://dx.doi.org/10.1007/978-3-540-77966-7_5},
  94 }
  95
  96 @inproceedings{artho:2003,
  97   author    = {Cyrille Artho and
  98                Doron Drusinsky and
  99                Allen Goldberg and
 100                Klaus Havelund and
 101                Michael R. Lowry and
 102                Corina S. P\v{a}s\v{a}reanu and
 103                Grigore Rosu and
 104                Willem Visser},
 105   title     = {Experiments with Test Case Generation and Runtime Analysis},
 106   booktitle = {Abstract State Machines, Advances in Theory and Practice},
 107   pages     = {87--107},
 108   year      = {2003},
 109   url       = {http://dx.doi.org/10.1007/3-540-36498-6_5},
 110 }
 111
 112 @article{groce:2004,
 113   author    = {Alex Groce and
 114                Willem Visser},
 115   title     = {Heuristics for model checking Java programs},
 116   journal   = {International Journal on Software Tools for Technology Transfer},
 117   volume    = {6},
 118   number    = {4},
 119   pages     = {260--276},
 120   year      = {2004},
 121   url       = {http://dx.doi.org/10.1007/s10009-003-0130-9},
 122 }
 123
 124 @inproceedings{groce:2002,
 125   author    = {Alex Groce and
 126                Willem Visser},
 127   title     = {Model checking Java programs using structural heuristics},
 128   booktitle = {Proceedings of International Symposium on Software Testing and Analysis},
 129   pages     = {12--21},
 130   year      = {2002},
 131   url       = {http://doi.acm.org/10.1145/566172.566175},
 132 }
 133
 134 @inproceedings{groce:visser:2002,
 135   author    = {Alex Groce and
 136                Willem Visser},
 137   title     = {Heuristic Model Checking for Java Programs},
 138   booktitle = {Proceedings of the 9th International SPIN Workshop on Model Checking of Software},
 139   pages     = {242--245},
 140   year      = {2002},
 141   url       = {http://dx.doi.org/10.1007/3-540-46017-9_21},
 142 }
 143
 144 @inproceedings{artho:2011,
 145  author = {Leungwattanakit, Watcharin and Artho, Cyrille and Hagiya, Masami and Tanabe, Yoshinori and Yamamoto, Mitsuharu},
 146  title = {Model checking distributed systems by combining caching and process checkpointing},
 147  booktitle = {Proceedings of the 26th IEEE/ACM International Conference on International Conference on Automated Software Engineering},
 148  year = {2011},
 149  pages = {103--112},
 150  publisher = {IEEE},
 151 month={November},
 152  address = {Lawrence, KS, USA},
 153  url  = {http://staff.aist.go.jp/c.artho/papers/checkpointing.pdf},
 154 }
 155
 156 @inproceedings{artho:2009,
 157  author = {Artho, Cyrille and Leungwattanakit, Watcharin and Hagiya, Masami and Tanabe, Yoshinori and Yamamoto, Mitsuharu},
 158  title = {Cache-Based model Checking of Networked Applications: From Linear to Branching Time},
 159  booktitle = {Proceedings of the 27th International Conference on Automated Software Engineering},
 160  year = {2009},
 161 month = {November},
 162  pages = {447--458},
 163  publisher = {IEEE},
 164  address = {Auckland, New Zealand},
 165  url = {http://staff.aist.go.jp/c.artho/papers/ase-2009.pdf},
 166 }
 167
 168 @inproceedings{artho:2008,
 169 author={Artho, Cyrille and Leungwattanakit, Watcharin and Hagiya, Masami and Tanabe, Yoshinori},
 170 title={Efficient Model Checking of Networked Applications},
 171 year={2008},
 172 volume={11},
 173 series={Lecture Notes in Business Information Processing},
 174 booktitle = {Proceedings of the 46th International Conference on Objects, Components, Models and Patterns},
 175 publisher={Springer},
 176 pages={22--40},
 177 address={Zurich, Switzerland},
 178 month={June/July},
 179 url = {http://staff.aist.go.jp/c.artho/papers/tools-2008.pdf}
 180 }
 181
 182 @inproceedings{grove:2003,
 183   author    = {Alex Groce and
 184                Willem Visser},
 185   title     = {What Went Wrong: Explaining Counterexamples},
 186   booktitle = {Proceedings of the 10th International SPIN Workshop on Model Checking of Software},
 187   pages     = {121--135},
 188   year      = {2003},
 189   url       = {http://dx.doi.org/10.1007/3-540-44829-2_8},
 190   publisher = {Springer},
 191   address = {Portland},
 192 }
 193
 194 @article{penix:2005,
 195   author    = {John Penix and
 196                Willem Visser and
 197                Seungjoon Park and
 198                Corina S. P\v{a}s\v{a}reanu and
 199                Eric Engstrom and
 200                Aaron Larson and
 201                Nicholas Weininger},
 202   title     = {Verifying Time Partitioning in the {DEOS} Scheduling Kernel},
 203   journal   = {Formal Methods in System Design},
 204   volume    = {26},
 205   number    = {2},
 206   pages     = {103--135},
 207   year      = {2005},
 208   url       = {http://dx.doi.org/10.1007/s10703-005-1490-4},
 209 }
 210
 211 @article{brat:2004,
 212   author    = {Guillaume P. Brat and
 213                Doron Drusinsky and
 214                Dimitra Giannakopoulou and
 215                Allen Goldberg and
 216                Klaus Havelund and
 217                Michael R. Lowry and
 218                Corina S. Pasareanu and
 219                Arnaud Venet and
 220                Willem Visser and
 221                Richard Washington},
 222   title     = {Experimental Evaluation of Verification and Validation Tools on Martian
 223                Rover Software},
 224   journal   = {Formal Methods in System Design},
 225   volume    = {25},
 226   number    = {2-3},
 227   pages     = {167--198},
 228   year      = {2004},
 229   url       = {http://dx.doi.org/10.1023/B:FORM.0000040027.28662.a4},
 230 }
 231
 232 @inproceedings{bordini:2003,
 233   author    = {Rafael H. Bordini and
 234                Michael Fisher and
 235                Carmen Pardavila and
 236                Willem Visser and
 237                Michael Wooldridge},
 238   title     = {Model Checking Multi-Agent Programs with {CASP}},
 239   booktitle = {Proceedings of Computer Aided Verification},
 240   pages     = {110--113},
 241   year      = {2003},
 242   url       = {http://dx.doi.org/10.1007/978-3-540-45069-6_10},
 243 }
 244
 245 @inproceedings{giannakopoulou:2004,
 246   author    = {Dimitra Giannakopoulou and
 247                Corina S. Pasareanu and
 248                Jamieson M. Cobleigh},
 249   title     = {Assume-Guarantee Verification of Source Code with Design-Level Assumptions},
 250   booktitle = {26th International Conference on Software Engineering {(ICSE} 2004),
 251                23-28 May 2004, Edinburgh, United Kingdom},
 252   pages     = {211--220},
 253   year      = {2004},
 254   url       = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2004.1317443},
 255 }
 256
 257 @inproceedings{mehlitz:2008,
 258   author    = {Peter Mehlitz},
 259   title     = {Trust Your Model - Verifying Aerospace System Models with Java Pathfinder},
 260   booktitle = {Aerospace Conference, 2008 IEEE},
 261   pages     = {1--11},
 262   year      = {2008},
 263   url       = {http://ti.arc.nasa.gov/m/pub-archive/1402/1402%20(Mehlitz).pdf},
 264 }
 265
 266 @inproceedings{stergiopoulos:2012,
 267  author = {Stergiopoulos, George and Tsoumas, Bill and Gritzalis, Dimitris},
 268  title = {Hunting Application-level Logical Errors},
 269  booktitle = {Proceedings of the 4th International Conference on Engineering Secure Software and Systems},
 270  year = {2012},
 271  address = {Eindhoven, The Netherlands},
 272  pages = {135--142},
 273  url = {http://dx.doi.org/10.1007/978-3-642-28166-2_13},
 274  publisher = {Springer},
 275 }
 276
 277 @article{mansouri:2007,
 278  author = {Masoud Mansouri-Samani and John Penix and Lawrence Markosian},
 279  title = {Assume-Guarantee Verification of Source Code with Design-Level Assumptions},
 280  journal = {Software Assurance Research Program (SARP), NASA IV&V publication},
 281  year = {2007},
 282  pages = {203--232},
 283  publisher = {Kluwer Academic Publishers},
 284  url = {http://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20080015887.pdf},
 285  }
 286
 287  @article{havelund:2002,
 288   author    = {Klaus Havelund and Willem Visser},
 289   title     = {Program Model Checking as a New Trend},
 290   journal = {International Journal on Software Tools for Technology Transfer (STTT)},
 291   volume = {4},
 292   number = {1},
 293   month = {October},
 294   year = {2002},
 295   url = {http://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20030003734.pdf},
 296 }
 297
 298 @article{pasareanu:dwyer:2003,
 299   author  = "C. P\v{a}s\v{a}reanu and M. Dwyer and W. Visser.",
 300   title   = "{Finding Feasible Abstract Counter-Examples}",
 301   journal = "International Journal on Software Tools for Technology Transfer (STTT)",
 302   year    = "2003",
 303   volume  = "5",
 304   number  = "1",
 305   month   = "November",
 306   url = "http://ti.arc.nasa.gov/m/profile/pcorina/papers/tacas_sttt01.ps"
 307 }
 308
 309 @inproceedings{brat:2001,
 310  author = {Guillaume Brat and Willem Visser},
 311  title = {Combining Static Analysis and Model Checking for Software Analysis},
 312  booktitle = {Proceedings of the 15th IEEE International Conference on Automated Software Engineering},
 313  year = {2001},
 314  address = {San Diego, USA},
 315  month = {November},
 316  url = {http://dl.acm.org/citation.cfm?id=872568},
 317 }
 318
 319 @inproceedings{visser:park:2000,
 320     author = {Willem Visser and Seungjoon Park and John Penix},
 321     title = {Using Predicate Abstraction to Reduce Object-Oriented Programs for Model Checking},
 322     booktitle = {Proceedings of the 3rd ACM SIGSOFT Workshop on Formal Methods in Software Practice},
 323     year = {2000},
 324     pages = {3--12},
 325     month = {August},
 326     url = "http://ti.arc.nasa.gov/m/tech/rse/publications/papers/SIGSOFT00/fmsp00.pdf",
 327 }
 328
 329 @article{havelund:2000,
 330   author    = {Klaus Havelund and
 331                Thomas Pressburger},
 332   title     = {Model Checking {Java} Programs using {Java} PathFinder},
 333   journal   = {International Journal on Software Tools for Technology Transfer (STTT)},
 334   volume    = {2},
 335   number    = {4},
 336   pages     = {366--381},
 337   year      = {2000},
 338   url       = {http://www.havelund.com/Publications/jpf-sttt.ps.Z},
 339 }
 340
 341 @inproceedings{havelund:1999,
 342   author    = {Klaus Havelund},
 343   title     = {Java PathFinder, {A} Translator from Java to Promela},
 344   booktitle = {Theoretical and Practical Aspects of {SPIN} Model Checking},
 345   month     = {July},
 346   year      = {1999},
 347   url       = {http://www.havelund.com/Publications/jpf1-spin-99.pdf},
 348 }
 349
 350 @inproceedings{havelund:skakkebaek:1999,
 351   author    = {Klaus Havelund and
 352                Jens U. Skakkeb{\ae}k},
 353   title     = {Applying Model Checking in Java Verification},
 354   booktitle = {Theoretical and Practical Aspects of {SPIN} Model Checking, 5th and
 355                6th International {SPIN} Workshops},
 356   pages     = {216--231},
 357   year      = {1999},
 358   url       = {http://www.havelund.com/Publications/jpf-fm99.ps.Z},
 359 }
 360
 361 @article{havelund:2007,
 362   author    = {Klaus Havelund},
 363   title     = {Java PathFinder User Guide},
 364   booktitle = {Unpublished Report},
 365   year = {1999},
 366   url = {http://www.havelund.com/Publications/jpf-manual.ps.Z},
 367 }
 368
 369 @article{havelund:Pressburger:1998,
 370   author    = {Klaus Havelund and Thomas Pressburger},
 371   title     = {Java PathFinder, A Translator from Java to Promela},
 372   booktitle = {Unpublished Report},
 373   year = {1998},
 374   url = {http://www.havelund.com/Publications/jpf1-report-99.pdf},
 375 }
 376
 377 @inproceedings{gligoric:2010,
 378   author    = {Milos Gligoric and
 379                Tihomir Gvero and
 380                Vilas Jagannath and
 381                Sarfraz Khurshid and
 382                Viktor Kuncak and
 383                Darko Marinov},
 384   title     = {Test generation through programming in {UDITA}},
 385   booktitle = {Proceedings of the 32nd {ACM/IEEE} International Conference on Software
 386                Engineering},
 387   address   = {Cape Town, South Africa},
 388   month     = {May},
 389   pages     = {225--234},
 390   year      = {2010},
 391   url       = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL10UDITA.pdf},
 392 }
 393
 394 @inproceedings{gligoric:jagannath:2010,
 395   author    = {Milos Gligoric and
 396                Vilas Jagannath and
 397                Darko Marinov},
 398   title     = {MuTMuT: Efficient Exploration for Mutation Testing of Multithreaded
 399                Code},
 400   booktitle = {Third International Conference on Software Testing, Verification and
 401                Validation},
 402   pages     = {55--64},
 403   month     = {April},
 404   address   = {Paris, France},
 405   year      = {2010},
 406   url       = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL10MuTMuT.pdf},
 407 }
 408
 409 @inproceedings{lauterburg:2010,
 410   author    = {Steven Lauterburg and
 411                Rajesh K. Karmani and
 412                Darko Marinov and
 413                Gul Agha},
 414   title     = {Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction
 415                Techniques},
 416   booktitle = {Fundamental Approaches to Software Engineering},
 417   address   = {Paphos, Cyprus},
 418   month     = {March},
 419   pages     = {308--322},
 420   year      = {2010},
 421   url       = {http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL10DPORHeuristics.pdf},
 422 }
 423
 424 @inproceedings{lauterburg:2009,
 425   author    = {Steven Lauterburg and
 426                Mirco Dotta and
 427                Darko Marinov and
 428                Gul A. Agha},
 429   title     = {A Framework for State-Space Exploration of Java-Based Actor Programs},
 430   booktitle = {24th {IEEE/ACM} International Conference on Automated Software Engineering},
 431   month     = {November},
 432   address   = {Auckland, New Zealand},
 433   pages     = {468--479},
 434   year      = {2009},
 435   url       = {http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL09Basset.pdf},
 436 }
 437
 438 @article{sobeih:2010,
 439   author    = {Ahmed Sobeih and
 440                Marcelo d'Amorim and
 441                Mahesh Viswanathan and
 442                Darko Marinov and
 443                Jennifer C. Hou},
 444   title     = {Assertion Checking in J-Sim Simulation Models of Network Protocols},
 445   journal   = {Simulation: Transactions of The Society for Modeling and Simulation International},
 446   volume    = {86},
 447   number    = {11},
 448   pages     = {651--673},
 449   year      = {2010},
 450   url       = {http://dx.doi.org/10.1177/0037549709349326},
 451 }
 452
 453 @inproceedings{gligoric:2009,
 454   author    = {Milos Gligoric and
 455                Tihomir Gvero and
 456                Steven Lauterburg and
 457                Darko Marinov and
 458                Sarfraz Khurshid},
 459   title     = {Optimizing Generation of Object Graphs in Java PathFinder},
 460   booktitle = {Second International Conference on Software Testing Verification and Validation},
 461   month     = {April},
 462   address   = {Denver, Colorado, {USA}},
 463   pages     = {51--60},
 464   year      = {2009},
 465   url       = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL09OptimizingGeneration.pdf},
 466 }
 467
 468 @article{damorim:2008,
 469   author    = {Marcelo d'Amorim and
 470                Steven Lauterburg and
 471                Darko Marinov},
 472   title     = {Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs},
 473   journal   = {{IEEE} Transactions on Software Engineering},
 474   volume    = {34},
 475   number    = {5},
 476   pages     = {597--613},
 477   year      = {2008},
 478   month     = {September/October},
 479   url       = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL08DeltaExecution.pdf},
 480 }
 481
 482 @inproceedings{lauterburg:2008,
 483   author    = {Steven Lauterburg and
 484                Ahmed Sobeih and
 485                Darko Marinov and
 486                Mahesh Viswanathan},
 487   title     = {Incremental state-space exploration for programs with dynamically
 488                allocated data},
 489   booktitle = {International Conference on Software Engineering},
 490   address   = {Leipzig, Germany},
 491   month     = {May},
 492   pages     = {291--300},
 493   year      = {2008},
 494   url       = {http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL08IncrementalChecking.pdf},
 495 }
 496
 497 @inproceedings{gvero:2008,
 498   author    = {Tihomir Gvero and
 499                Milos Gligoric and
 500                Steven Lauterburg and
 501                Marcelo d'Amorim and
 502                Darko Marinov and
 503                Sarfraz Khurshid},
 504   title     = {State extensions for java pathfinder},
 505   booktitle = {International Conference on Software Engineering, Demo Papers},
 506   address   = {Leipzig, Germany},
 507   month     = {May},
 508   pages     = {863--866},
 509   year      = {2008},
 510   url       = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL09OptimizingGeneration.pdf},
 511 }
 512
 513 @inproceedings{damorim:2007,
 514   author    = {Marcelo d'Amorim and
 515                Steven Lauterburg and
 516                Darko Marinov},
 517   title     = {Delta execution for efficient state-space exploration of object-oriented
 518                programs},
 519   booktitle = {Proceedings of the {ACM/SIGSOFT} International Symposium on Software
 520                Testing and Analysis},
 521   address   = {London, UK},
 522   month     = {July},
 523   pages     = {50--60},
 524   year      = {2007},
 525   url       = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL07DeltaExecution.pdf},
 526 }
 527
 528 @inproceedings{zhou:2007,
 529  author = {Zhou, Yuanyuan and Marinov, Darko and Sanders, William and Zilles, Craig and d'Amorim, Marcelo and Lauterburg, Steven and Lefever, Ryan M. and Tucek, Joe},
 530  title = {Delta Execution for Software Reliability},
 531  booktitle = {Proceedings of the 3rd Workshop on on Hot Topics in System Dependability},
 532  series = {HotDep'07},
 533  year = {2007},
 534  address = {Edinburgh, UK},
 535  url = {http://mir.cs.illinois.edu/~marinov/publications/ZhouETAL07DeltaExecution.pdf},
 536  publisher = {USENIX Association},
 537 }
 538
 539 @inproceedings{damorim:2006,
 540   author    = {Marcelo d'Amorim and
 541                Ahmed Sobeih and
 542                Darko Marinov},
 543   title     = {Optimized Execution of Deterministic Blocks in Java PathFinder},
 544   booktitle = {Proceedings of Formal Methods and Software Engineering, 8th International Conference
 545                on Formal Engineering Methods},
 546   address   = {Macao, China},
 547   month     =  {November},
 548   pages     = {549--567},
 549   year      = {2006},
 550   url       = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL06OptimizedDeterministicBlocks.pdf},
 551 }
 552
 553 @inproceedings{damorim:pacheco:2006,
 554   author    = {Marcelo d'Amorim and
 555                Carlos Pacheco and
 556                Tao Xie and
 557                Darko Marinov and
 558                Michael D. Ernst},
 559   title     = {An Empirical Comparison of Automated Generation and Classification
 560                Techniques for Object-Oriented Unit Testing},
 561   booktitle = {Proceedings of 21st {IEEE/ACM} International Conference on Automated Software Engineering},
 562   address   = {Tokyo, Japan},
 563   month     = {September},
 564   pages     = {59--68},
 565   year      = {2006},
 566   url       = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL06Symclat.pdf},
 567 }
 568
 569 @unpublished{kulikov:2010,
 570   author = {Sergey Kulikov and Nastaran Shafiei and Franck van Breugel and Willem Visser},
 571   title = {{Detecting Data Races with Java PathFinder}},
 572   year = "2010",
 573   url = {http://www.cse.yorku.ca/~franck/research/drafts/race.pdf}
 574 }
 575
 576 @inproceedings{indradeep:2013,
 577   author = {Ghosh, Indradeep and Shafiei, Nastaran and Li, Guodong and Chiang, Wei-Fan},
 578   title = {{JST: an automatic test generation tool for industrial Java applications with strings}},
 579   booktitle = {Proceedings of the 35th International Conference on Software Engineering},
 580   year = {2013},
 581   month = {May},
 582   address = {San Francisco, CA, USA},
 583   pages = {992--1001},
 584   publisher = {IEEE},
 585   url = {http://dl.acm.org/citation.cfm?id=2486925}
 586 }
 587
 588 @article{nshafiei:2012,
 589   author = {Shafiei, Nastaran and Mehlitz, Peter C.},
 590   journal = {ACM SIGSOFT Software Engineering Notes},
 591   number = 6,
 592   pages = {1-5},
 593   title = {{Modeling class loaders in Java PathFinder version 7}},
 594   volume = 37,
 595   year = 2012,
 596   month = {November},
 597   url = {http://dl.acm.org/citation.cfm?id=2382800}
 598 }
 599
 600 @article{shafiei:2014,
 601   author = {Shafiei, Nastaran and Mehlitz, Peter C.},
 602   journal = {ACM SIGSOFT Software Engineering Notes},
 603   number = 1,
 604   pages = {1-5},
 605   title = {{Extending JPF to verify distributed systems}},
 606   volume = 39,
 607   year = 2014,
 608   month = {January},
 609   url = {http://dl.acm.org/citation.cfm?id=2560577},
 610 }
 611
 612 @inproceedings{shafiei:2013,
 613   author    = {Nastaran Shafiei and
 614                Franck van Breugel},
 615   title     = {Towards model checking of computer games with Java PathFinder},
 616   booktitle = {Proceedings of the 3rd International Workshop on Games and Software
 617                Engineering},
 618   address   = {San Francisco, CA, USA},
 619   month     = {May},
 620   pages     = {15--21},
 621   year      = {2013},
 622   url       = {http://dl.acm.org/citation.cfm?id=2662596},
 623 }
 624
 625
 626 @inproceedings{shafiei:breugel:2014,
 627   author    = {Nastaran Shafiei and
 628                Franck van Breugel},
 629   title     = {Automatic handling of native methods in Java PathFinder},
 630   booktitle = {Proceedings of the International SPIN Workshop on Model Checking of Software},
 631   address   = {San Jose, CA, USA},
 632   month     = {July},
 633   pages     = {97--100},
 634   year      = {2014},
 635   url       = {http://dl.acm.org/citation.cfm?id=2632363},
 636 }