@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},
}