I'm now working at SEVEN Networks as a Senior Software Engineer. See my homepage for contact details and more information about my current whereabouts.

During my time as a contractor at NASA I was employed by RIACS (Research Institute for Advanced Computer Science) and conduct my research within the Automated Software Engineering group at NASA Ames. I obtained an M.Sc. from the  University of Stellenbosch in South Africa (1993) and a Ph.D. from the University of Manchester in the UK (1998).

My research focuses on doing model checking for actual programs and more specifically I'm working on Java PathFinder , a model checker for Java. My research is slowly tilting towards testing and to that end we have extended JPF with a symbolic execution capability that allows us to reason over symbolic data and symbolic structures. The main application off the new JPF is to do test-input generation in both a black- and white-box fashion. 

Program Committees

• Program co-Chair for ASE 2008
• Brazilian Symposium on Formal Methods 2007
  
• ICSE 2007
  
• ICSE 2005 Experience Reports Track
  
• Foundations of Software Engineering (FSE) 2004
  
• International Workshop on Parallel and Distributed Model Checking (PDMC) 2003, 2004 and 2005
  
• Infinity 2004 and 2005
  
• International Conference on Automated Software Engineering (ASE) 2001, 2002, 2003, 2005, 2006, and 2007
• SPIN Workshop 2000, 2001, 2002, 2005, 2006, and 2007
• Formal Methods for Industrial Critical Systems (FMICS) 2002
• Tools and Algorithms for Construction and Analysis of Systems (TACAS) 2003
• Model Checking and Artificial Intelligence Workshop 2002
• Software Model Checking Workshop 2001, 2003 and 2005
  

Publications

Journal

1. Predicate Abstraction with Under-approximation Refinement Logical Methods in Computer Science
   Corina Pasareanu, Radek Pelanek, Willem Visser
   (To Appear in 2007)
   
2. 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
3. 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
4. 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
5. 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
   
6. 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 
7. 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 
8. 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
   
9. 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
10. Model Checking Rational Agents
    R. Bordini, M. Fisher, W. Visser,  and M. Wooldridge
    IEEE Intelligent Systems 19(5):46-52.
    September/October, 2004
    

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

Conference

1. 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
   
2. Test Input Generation for Java Containers using State Matching
   Willem Visser, Corina Pasareanu and Radek Pelanek
   Proc. of ISSTA, July 2006.
   Download
   
3. 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
   
4. Autonomy Software: V\&V Challenges and Characteristics
   Johann Schumann, Willem Visser
   Proc. of IEEE Aerospace Conf., Bigsky, MT, March 2006.
   
5. 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
   
6. 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.
   
7. 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
   
8. Test Input Generation for Red Black Trees using Abstraction
   Corina Pasareanu, Radek Pelanek and Willem Visser
   Proceedings of ASE 2005
   Download
   
9. Concrete Model Checking with Abstract Matching and Refinement
   Corina Pasareanu, Radek Pelanek and Willem Visser
   Proceedings of CAV 2005, LNCS 3576
   Download
   
10. 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
    
11. 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
    
12. Test Input Generation with Java PathFinder
    W. Visser, C. Pasareanu, S. Khurshid
    Proceedings of ISSTA 2004
    Boston, MA, July 2004
    Download
    
13. 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
    
14. 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
    
15. 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)
    
16. 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
    
17. What Went Wrong: Explaining Counterexamples
    A. Groce and W. Visser
    Proceedings of SPIN 2003. Portland, Oregon. May 2003
    Download (.ps)
    
18. 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)
    
19. Model Checking Java Programs using Structural Heuristics
    A. Groce and W. Visser 
    Proceedings of ISSTA 2002. Rome, Italy. July 2002 
    Download (.ps.gz)
    
20. Heuristic Model Checking for Java Programs  
    A. Groce and W. Visser 
    Proceedings of SPIN 2002. Grenoble, France. April 2002
    Download (.pdf)
    
21. Combining Static Analysis and Model Checking for Software Analysis 
    G. Brat and W. Visser 
    Proceedings of ASE2001. San Diego, November 2001 
    Download (.ps.gz)
    
22. Addressing Dynamic Issues of Program Model Checking 
    F. Lerda and W. Visser 
    Proccedings of SPIN2001. Toronto, May 2001 
    Download (.ps.gz)
    
23. 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)
    
24. Finding Feasible Counter-examples when Model Checking Abstracted Java Programs 
    C. Pasareanu, M. Dwyer, W. Visser 
    Proceedings of TACAS2001. April 2001. 
    Download (.pdf)
    
25. 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)
    
26. 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).
    
27. 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)
    
28. 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).
    
29. 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)
    
30. Adding Active Objects to SPIN.  
    W. Visser, K. Havelund and J. Penix. 
    Participants proceedings of SPIN99a Workshop. July 1999. Trento, Italy. 
    Download (.ps.gz).
    
31. Efficient CTL* Model Checking using Games and Automata. 
    W. Visser 
    Ph.D. Thesis. University of Manchester, UK. June 1998. 
    Download (.ps.gz).
    
32. 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).
    
33. Memory Efficient State Storage in SPIN 
    W. Visser and H. Barringer 
    Proceedings of SPIN96 Workshop. Rutgers, USA. August 1996. 
    Download (.ps.gz).
    
34. A Run-time Environment for a Validation Language 
    W. Visser 
    M.Sc. Thesis. University of Stellenbosch, South Africa. December 1993. 
    Download (.ps.gz).

• Software Model Checking Tutorial 
  This is a historical overview of model checking for software with a distinct JPF-slant
  This was presented as a tutorial at ASE 2002 and a number of times afterwards at different places
• Symbolic Execution and Test-input Generation
  This showcases how JPF with symbolic execution can be used to generate tests for branch-coverage of red-black trees
  This presentation is a mix of ones given at University of Utah, BYU and UC Santa Cruz in early 2004
• Experimental Evaluation of  V&V Tools on Martian Rover Software
  Results from the case study where we compared testing with static analysis, model checking and runtime analysis
  Presented at the SEI Software Model Checking Workshop in 2003
  This holds no punches - read at own risk!