Publications

Journal

1. A survey of new trends in symbolic execution for software testing and analysis
   Corina Pasareanu and Willem Visser
   International Journal on Software Tools for Technology Transfer (STTT)
   Volume 11, Number 4, October 2009
   Download
2. Property-based Slicing for Agent-Oriented Programming Language
   R. Bordini, M. Fisher, M. Wooldridge and W. Visser
   Journal of Logic and Computation
   2009 Volume 19 Number 6 Pages 1385-1425
   Official Link
3. Symbolic Execution with Abstraction.
   International Journal on Software Tools for Technology Transfer (STTT).
   Saswat Anand, Corina Pasareanu, Willem Visser
   Volume 11, Number 1, 2009
   Download
4. Predicate Abstraction with Under-approximation Refinement
   Logical Methods in Computer Science
   Corina Pasareanu, Radek Pelanek, Willem Visser
   Volume 3, Issue 1, 2007
   Download
5. Verifying Time Partitioning in the DEOS Scheduling Kernel
   J. Penix, W. Visser. C. Pasareanu, E. Engstrom, A. Larson and N. Weininger
   Formal Methods in Systems Design Journal
   Volume 26, Issue 2, March 2005
   Download
6. Combining Test Case Generation and Runtime Verification
   C. Artho, H. Barringer, A. Goldberg, K. Havelund, S. Khurshid, M. Lowry, C. Pasareanu, G. Rosu, K. Sen, W. Visser, R. Washington
   Theoretical Computer Science 336(2-3): 209-234 (2005)
   Download
7. Heuristics for Model Checking Java Programs
   A. Groce and W. Visser
   International Journal on Software Tools for Technology Transfer (STTT).
   Volume 6, Number 4, December 2004
   Download
8. Experimental Evaluation of Verification and Validation Tools on Martian Rover Software
   G. Brat, D. Drusinsky, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, R. Washington and W. Visser
   Formal Methods in Systems Design Journal
   Volume 25, September 2005
   Download
9. Finding Feasible Abstract Counter-Examples
   C. Pasareanu, M. Dwyer and W. Visser
   International Journal on Software Tools for Technology Transfer (STTT)
   Volume 5, Number 1, November 2003
   Download
10. Model Checking Programs
    W. Visser, K. Havelund, G. Brat, S. Park and F. Lerda
    Automated Software Engineering Journal
    Volume 10, Number 2, April 2003
    Download
11. Program Model Checking as a New Trend
    K. Havelund and W. Visser
    International Journal on Software Tools for Technology Transfer (STTT)
    Volume 4, Number 1, October 2002
    Download
12. Practical CTL* Model Checking – Should SPIN be extended
    W. Visser and H. Barringer.
    International Journal on Software Tools for Technology Transfer (STTT).
    Volume 2, Number 4, April 2000
    Download
13. Model Checking Rational Agents
    R. Bordini, M. Fisher, W. Visser, and M. Wooldridge
    IEEE Intelligent Systems 19(5):46-52.
    September/October, 2004

Conference

1. Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution
   Neha Rungta, Eric Mercer and Willem Visser.
   SPIN 2009. Grenoble France
   Download
2. Who Really Cares if the Program Crashes
   Abstract for Invited Presentation
   SPIN Workshop 2009
3. Symbolic Execution and Model Checking for Testing.
   Corina Pasareanu and Willem Visser
   Proceedings of the Third International Haifa Verification Conference (HVC)
   October 2007. Haifa, Israel
   See STTT Journal Version above (download)
4. Variably Interprocedural Program analysis for Runtime Error Detection
   Aaron Tomb, Guillaume Brat, Willem Visser
   Proc. of ISSTA, July 2007.
   Download
5. Formal Software Analysis Emerging Trends in Software Model Checking
   Matt Dwyer, John Hatcliff, Robby, Corina Pasareanu, Willem Visser
   Proc. International Conference on Software Engineering Future of Software Engineering (ICSE FOSE), 2007.
   Download
6. JPF-SE: A Symbolic Execution Extension to Java Pathfinder
   Saswat Anand, Corina Pasareanu, Willem Visser
   Proc. 13th International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007.
   Download
