--- /dev/null
+@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