Publications

Journal

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