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