Renaming /doc to /docs for use with GitHub Pages
[jpf-core.git] / docs / papers / references.bib
diff --git a/docs/papers/references.bib b/docs/papers/references.bib
new file mode 100644 (file)
index 0000000..698195f
--- /dev/null
@@ -0,0 +1,636 @@
+@article{visser:2003,
+ author = {Visser, Willem and Havelund, Klaus and Brat, Guillaume and Park, Seungjoon and Lerda, Flavio},
+ title = "{M}odel {C}hecking {P}rograms",
+ journal = {Automated Software Engineering},
+ volume = {10},
+ number = {2},
+ month = {April},
+ year = {2003}, 
+ pages = {203--232},
+ publisher = {Kluwer Academic Publishers}, 
+ url = "http://dl.acm.org/citation.cfm?id=641186"
+ }
+
+@inproceedings{lerda:2001,
+ author = {Lerda, Flavio and Visser, Willem},
+ title = {Addressing Dynamic Issues of Program Model Checking},
+ booktitle = {Proceedings of the 8th International SPIN Workshop on Model Checking of Software},
+ year = {2001},
+ pages = {80--102},
+ publisher = {Springer},
+ url = "http://dl.acm.org/citation.cfm?id=380921.380931",
+} 
+
+@inproceedings{khurshid:2003,
+    author = {Sarfraz Khurshid and Corina S. P\v{a}s\v{a}reanu and Willem Visser},
+    title = {Generalized Symbolic Execution for Model Checking and Testing},
+    booktitle = {Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
+    year = {2003},
+    pages = {553--568},
+    publisher = {Springer},
+    url = "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.8862"
+}
+
+@article{visser:2004,
+ author = {Visser, Willem and P\v{a}s\v{a}reanu, Corina S. and Khurshid, Sarfraz},
+ title = {Test Input Generation with Java PathFinder},
+ journal = {Proceedings of International Symposium on Software Testing and Analysis},
+ volume = {29},
+ number = {4},
+ month = jul,
+ year = {2004},
+ pages = {97--107},
+ publisher = {ACM},
+ url = "http://dl.acm.org/citation.cfm?id=1007526",
+} 
+
+@article{pasareanu:2004,
+year={2004},
+volume={2989},
+series={Lecture Notes in Computer Science},
+title={Verification of Java Programs Using Symbolic Execution and Invariant Generation},
+url={http://link.springer.com/chapter/10.1007%2F978-3-540-24732-6_13#},
+publisher={Springer},
+author={Păsăreanu, Corina S. and Visser, Willem},
+pages={164-181},
+}
+
+@inproceedings{person:2008,
+ author = {Person, Suzette and Dwyer, Matthew B. and Elbaum, Sebastian and P\v{a}s\v{a}reanu, Corina S.},
+ title = {Differential Symbolic Execution},
+ booktitle = {Proceedings of the 16th {ACM} {SIGSOFT} International Symposium on Foundations of Software Engineering},
+ year = {2008},
+ pages = {226--237},
+ url = {http://doi.acm.org/10.1145/1453101.1453131},
+ publisher = {ACM},
+ }
+@inproceedings{pasareanu:2008,
+  author    = {Corina S. P\v{a}s\v{a}reanu and
+               Peter C. Mehlitz and
+               David H. Bushnell and
+               Karen Gundy{-}Burlet and
+               Michael R. Lowry and
+               Suzette Person and
+               Mark Pape},
+  title     = {Combining unit-level symbolic execution and system-level concrete
+               execution for testing {NASA} software},
+  booktitle = {Proceedings of the {ACM} {SIGSOFT} International Symposium on Software
+               Testing and Analysis},
+  pages     = {15--26},
+  year      = {2008},
+  url       = {http://doi.acm.org/10.1145/1390630.1390635},
+}
+
+@inproceedings{pasareanu:2007,
+  author    = {Corina S. P\v{a}s\v{a}reanu and
+               Willem Visser},
+  title     = {Symbolic Execution and Model Checking for Testing},
+  booktitle = {Hardware and Software: Verification and Testing, Third International
+               Haifa Verification Conference},
+  pages     = {17--18},
+  year      = {2007},
+  url       = {http://dx.doi.org/10.1007/978-3-540-77966-7_5},
+}
+
+@inproceedings{artho:2003,
+  author    = {Cyrille Artho and
+               Doron Drusinsky and
+               Allen Goldberg and
+               Klaus Havelund and
+               Michael R. Lowry and
+               Corina S. P\v{a}s\v{a}reanu and
+               Grigore Rosu and
+               Willem Visser},
+  title     = {Experiments with Test Case Generation and Runtime Analysis},
+  booktitle = {Abstract State Machines, Advances in Theory and Practice},
+  pages     = {87--107},
+  year      = {2003},
+  url       = {http://dx.doi.org/10.1007/3-540-36498-6_5},
+}
+
+@article{groce:2004,
+  author    = {Alex Groce and
+               Willem Visser},
+  title     = {Heuristics for model checking Java programs},
+  journal   = {International Journal on Software Tools for Technology Transfer},
+  volume    = {6},
+  number    = {4},
+  pages     = {260--276},
+  year      = {2004},
+  url       = {http://dx.doi.org/10.1007/s10009-003-0130-9},
+}
+
+@inproceedings{groce:2002,
+  author    = {Alex Groce and
+               Willem Visser},
+  title     = {Model checking Java programs using structural heuristics},
+  booktitle = {Proceedings of International Symposium on Software Testing and Analysis},
+  pages     = {12--21},
+  year      = {2002},
+  url       = {http://doi.acm.org/10.1145/566172.566175},
+}
+
+@inproceedings{groce:visser:2002,
+  author    = {Alex Groce and
+               Willem Visser},
+  title     = {Heuristic Model Checking for Java Programs},
+  booktitle = {Proceedings of the 9th International SPIN Workshop on Model Checking of Software},
+  pages     = {242--245},
+  year      = {2002},
+  url       = {http://dx.doi.org/10.1007/3-540-46017-9_21},
+}
+
+@inproceedings{artho:2011,
+ author = {Leungwattanakit, Watcharin and Artho, Cyrille and Hagiya, Masami and Tanabe, Yoshinori and Yamamoto, Mitsuharu},
+ title = {Model checking distributed systems by combining caching and process checkpointing},
+ booktitle = {Proceedings of the 26th IEEE/ACM International Conference on International Conference on Automated Software Engineering},
+ year = {2011},
+ pages = {103--112},
+ publisher = {IEEE},
+month={November},
+ address = {Lawrence, KS, USA},
+ url  = {​http://staff.aist.go.jp/c.artho/papers/checkpointing.pdf},
+} 
+
+@inproceedings{artho:2009,
+ author = {Artho, Cyrille and Leungwattanakit, Watcharin and Hagiya, Masami and Tanabe, Yoshinori and Yamamoto, Mitsuharu},
+ title = {Cache-Based model Checking of Networked Applications: From Linear to Branching Time},
+ booktitle = {Proceedings of the 27th International Conference on Automated Software Engineering},
+ year = {2009},
+month = {November},
+ pages = {447--458},
+ publisher = {IEEE},
+ address = {Auckland, New Zealand},
+ url = {​http://staff.aist.go.jp/c.artho/papers/ase-2009.pdf},
+}
+
+@inproceedings{artho:2008,
+author={Artho, Cyrille and Leungwattanakit, Watcharin and Hagiya, Masami and Tanabe, Yoshinori},
+title={Efficient Model Checking of Networked Applications},
+year={2008},
+volume={11},
+series={Lecture Notes in Business Information Processing},
+booktitle = {Proceedings of the 46th International Conference on Objects, Components, Models and Patterns},
+publisher={Springer},
+pages={22--40},
+address={Zurich, Switzerland},
+month={June/July},
+url = {http://staff.aist.go.jp/c.artho/papers/tools-2008.pdf}
+}
+
+@inproceedings{grove:2003,
+  author    = {Alex Groce and
+               Willem Visser},
+  title     = {What Went Wrong: Explaining Counterexamples},
+  booktitle = {Proceedings of the 10th International SPIN Workshop on Model Checking of Software},
+  pages     = {121--135},
+  year      = {2003},
+  url       = {http://dx.doi.org/10.1007/3-540-44829-2_8},
+  publisher = {Springer},
+  address = {Portland},
+}
+
+@article{penix:2005,
+  author    = {John Penix and
+               Willem Visser and
+               Seungjoon Park and
+               Corina S. P\v{a}s\v{a}reanu and
+               Eric Engstrom and
+               Aaron Larson and
+               Nicholas Weininger},
+  title     = {Verifying Time Partitioning in the {DEOS} Scheduling Kernel},
+  journal   = {Formal Methods in System Design},
+  volume    = {26},
+  number    = {2},
+  pages     = {103--135},
+  year      = {2005},
+  url       = {http://dx.doi.org/10.1007/s10703-005-1490-4},
+}
+
+@article{brat:2004,
+  author    = {Guillaume P. Brat and
+               Doron Drusinsky and
+               Dimitra Giannakopoulou and
+               Allen Goldberg and
+               Klaus Havelund and
+               Michael R. Lowry and
+               Corina S. Pasareanu and
+               Arnaud Venet and
+               Willem Visser and
+               Richard Washington},
+  title     = {Experimental Evaluation of Verification and Validation Tools on Martian
+               Rover Software},
+  journal   = {Formal Methods in System Design},
+  volume    = {25},
+  number    = {2-3},
+  pages     = {167--198},
+  year      = {2004},
+  url       = {http://dx.doi.org/10.1023/B:FORM.0000040027.28662.a4},
+}
+
+@inproceedings{bordini:2003,
+  author    = {Rafael H. Bordini and
+               Michael Fisher and
+               Carmen Pardavila and
+               Willem Visser and
+               Michael Wooldridge},
+  title     = {Model Checking Multi-Agent Programs with {CASP}},
+  booktitle = {Proceedings of Computer Aided Verification},
+  pages     = {110--113},
+  year      = {2003},
+  url       = {http://dx.doi.org/10.1007/978-3-540-45069-6_10},
+}
+
+@inproceedings{giannakopoulou:2004,
+  author    = {Dimitra Giannakopoulou and
+               Corina S. Pasareanu and
+               Jamieson M. Cobleigh},
+  title     = {Assume-Guarantee Verification of Source Code with Design-Level Assumptions},
+  booktitle = {26th International Conference on Software Engineering {(ICSE} 2004),
+               23-28 May 2004, Edinburgh, United Kingdom},
+  pages     = {211--220},
+  year      = {2004},
+  url       = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2004.1317443},
+}
+
+@inproceedings{mehlitz:2008,
+  author    = {Peter Mehlitz},
+  title     = {Trust Your Model - Verifying Aerospace System Models with Java Pathfinder},
+  booktitle = {Aerospace Conference, 2008 IEEE},
+  pages     = {1--11},
+  year      = {2008},
+  url       = {http://ti.arc.nasa.gov/m/pub-archive/1402/1402%20(Mehlitz).pdf},
+}
+
+@inproceedings{stergiopoulos:2012,
+ author = {Stergiopoulos, George and Tsoumas, Bill and Gritzalis, Dimitris},
+ title = {Hunting Application-level Logical Errors},
+ booktitle = {Proceedings of the 4th International Conference on Engineering Secure Software and Systems},
+ year = {2012},
+ address = {Eindhoven, The Netherlands},
+ pages = {135--142},
+ url = {http://dx.doi.org/10.1007/978-3-642-28166-2_13},
+ publisher = {Springer},
+}
+
+@article{mansouri:2007,
+ author = {Masoud Mansouri-Samani and John Penix and Lawrence Markosian},
+ title = {Assume-Guarantee Verification of Source Code with Design-Level Assumptions},
+ journal = {Software Assurance Research Program (SARP), NASA IV&V publication},
+ year = {2007},
+ pages = {203--232},
+ publisher = {Kluwer Academic Publishers}, 
+ url = {http://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20080015887.pdf},    
+ }
+ @article{havelund:2002,
+  author    = {Klaus Havelund and Willem Visser},
+  title     = {Program Model Checking as a New Trend},
+  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
+  volume = {4},
+  number = {1},
+  month = {October},
+  year = {2002},
+  url = {http://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20030003734.pdf},
+}
+
+@article{pasareanu:dwyer:2003,
+  author  = "C. P\v{a}s\v{a}reanu and M. Dwyer and W. Visser.",
+  title   = "{Finding Feasible Abstract Counter-Examples}",
+  journal = "International Journal on Software Tools for Technology Transfer (STTT)",
+  year    = "2003",
+  volume  = "5",
+  number  = "1",
+  month   = "November",
+  url = "http://ti.arc.nasa.gov/m/profile/pcorina/papers/tacas_sttt01.ps"
+}
+
+@inproceedings{brat:2001,
+ author = {Guillaume Brat and Willem Visser},
+ title = {Combining Static Analysis and Model Checking for Software Analysis},
+ booktitle = {Proceedings of the 15th IEEE International Conference on Automated Software Engineering},
+ year = {2001},
+ address = {San Diego, USA},
+ month = {November},
+ url = {http://dl.acm.org/citation.cfm?id=872568},
+}
+
+@inproceedings{visser:park:2000,
+    author = {Willem Visser and Seungjoon Park and John Penix},
+    title = {Using Predicate Abstraction to Reduce Object-Oriented Programs for Model Checking},
+    booktitle = {Proceedings of the 3rd ACM SIGSOFT Workshop on Formal Methods in Software Practice},
+    year = {2000},
+    pages = {3--12},
+    month = {August},
+    url = "http://ti.arc.nasa.gov/m/tech/rse/publications/papers/SIGSOFT00/fmsp00.pdf",
+}
+
+@article{havelund:2000,
+  author    = {Klaus Havelund and
+               Thomas Pressburger},
+  title     = {Model Checking {Java} Programs using {Java} PathFinder},
+  journal   = {International Journal on Software Tools for Technology Transfer (STTT)},
+  volume    = {2},
+  number    = {4},
+  pages     = {366--381},
+  year      = {2000},
+  url       = {http://www.havelund.com/Publications/jpf-sttt.ps.Z},
+}
+
+@inproceedings{havelund:1999,
+  author    = {Klaus Havelund},
+  title     = {Java PathFinder, {A} Translator from Java to Promela},
+  booktitle = {Theoretical and Practical Aspects of {SPIN} Model Checking},
+  month     = {July},
+  year      = {1999}, 
+  url       = {http://www.havelund.com/Publications/jpf1-spin-99.pdf},
+}
+
+@inproceedings{havelund:skakkebaek:1999,
+  author    = {Klaus Havelund and
+               Jens U. Skakkeb{\ae}k},
+  title     = {Applying Model Checking in Java Verification},
+  booktitle = {Theoretical and Practical Aspects of {SPIN} Model Checking, 5th and
+               6th International {SPIN} Workshops},
+  pages     = {216--231},
+  year      = {1999},
+  url       = {http://www.havelund.com/Publications/jpf-fm99.ps.Z},
+}
+
+@article{havelund:2007,
+  author    = {Klaus Havelund},
+  title     = {Java PathFinder User Guide},
+  booktitle = {Unpublished Report},
+  year = {1999},
+  url = {​http://www.havelund.com/Publications/jpf-manual.ps.Z},
+}
+
+@article{havelund:Pressburger:1998,
+  author    = {Klaus Havelund and Thomas Pressburger},
+  title     = {Java PathFinder, A Translator from Java to Promela},
+  booktitle = {Unpublished Report},
+  year = {1998},
+  url = {​​http://www.havelund.com/Publications/jpf1-report-99.pdf},
+}
+
+@inproceedings{gligoric:2010,
+  author    = {Milos Gligoric and
+               Tihomir Gvero and
+               Vilas Jagannath and
+               Sarfraz Khurshid and
+               Viktor Kuncak and
+               Darko Marinov},
+  title     = {Test generation through programming in {UDITA}},
+  booktitle = {Proceedings of the 32nd {ACM/IEEE} International Conference on Software
+               Engineering},
+  address   = {Cape Town, South Africa},
+  month     = {May},
+  pages     = {225--234},
+  year      = {2010},
+  url       = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL10UDITA.pdf},
+}
+
+@inproceedings{gligoric:jagannath:2010,
+  author    = {Milos Gligoric and
+               Vilas Jagannath and
+               Darko Marinov},
+  title     = {MuTMuT: Efficient Exploration for Mutation Testing of Multithreaded
+               Code},
+  booktitle = {Third International Conference on Software Testing, Verification and
+               Validation},
+  pages     = {55--64},
+  month     = {April},
+  address   = {Paris, France},
+  year      = {2010},
+  url       = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL10MuTMuT.pdf},
+}
+
+@inproceedings{lauterburg:2010,
+  author    = {Steven Lauterburg and
+               Rajesh K. Karmani and
+               Darko Marinov and
+               Gul Agha},
+  title     = {Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction
+               Techniques},
+  booktitle = {Fundamental Approaches to Software Engineering},
+  address   = {Paphos, Cyprus},
+  month     = {March},
+  pages     = {308--322},
+  year      = {2010},
+  url       = {http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL10DPORHeuristics.pdf},
+}
+
+@inproceedings{lauterburg:2009,
+  author    = {Steven Lauterburg and
+               Mirco Dotta and
+               Darko Marinov and
+               Gul A. Agha},
+  title     = {A Framework for State-Space Exploration of Java-Based Actor Programs},
+  booktitle = {24th {IEEE/ACM} International Conference on Automated Software Engineering},
+  month     = {November},
+  address   = {Auckland, New Zealand},
+  pages     = {468--479},
+  year      = {2009},
+  url       = {http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL09Basset.pdf},
+}
+
+@article{sobeih:2010,
+  author    = {Ahmed Sobeih and
+               Marcelo d'Amorim and
+               Mahesh Viswanathan and
+               Darko Marinov and
+               Jennifer C. Hou},
+  title     = {Assertion Checking in J-Sim Simulation Models of Network Protocols},
+  journal   = {Simulation: Transactions of The Society for Modeling and Simulation International},
+  volume    = {86},
+  number    = {11},
+  pages     = {651--673},
+  year      = {2010},
+  url       = {http://dx.doi.org/10.1177/0037549709349326},
+}
+
+@inproceedings{gligoric:2009,
+  author    = {Milos Gligoric and
+               Tihomir Gvero and
+               Steven Lauterburg and
+               Darko Marinov and
+               Sarfraz Khurshid},
+  title     = {Optimizing Generation of Object Graphs in Java PathFinder},
+  booktitle = {Second International Conference on Software Testing Verification and Validation},
+  month     = {April},
+  address   = {Denver, Colorado, {USA}},
+  pages     = {51--60},
+  year      = {2009},
+  url       = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL09OptimizingGeneration.pdf},
+}
+
+@article{damorim:2008,
+  author    = {Marcelo d'Amorim and
+               Steven Lauterburg and
+               Darko Marinov},
+  title     = {Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs},
+  journal   = {{IEEE} Transactions on Software Engineering},
+  volume    = {34},
+  number    = {5},
+  pages     = {597--613},
+  year      = {2008},
+  month     = {September/October},
+  url       = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL08DeltaExecution.pdf},
+}
+
+@inproceedings{lauterburg:2008,
+  author    = {Steven Lauterburg and
+               Ahmed Sobeih and
+               Darko Marinov and
+               Mahesh Viswanathan},
+  title     = {Incremental state-space exploration for programs with dynamically
+               allocated data},
+  booktitle = {International Conference on Software Engineering},
+  address   = {Leipzig, Germany},
+  month     = {May},
+  pages     = {291--300},
+  year      = {2008},
+  url       = {​http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL08IncrementalChecking.pdf},
+}
+
+@inproceedings{gvero:2008,
+  author    = {Tihomir Gvero and
+               Milos Gligoric and
+               Steven Lauterburg and
+               Marcelo d'Amorim and
+               Darko Marinov and
+               Sarfraz Khurshid},
+  title     = {State extensions for java pathfinder},
+  booktitle = {International Conference on Software Engineering, Demo Papers},
+  address   = {Leipzig, Germany},
+  month     = {May},
+  pages     = {863--866},
+  year      = {2008},
+  url       = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL09OptimizingGeneration.pdf},
+}
+
+@inproceedings{damorim:2007,
+  author    = {Marcelo d'Amorim and
+               Steven Lauterburg and
+               Darko Marinov},
+  title     = {Delta execution for efficient state-space exploration of object-oriented
+               programs},
+  booktitle = {Proceedings of the {ACM/SIGSOFT} International Symposium on Software
+               Testing and Analysis},
+  address   = {London, UK},
+  month     = {July},
+  pages     = {50--60},
+  year      = {2007},
+  url       = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL07DeltaExecution.pdf},
+}
+
+@inproceedings{zhou:2007,
+ 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},
+ title = {Delta Execution for Software Reliability},
+ booktitle = {Proceedings of the 3rd Workshop on on Hot Topics in System Dependability},
+ series = {HotDep'07},
+ year = {2007},
+ address = {Edinburgh, UK},
+ url = {http://mir.cs.illinois.edu/~marinov/publications/ZhouETAL07DeltaExecution.pdf},
+ publisher = {USENIX Association},
+} 
+
+@inproceedings{damorim:2006,
+  author    = {Marcelo d'Amorim and
+               Ahmed Sobeih and
+               Darko Marinov},
+  title     = {Optimized Execution of Deterministic Blocks in Java PathFinder},
+  booktitle = {Proceedings of Formal Methods and Software Engineering, 8th International Conference
+               on Formal Engineering Methods},
+  address   = {Macao, China}, 
+  month     =  {November},
+  pages     = {549--567},
+  year      = {2006},
+  url       = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL06OptimizedDeterministicBlocks.pdf},
+}
+
+@inproceedings{damorim:pacheco:2006,
+  author    = {Marcelo d'Amorim and
+               Carlos Pacheco and
+               Tao Xie and
+               Darko Marinov and
+               Michael D. Ernst},
+  title     = {An Empirical Comparison of Automated Generation and Classification
+               Techniques for Object-Oriented Unit Testing},
+  booktitle = {Proceedings of 21st {IEEE/ACM} International Conference on Automated Software Engineering},
+  address   = {Tokyo, Japan},
+  month     = {September},
+  pages     = {59--68},
+  year      = {2006},
+  url       = {​http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL06Symclat.pdf},
+}
+
+@unpublished{kulikov:2010,
+  author = {Sergey Kulikov and Nastaran Shafiei and Franck van Breugel and Willem Visser},
+  title = {{Detecting Data Races with Java PathFinder}},
+  year = "2010",
+  url = {http://www.cse.yorku.ca/~franck/research/drafts/race.pdf}
+}
+
+@inproceedings{indradeep:2013,
+  author = {Ghosh, Indradeep and Shafiei, Nastaran and Li, Guodong and Chiang, Wei-Fan},
+  title = {{JST: an automatic test generation tool for industrial Java applications with strings}},
+  booktitle = {Proceedings of the 35th International Conference on Software Engineering},
+  year = {2013},
+  month = {May},
+  address = {San Francisco, CA, USA},
+  pages = {992--1001},
+  publisher = {IEEE},
+  url = {http://dl.acm.org/citation.cfm?id=2486925}
+} 
+
+@article{nshafiei:2012,
+  author = {Shafiei, Nastaran and Mehlitz, Peter C.},
+  journal = {ACM SIGSOFT Software Engineering Notes},
+  number = 6,
+  pages = {1-5},
+  title = {{Modeling class loaders in Java PathFinder version 7}},
+  volume = 37,
+  year = 2012,
+  month = {November},
+  url = {http://dl.acm.org/citation.cfm?id=2382800}
+}
+
+@article{shafiei:2014,
+  author = {Shafiei, Nastaran and Mehlitz, Peter C.},
+  journal = {ACM SIGSOFT Software Engineering Notes},
+  number = 1,
+  pages = {1-5},
+  title = {{Extending JPF to verify distributed systems}},
+  volume = 39,
+  year = 2014,
+  month = {January},
+  url = {http://dl.acm.org/citation.cfm?id=2560577},
+}
+
+@inproceedings{shafiei:2013,
+  author    = {Nastaran Shafiei and
+               Franck van Breugel},
+  title     = {Towards model checking of computer games with Java PathFinder},
+  booktitle = {Proceedings of the 3rd International Workshop on Games and Software
+               Engineering},
+  address   = {San Francisco, CA, USA},
+  month     = {May},
+  pages     = {15--21},
+  year      = {2013},
+  url       = {http://dl.acm.org/citation.cfm?id=2662596},
+}
+
+
+@inproceedings{shafiei:breugel:2014,
+  author    = {Nastaran Shafiei and
+               Franck van Breugel},
+  title     = {Automatic handling of native methods in Java PathFinder},
+  booktitle = {Proceedings of the International SPIN Workshop on Model Checking of Software},
+  address   = {San Jose, CA, USA},
+  month     = {July},
+  pages     = {97--100},
+  year      = {2014},
+  url       = {http://dl.acm.org/citation.cfm?id=2632363},
+}
\ No newline at end of file