7. Test Input Generation for Java Containers using State Matching
   Willem Visser, Corina Pasareanu and Radek Pelanek
   Proc. of ISSTA, July 2006.
   Download
8. Symbolic Execution with Abstract Subsumption Checking
   Saswat Anand, Corina Pasareanu, Willem Visser
   Proc. of 13th International SPIN Workshop on Model Checking of Software (SPIN), 2006.
   Download
9. Autonomy Software: V\&V Challenges and Characteristics
   Johann Schumann, Willem Visser
   Proc. of IEEE Aerospace Conf., Bigsky, MT, March 2006.
10. A Simulation Based Model Checker for Real-time Java
    Gary Lindstrom, Peter Mehlitz, Willem Visser
    The 3rd Workshop on Java Technologies for Real-time and Embedded Systems (JTRES). October 2005
11. Towards the Verification of Human-Robot Teams
    M. Fisher, E. Pearce, M. Wooldridge, M. Sierhuis, W. Visser, W., R. Bordini
    Proc. of IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation
    Loyola College Graduate Center, Columbia, MD, 23-24 September 2005.
12. Model Checking Real Time Java Using Java PathFinder
    Gary Lindstrom, Peter Mehlitz, and Willem Visser
    Proc. Third International Symposium on Automated Technology for Verification and Analysis (ATVA) 2005
    Download
13. Test Input Generation for Red Black Trees using Abstraction
    Corina Pasareanu, Radek Pelanek and Willem Visser
    Proceedings of ASE 2005
    Download
14. Concrete Model Checking with Abstract Matching and Refinement
    Corina Pasareanu, Radek Pelanek and Willem Visser
    Proceedings of CAV 2005, LNCS 3576
    Download
15. Analyzing Interaction Orderings with Model Checking.
    Matthew Dwyer, Robby, Oksana Tkachuk, Willem Visser
    In Proceedings of the 19th Automated Software Engineering
    Conference. Linz, Austria, September 2004.
    Download
16. State-space Reduction Techniques in Agent Verification.
    R. Bordini, M. Fisher, W. Visser, and M. Wooldridge
    In Proceedings of the Third International Joint Conference
    on Autonomous Agents and Multi-Agent Systems (AAMAS-2004),
    New York, NY, 19-23 July 2004.
    Download
17. Test Input Generation with Java PathFinder
    W. Visser, C. Pasareanu, S. Khurshid
    Proceedings of ISSTA 2004
    Boston, MA, July 2004
    Download
18. Verification of Java Programs Using Symbolic Execution and Invariant Generation
    C. Pasareanu and W. Visser
    Proceedings of SPIN 2004
    Barcelona, Spian, April 2004
    LNCS 2989
    Download
19. Experiments with Test Case Generation and Runtime Analysis
    C. Artho, D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu, W. Visser
    Proceedings of Abstract State Machines 2003
    Taormina, Italy, March 2003
    LNCS 2589
    Download
20. Auto-Generating Test Sequences using Model Checkers: A Case Study
    M. Heimdahl, S. Rayadurgam, W. Visser, G. Devaraj, J. Gao
    Proceedings of Formal Approaches to Testing of Software (FATES) 2003
    Quebec, Canada, October 2003
    LNCS 2931
    Download (conference version)
    
21. Model Checking Multi-Agent Programs with CASP
    R. Bordini, M. Fisher, C. Pardavila, W. Visser, M. Wooldridge
    Proceedings of CAV 2003
    Boulder, Colorado, July 2003
    LNCS 2725
    Download
22. What Went Wrong: Explaining Counterexamples
    A. Groce and W. Visser
    Proceedings of SPIN 2003. Portland, Oregon. May 2003
    Download (.ps)
    
23. Generalized Symbolic Execution for Model Checking and Testing
    S. Khurshid, C. S. Pasareanu and W. Visser
    Proceedings of TACAS 2003. Warsaw, Poland, April 2003
    Download (.ps)
    
24. Model Checking Java Programs using Structural Heuristics
    A. Groce and W. Visser
    Proceedings of ISSTA 2002. Rome, Italy. July 2002
    Download (.ps.gz)
    
25. Heuristic Model Checking for Java Programs
    A. Groce and W. Visser
    Proceedings of SPIN 2002. Grenoble, France. April 2002
    Download (.pdf)
    
