|
|
|
|
Papers
- Kiasan/KUnit: Automatic Test Case Generation and Analysis Feedback for Open Object-oriented Systems, April 2007.
Xianghua (William) Deng, Robby, John Hatcliff.
Technical Report, SAnToS-TR2007-1 (submitted for publication).
pdf (extended version, last updated: April 23, 2007)
The extended version includes: (1) expanded experiment data for KUnit (using lazy/lazier# initialization algorithms), (2) an expanded report on java.util.TreeMap coverage analysis, (3) expanded jCUTE experiment data and comparison, (3) Kiasan's (lazy/lazier/lazier#) formal semantics and relative soundness and completeness proofs, and (4) KUnit (lazy/lazier/lazier#) reverse execution formal semantics and consistency proofs wrt. Kiasan's formal semantics.
Experiment data: lazy initialization, lazier# initialization
|
|
- Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs, April 2007.
Xianghua Deng, Robby, and John Hatcliff.
Technical Report, SAnToS-TR2007-3 (accepted at SEFM 2007).
pdf (extended version, last updated: June 24, 2007)
The extended version includes: (1) experiment data summaries for Kiasan (using the lazy/lazier/lazier# initialization algorithms), (2) swap's (lazy/lazier/lazier#) symbolic states, (3) expanded description of the case counting method (red-black tree, binary search tree, and AVL tree), and (4) Kiasan's (lazy/lazier/lazier#) formal semantics and relative soundness/completeness proofs.
Experiment Data: lazy initialization, lazier initialization, lazier# initialization
|
|
- Enabling Efficient Partial Order Reductions for Model Checking Object-oriented Programs Using Static Calculation of Program Dependences, March 2007.
Venkatesh P. Ranganath, John Hatcliff, and Robby.
Technical Report, SAnToS-TR2007-2.
pdf (extended version, last updated: March 29, 2007).
|
|
- Building Your Own Software Model Checker Using The Bogor Extensible Model Checking Framework, January 2005.
Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby.
In the Proceedings of 17th Conference on Computer-Aided Verification (CAV 2005).
Technical Report, SAnToS-TR2005-1.
pdf (Last updated: April 29, 2005).
|
|
- Bogor: An Extensible Framework for Domain-Specific Model Checking, December 2004.
John Hatcliff, Matthew B. Dwyer, Robby.
To appear in the Newsletter of European Association of Software Science and Technology (EASST).
Technical Report, SAnToS-TR2004-9.
pdf (Last updated: December 1, 2004).
|
|
- Supporting Model Checking Education using BOGOR/Eclipse, August 2004.
Matthew B. Dwyer, John Hatcliff, Robby.
In the Proceedings of the 2004 OOPSLA Workshop on Eclipse
Technology eXchange (eTX/OOPSLA 2004).
Technical Report, SAnToS-TR2004-6.
pdf (Last updated: January 5, 2005). Software Model Checking: Theory and Practice website
|
|
- A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking, June 2004.
Edwin Rodr
|
|
- Space-Reduction Strategies for Model Checking Dynamic Systems, May 2003.
Robby, Matthew B. Dwyer, John Hatcliff, Radu Iosif.
In the Proceedings of 2003 Workshop on Software Model Checking (SoftMC 2003).
Technical Report, SAnToS-TR2003-5.
pdf (Last updated: August 7, 2003).
|
|
- Bogor: A Flexible Framework for Creating Software Model Checkers, June 2006.
Robby, Matthew B. Dwyer, John Hatcliff.
In the Proceedings of Testing: Academic & Industrial Conference - Practice And Research Techniques.
Technical Report, SAnToS-TR2006-2.
pdf (Last updated: June 15, 2006).
|
|
- Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems, March 2006.
Xianghua Deng, Jooyong Lee, Robby.
To appear in the Proceedings of the 21st IEEE International Conference on Automated Software Engineering.
Technical Report, SAnToS-TR2006-1.
pdf (Last updated: June 30, 2006).
|
|
- Using Design Metrics for Predicting System Flexibility, October 2005.
Robby, Scott A. DeLoach, Valeriy A. Kolesnikov.
In the Proceedings of the 2006 International Conference on Fundamental Approaches to Software Engineering (FASE 2006).
pdf (Last updated: January 5, 2005).
|
|
- Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs, October 2005.
Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Venkatesh Prasad Ranganath, Robby, and Todd Wallentine.
In the Proceedings of the Tweflth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2006).
pdf (Last updated: January 6, 2005).
|
|
- Extending JML for Modular Specification and Verification of Multi-Threaded Programs, December
2004.
Edwin Rodr
|
|
- A Case Study in Domain-customized Model Checking for Real-time Component Software, July 2004.
Matthew Hoosier, John Hatcliff, Robby, Matthew B. Dwyer.
To appear in the Proceedings of the 1st International Symposium on Leveraging Applications of Formal Method (ISoLA 2004)
Technical Report, SAnToS-TR2004-4.
pdf (Last updated: July 11,
2004). Experimental Artifacts
|
|
- Analyzing Interaction Orderings with Model Checking, April 2004.
Matthew B. Dwyer, Robby, Oksana Tkachuk, Willem Visser.
In the Proceedings of the Nineteenth IEEE International Conference on Automated Software Engineering (ASE 2004).
Technical Report, SAnToS-TR2004-1.
pdf (Last updated: April 14, 2004). BEG website
|
|
- Checking Strong Specifications Using An Extensible Software Model Checking Framework, October 2003.
Robby, Edwin Rodr
|
|
- Verifying Atomicity Specifications for Concurrent Object-Oriented Software using Model Checking, August 2003.
John Hatcliff, Robby, Matthew B. Dwyer.
In the Proceedings of the Fifth International Conference on
Verification, Model Checking and Abstract Interpretation (VMCAI 2004).
Technical Report, SAnToS-TR2003-7.
pdf (Last updated: November 11, 2003). examples
|
|
- Space Reductions for Model Checking Quasi-Cyclic Systems, April 2003.
Matthew B. Dwyer, Robby, William Deng, John Hatcliff.
In the Proceedings of the Third International Conference on Embedded Software (EMSOFT 2003).
Technical Report, SAnToS-TR2003-4.
pdf (Last updated: July 28, 2003). case-studies
|
|
- Bogor: An Extensible and Highly-Modular Model Checking Framework, March 2003.
Robby, Matthew B. Dwyer, John Hatcliff
In the Proceedings of the Fourth Joint Meeting of the European Software
Engineering Conference and ACM SIGSOFT Symposium on the Foundations of
Software Engineering (ESEC/FSE 2003).
Technical Report, SAnToS-TR2003-3.
pdf (Last updated: July 1, 2003).
|
|
- Model-checking Middleware-based Event-driven Real-time Embedded Software, March 2003.
William Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Robby, Gurdip Singh.
In the Proceedings of the First International Symposium on Formal Methods for Components and Objects (FMCO 2002).
Technical Report, SAnToS-TR2003-2.
pdf (Last updated: April 9, 2003).
|
|
- Exploiting
Object Escape and Locking Information in Partial Order Reduction for
Concurrent Object-Oriented Programs, February 2003.
Matthew B. Dwyer, John Hatcliff, Robby, Venkatesh R. Prasad.
In Formal Methods in System Design Journal (FMSD), Volume 25, Issue 2-3, Sep-Nov 2004, p.199-240.
Technical Report, SAnToS-TR2003-1.
pdf (Last updated: March 23, 2004).
Kluwer Online (most recent)
|
|
- Checking JML Specifications Using An Extensible Software Model Checking Framework, August 2004.
Robby, Edwin Rodr
|
|
|
|
|
|
|
Papers