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},
10 publisher = {Kluwer Academic Publishers},
11 url = "http://dl.acm.org/citation.cfm?id=641186"
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},
20 publisher = {Springer},
21 url = "http://dl.acm.org/citation.cfm?id=380921.380931",
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},
30 publisher = {Springer},
31 url = "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.8862"
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},
44 url = "http://dl.acm.org/citation.cfm?id=1007526",
47 @article{pasareanu:2004,
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#},
54 author={Păsăreanu, Corina S. and Visser, Willem},
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},
64 url = {http://doi.acm.org/10.1145/1453101.1453131},
68 @inproceedings{pasareanu:2008,
69 author = {Corina S. P\v{a}s\v{a}reanu and
72 Karen Gundy{-}Burlet and
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},
82 url = {http://doi.acm.org/10.1145/1390630.1390635},
85 @inproceedings{pasareanu:2007,
86 author = {Corina S. P\v{a}s\v{a}reanu and
88 title = {Symbolic Execution and Model Checking for Testing},
89 booktitle = {Hardware and Software: Verification and Testing, Third International
90 Haifa Verification Conference},
93 url = {http://dx.doi.org/10.1007/978-3-540-77966-7_5},
96 @inproceedings{artho:2003,
97 author = {Cyrille Artho and
102 Corina S. P\v{a}s\v{a}reanu and
105 title = {Experiments with Test Case Generation and Runtime Analysis},
106 booktitle = {Abstract State Machines, Advances in Theory and Practice},
109 url = {http://dx.doi.org/10.1007/3-540-36498-6_5},
113 author = {Alex Groce and
115 title = {Heuristics for model checking Java programs},
116 journal = {International Journal on Software Tools for Technology Transfer},
121 url = {http://dx.doi.org/10.1007/s10009-003-0130-9},
124 @inproceedings{groce:2002,
125 author = {Alex Groce and
127 title = {Model checking Java programs using structural heuristics},
128 booktitle = {Proceedings of International Symposium on Software Testing and Analysis},
131 url = {http://doi.acm.org/10.1145/566172.566175},
134 @inproceedings{groce:visser:2002,
135 author = {Alex Groce and
137 title = {Heuristic Model Checking for Java Programs},
138 booktitle = {Proceedings of the 9th International SPIN Workshop on Model Checking of Software},
141 url = {http://dx.doi.org/10.1007/3-540-46017-9_21},
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},
152 address = {Lawrence, KS, USA},
153 url = {http://staff.aist.go.jp/c.artho/papers/checkpointing.pdf},
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},
164 address = {Auckland, New Zealand},
165 url = {http://staff.aist.go.jp/c.artho/papers/ase-2009.pdf},
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},
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},
177 address={Zurich, Switzerland},
179 url = {http://staff.aist.go.jp/c.artho/papers/tools-2008.pdf}
182 @inproceedings{grove:2003,
183 author = {Alex Groce and
185 title = {What Went Wrong: Explaining Counterexamples},
186 booktitle = {Proceedings of the 10th International SPIN Workshop on Model Checking of Software},
189 url = {http://dx.doi.org/10.1007/3-540-44829-2_8},
190 publisher = {Springer},
191 address = {Portland},
195 author = {John Penix and
198 Corina S. P\v{a}s\v{a}reanu and
202 title = {Verifying Time Partitioning in the {DEOS} Scheduling Kernel},
203 journal = {Formal Methods in System Design},
208 url = {http://dx.doi.org/10.1007/s10703-005-1490-4},
212 author = {Guillaume P. Brat and
214 Dimitra Giannakopoulou and
218 Corina S. Pasareanu and
222 title = {Experimental Evaluation of Verification and Validation Tools on Martian
224 journal = {Formal Methods in System Design},
229 url = {http://dx.doi.org/10.1023/B:FORM.0000040027.28662.a4},
232 @inproceedings{bordini:2003,
233 author = {Rafael H. Bordini and
238 title = {Model Checking Multi-Agent Programs with {CASP}},
239 booktitle = {Proceedings of Computer Aided Verification},
242 url = {http://dx.doi.org/10.1007/978-3-540-45069-6_10},
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},
254 url = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2004.1317443},
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},
263 url = {http://ti.arc.nasa.gov/m/pub-archive/1402/1402%20(Mehlitz).pdf},
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},
271 address = {Eindhoven, The Netherlands},
273 url = {http://dx.doi.org/10.1007/978-3-642-28166-2_13},
274 publisher = {Springer},
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},
283 publisher = {Kluwer Academic Publishers},
284 url = {http://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20080015887.pdf},
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)},
295 url = {http://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20030003734.pdf},
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)",
306 url = "http://ti.arc.nasa.gov/m/profile/pcorina/papers/tacas_sttt01.ps"
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},
314 address = {San Diego, USA},
316 url = {http://dl.acm.org/citation.cfm?id=872568},
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},
326 url = "http://ti.arc.nasa.gov/m/tech/rse/publications/papers/SIGSOFT00/fmsp00.pdf",
329 @article{havelund:2000,
330 author = {Klaus Havelund and
332 title = {Model Checking {Java} Programs using {Java} PathFinder},
333 journal = {International Journal on Software Tools for Technology Transfer (STTT)},
338 url = {http://www.havelund.com/Publications/jpf-sttt.ps.Z},
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},
347 url = {http://www.havelund.com/Publications/jpf1-spin-99.pdf},
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},
358 url = {http://www.havelund.com/Publications/jpf-fm99.ps.Z},
361 @article{havelund:2007,
362 author = {Klaus Havelund},
363 title = {Java PathFinder User Guide},
364 booktitle = {Unpublished Report},
366 url = {http://www.havelund.com/Publications/jpf-manual.ps.Z},
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},
374 url = {http://www.havelund.com/Publications/jpf1-report-99.pdf},
377 @inproceedings{gligoric:2010,
378 author = {Milos Gligoric and
384 title = {Test generation through programming in {UDITA}},
385 booktitle = {Proceedings of the 32nd {ACM/IEEE} International Conference on Software
387 address = {Cape Town, South Africa},
391 url = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL10UDITA.pdf},
394 @inproceedings{gligoric:jagannath:2010,
395 author = {Milos Gligoric and
398 title = {MuTMuT: Efficient Exploration for Mutation Testing of Multithreaded
400 booktitle = {Third International Conference on Software Testing, Verification and
404 address = {Paris, France},
406 url = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL10MuTMuT.pdf},
409 @inproceedings{lauterburg:2010,
410 author = {Steven Lauterburg and
411 Rajesh K. Karmani and
414 title = {Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction
416 booktitle = {Fundamental Approaches to Software Engineering},
417 address = {Paphos, Cyprus},
421 url = {http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL10DPORHeuristics.pdf},
424 @inproceedings{lauterburg:2009,
425 author = {Steven Lauterburg and
429 title = {A Framework for State-Space Exploration of Java-Based Actor Programs},
430 booktitle = {24th {IEEE/ACM} International Conference on Automated Software Engineering},
432 address = {Auckland, New Zealand},
435 url = {http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL09Basset.pdf},
438 @article{sobeih:2010,
439 author = {Ahmed Sobeih and
441 Mahesh Viswanathan and
444 title = {Assertion Checking in J-Sim Simulation Models of Network Protocols},
445 journal = {Simulation: Transactions of The Society for Modeling and Simulation International},
450 url = {http://dx.doi.org/10.1177/0037549709349326},
453 @inproceedings{gligoric:2009,
454 author = {Milos Gligoric and
456 Steven Lauterburg and
459 title = {Optimizing Generation of Object Graphs in Java PathFinder},
460 booktitle = {Second International Conference on Software Testing Verification and Validation},
462 address = {Denver, Colorado, {USA}},
465 url = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL09OptimizingGeneration.pdf},
468 @article{damorim:2008,
469 author = {Marcelo d'Amorim and
470 Steven Lauterburg and
472 title = {Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs},
473 journal = {{IEEE} Transactions on Software Engineering},
478 month = {September/October},
479 url = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL08DeltaExecution.pdf},
482 @inproceedings{lauterburg:2008,
483 author = {Steven Lauterburg and
487 title = {Incremental state-space exploration for programs with dynamically
489 booktitle = {International Conference on Software Engineering},
490 address = {Leipzig, Germany},
494 url = {http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL08IncrementalChecking.pdf},
497 @inproceedings{gvero:2008,
498 author = {Tihomir Gvero and
500 Steven Lauterburg and
504 title = {State extensions for java pathfinder},
505 booktitle = {International Conference on Software Engineering, Demo Papers},
506 address = {Leipzig, Germany},
510 url = {http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL09OptimizingGeneration.pdf},
513 @inproceedings{damorim:2007,
514 author = {Marcelo d'Amorim and
515 Steven Lauterburg and
517 title = {Delta execution for efficient state-space exploration of object-oriented
519 booktitle = {Proceedings of the {ACM/SIGSOFT} International Symposium on Software
520 Testing and Analysis},
521 address = {London, UK},
525 url = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL07DeltaExecution.pdf},
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},
534 address = {Edinburgh, UK},
535 url = {http://mir.cs.illinois.edu/~marinov/publications/ZhouETAL07DeltaExecution.pdf},
536 publisher = {USENIX Association},
539 @inproceedings{damorim:2006,
540 author = {Marcelo d'Amorim and
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},
550 url = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL06OptimizedDeterministicBlocks.pdf},
553 @inproceedings{damorim:pacheco:2006,
554 author = {Marcelo d'Amorim and
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},
566 url = {http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL06Symclat.pdf},
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}},
573 url = {http://www.cse.yorku.ca/~franck/research/drafts/race.pdf}
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},
582 address = {San Francisco, CA, USA},
585 url = {http://dl.acm.org/citation.cfm?id=2486925}
588 @article{nshafiei:2012,
589 author = {Shafiei, Nastaran and Mehlitz, Peter C.},
590 journal = {ACM SIGSOFT Software Engineering Notes},
593 title = {{Modeling class loaders in Java PathFinder version 7}},
597 url = {http://dl.acm.org/citation.cfm?id=2382800}
600 @article{shafiei:2014,
601 author = {Shafiei, Nastaran and Mehlitz, Peter C.},
602 journal = {ACM SIGSOFT Software Engineering Notes},
605 title = {{Extending JPF to verify distributed systems}},
609 url = {http://dl.acm.org/citation.cfm?id=2560577},
612 @inproceedings{shafiei:2013,
613 author = {Nastaran Shafiei and
615 title = {Towards model checking of computer games with Java PathFinder},
616 booktitle = {Proceedings of the 3rd International Workshop on Games and Software
618 address = {San Francisco, CA, USA},
622 url = {http://dl.acm.org/citation.cfm?id=2662596},
626 @inproceedings{shafiei:breugel:2014,
627 author = {Nastaran Shafiei and
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},
635 url = {http://dl.acm.org/citation.cfm?id=2632363},