26. Combining Static Analysis and Model Checking for Software Analysis
    G. Brat and W. Visser
    Proceedings of ASE2001. San Diego, November 2001
    Download (.ps.gz)
    
27. Addressing Dynamic Issues of Program Model Checking
    F. Lerda and W. Visser
    Proccedings of SPIN2001. Toronto, May 2001
    Download (.ps.gz)
    
28. Tool-supported Program Abstraction for Finite-state Verification
    M. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, Robby, W. Visser, H. Zheng
    Proceedings of ICSE2001. Toronto, Canada, May 2001.
    Download (.pdf)
    
29. Finding Feasible Counter-examples when Model Checking Abstracted Java Programs
    C. Pasareanu, M. Dwyer, W. Visser
    Proceedings of TACAS2001. April 2001.
    Download (.pdf)
    
30. Model Checking Programs.
    W. Visser, K. Havelund, G. Brat, S. Park.
    Proceedings of the 15th International Conference on Automated Software Engineering (ASE), Grenoble, France, September 2000.
    Download (.ps.gz)
    
31. Applying Predicate Abstraction to Model Check Object-Oriented Programs.
    W. Visser, S. Park and J. Penix.
    3rd ACM SIGSOFT Workshop on Formal Methods in Software Practice. August 2000.
    Download (.ps.gz).
    
32. Java PathFinder – A second generation of a Java model checker
    G. Brat, K. Havelund, S. Park, W. Visser
    Proceedings of the Workshop on Advances in Verification, Chicago, Illinois, July 2000.
    Download (.ps.gz)
    
33. Verification of Time Partitioning in the DEOS real-time Scheduling Kernel.
    J Penix, W. Visser, E. Engstrom, A. Larson and N. Weininger.
    22nd International Conference on Software Engineering. June 2000.
    Download (.ps.gz).
    
34. Formal Analysis of the Remote Agent Before and After Flight.
    K. Havelund, M. Lowry, S. Park, C. Pecheur, J. Penix, W. Visser, J.L. White.
    5th Langley Formal Methods Workshop. June 2000.
    Download (.ps.gz)
    
35. Adding Active Objects to SPIN.
    W. Visser, K. Havelund and J. Penix.
    Participants proceedings of SPIN99a Workshop. July 1999. Trento, Italy.
    Download (.ps.gz).
    
36. Efficient CTL* Model Checking using Games and Automata.
    W. Visser
    Ph.D. Thesis. University of Manchester, UK. June 1998.
    Download (.ps.gz).
    
37. Efficient CTL Model Checking for Analysis of Rainbow Designs.
    W. Visser, H. Barringer, D. Fellows, G. Gough and A. Williams.
    Proceedings of CHARME97 Workshop. Montreal, Canada. October 1997.
    Download (.ps.gz).
    
38. Memory Efficient State Storage in SPIN
    W. Visser and H. Barringer
    Proceedings of SPIN96 Workshop. Rutgers, USA. August 1996.
    Download (.ps.gz).
    
39. A Run-time Environment for a Validation Language
    W. Visser
    M.Sc. Thesis. University of Stellenbosch, South Africa. December 1993.
    Download (.ps.gz).

Workshop Organization

1. Software Model Checking Workshop
   S. Stoller and W. Visser
   Electronic Notes in Theoretical Computer Science
   Volume 55, Number 3, July 2001
2. Software Model Checking Workshop
   B. Cook, S. Stoller and W. Visser
   Electronic Notes in Theoretical Computer Science
   Volume 89, Number 3, July 2003
3. The First International Workshop on Automated Program Analysis, Testing and Verification
   N. Tracy, J. Penix and W. Visser
   Guest Editors
   Software Testing, Verification & Reliability Journal
   Volume 11, Number 2, June 2001
4. RIACS Workshop on the Verification and Validation of Autonomous and Adaptive Systems
   C. Pecheur, W. Visser and R. Simmons
   AI Magazine
   Volume 22, Number 3, 2001
5. 7th International SPIN Workshop on Model Checking and Software Verification
   K. Havelund, J. Penix and W. Visser
   Editors
   September 2000
   Lecture Notes in Computer Science, Volume 1885