- All Publications
- Static Analysis
- FLAVERS
- PROPEL
- Finite-State Verification
»
- Property Specification
- Fault-Tree Analysis
- Failure Mode and Effect Analysis
- MPI Verification
- INCA
- Experimentation
- Process Programming and Workflow
[...]
- Software Development
[...]
- Case Studies
[...]
- Electronic Enterprise Institute
- Jump To:
- 2012
- 2010
- 2008
- 2006
- 2004
- 2003
- 2002
- 2001
- 2000
- 1999
- 1998
- 1997
- 1996
- 1995
- 1990
|
LASER Publications
Finite-State Verification
A Systematic Process-model-based Approach for Synthesizing Attacks and Evaluating Them
Huong Phan,
George S. Avrunin,
Lori A. Clarke,
Leon J. Osterweil,
Matt Bishop,
2012 Electronic Voting Technology Workshop/Workshop on Trustworthy Elections (EVT/WOTE '12), August 6-7, 2012. (UM-CS-2012-029)
[ Usenix ]
[ PDF ]
[ Slides ]
Improving Processes Using Static Analysis Techniques
Bin Chen,
Doctoral Thesis, Department of Computer Science, University of Massachusetts, Amherst, MA 01003, September 2010. (THESIS-CHEN)
[ PDF ]
Specifying and Verifying Requirements for Election
Processes
Borislava I. Simidchieva,
Matthew S. Marzilli,
Lori A. Clarke,
Leon J. Osterweil,
In dg.o 2008: Proceedings of the 9th Annual International Conference on Digital Government Research, Montreal, Canada, May 2008, S. A. Chun, M. Janssen, and J. R. Gil-Garcia, Eds., Digital Government Society of North America, pp. 63-72. (UM-CS-2008-21)
[ ACM ]
[ PDF ]
[ Slides ]
Analyzing Medical Processes
Bin Chen,
George S. Avrunin,
Elizabeth A. Henneman,
Lori A. Clarke,
Leon J. Osterweil,
Philip L. Henneman,
ACM SIGSOFT/IEEE 30th International Conference on Software Engineering (ICSE'08), Leipzig, Germany, May 2008, pp. 623-632. (UM-CS-2007-51)
[ ACM ]
[ PDF ]
[ Slides ]
Using Software Engineering Technology to Improve the Quality of Medical Processes
Lori A. Clarke,
George S. Avrunin,
Leon J. Osterweil,
ACM SIGSOFT/IEEE Companion 30th International Conference on Software Engineering (ICSE'08), Leipzig, Germany, May 2008, pp. 889-898. (UM-CS-2008-20)
[ ACM ]
[ PDF ]
[ Slides ]
Breaking Up is Hard to Do: An Evaluation of Automated Assume-Guarantee Reasoning
Jamieson M. Cobleigh,
George S. Avrunin,
Lori A. Clarke,
ACM Transactions on Sofware Engineering and Methodology. Vol. 17, Issue 2, April 2008. (UM-CS-2007-27)
This is an updated version of TR UM-CS-2007-07, which was originally dated August 2007. This report is a revised and extended version of UM-CS-2004-022, which appeared in ISSTA 2006.
[ ACM ]
[ PDF ]
[ Online-only Appendix ]
[ Experimental Subjects ]
Breaking Up is Hard to Do: An Investigation of Decomposition for Assume-Guarantee Reasoning
Jamieson M. Cobleigh,
George S. Avrunin,
Lori A. Clarke,
ACM SIGSOFT 2006 International Symposium on Software Testing and Analysis (ISSTA '06) Portland, ME, pp. 97-108, July 2006. (UM-CS-2004-022)
This is an updated version originally dated May 2004. Please see "Breaking Up is Hard to Do: An Evaluation of Automated Assume-Guarantee Reasoning" UM-CS-2007-27 for a revised and extended version of this report.
[ ACM ]
[ PDF ]
[ PDF with Appendix B ]
[ Slides ]
Verification Support for Plug-and-Play Architectural Design
Shangzhu Wang,
George S. Avrunin,
Lori A. Clarke,
ACM SIGSOFT 2006 Workshop on Role of Software Architecture for Testing and Analysis (ROSATEA 2006), Portland, ME, pp. 49-50, July 2006. (UM-CS-2006-32)
[ ACM ]
[ PDF ]
[ Poster ]
Managing Space for Finite-State Verification
Jianbin Tan,
George S. Avrunin,
Lori A. Clarke,
ACM SIGSOFT/IEEE 28th International Conference on Software Engineering (ICSE 2006), Shanghai, China, pp. 152-161, May 2006. (UM-CS-2005-66)
[ ACM ]
[ PDF ]
[ Slides ]
Heuristic-Guided Counterexample Search in FLAVERS
Jianbin Tan,
George S. Avrunin,
Lori A. Clarke,
Shlomo Zilberstein,
Stefan Leue,
ACM SIGSOFT 2004, 12th International Symposium on the Foundations of Software Engineering (FSE 12), Newport Beach, CA, pgs 201-210, November 2004. (UM-CS-2004-023)
[ ACM ]
[ PDF ]
[ Slides ]
Flow Analysis for Verifying Properties of Concurrent Software Systems
Matthew B. Dwyer,
Lori A. Clarke,
Jamieson M. Cobleigh,
Gleb Naumovich,
ACM Transactions on Software Engineering and Methodology (TOSEM), Vol. 13, No. 4, pp. 359-430, October 2004. (UM-CS-2004-006)
This is an updated version of UM-CS-1999-052 and UM-CS-2003-030.
[ ACM ]
[ PDF ]
[ Appendices B and C ]
Flow Analysis for Verifying Properties of Concurrent Software Systems
Matthew B. Dwyer,
Lori A. Clarke,
Jamieson M. Cobleigh,
Gleb Naumovich,
Department of Computer Science, University of Massachusetts, Amherst, MA 01003, October 2003. (UM-CS-2003-030)
See UM-CS-2004-006 for an updated version
The INCA Query Language
Stephen F. Siegel,
Department of Computer Science, University of Massachusetts, Amherst, MA 01003, May 2002. (UM-CS-2002-018)
[ PostScript ]
[ PDF ]
FLAVERS: a Finite State Verification Technique for Software Systems
Jamieson M. Cobleigh,
Lori A. Clarke,
Leon J. Osterweil,
IBM Systems Journal (Issue on Software Testing and Verification), 41(1), pp. 140-165, 2002. (UM-CS-2001-017)
[ IBM Systems Journal ]
[ PostScript ]
[ PDF ]
Extending FLAVERS to Check Properties on Infinite Executions of Concurrent Software Systems
Gleb Naumovich,
Lori A. Clarke,
Monterey Workshop 2001 on Engineering Automation for Software Intensive System Integration, Monterey, CA, pp. 267-276, June 2001. (UM-CS-2000-010)
[ PostScript ]
[ PDF ]
The Right Algorithm at the Right Time: Comparing Data Flow Analysis Algorithms for Finite State Verification
Jamieson M. Cobleigh,
Lori A. Clarke,
Leon J. Osterweil,
23rd International Conference on Software Engineering (ICSE 2001), Toronto, Canada, pp. 37-46, May 2001. (UM-CS-2000-046)
[ PostScript ]
[ PDF ]
[ IEEE ]
Improving the Precision of INCA by Preventing Spurious Cycles
Stephen F. Siegel,
George S. Avrunin,
ACM Sigsoft 2000 International Symposium on Software Testing and Analysis (ISSTA 2000), Portland, OR, pp. 191-200, August 2000. (UM-CS-2000-009)
[ PostScript ]
[ PDF ]
Comparing Finite-State Verification Techniques for Concurrent Software
George S. Avrunin,
James C. Corbett,
Matthew B. Dwyer,
Corina S. Pasareanu,
Stephen F. Siegel,
Department of Computer Science, University of Massachusetts, Amherst, MA 01003, November 1999. (UM-CS-1999-069)
[ PostScript ]
[ PDF ]
Flow Analysis for Verifying Specifications of Concurrent and Distributed Software
Matthew B. Dwyer,
Lori A. Clarke,
Department of Computer Science, University of Massachusetts, Amherst, MA 01003, August 1999. (UM-CS-1999-052)
See UM-CS-2004-006 for an updated version
[ PostScript ]
[ PDF ]
Benchmarking Finite-State Verifiers
George S. Avrunin,
James C. Corbett,
Matthew B. Dwyer,
Department of Computer Science, University of Massachusetts, Amherst, MA 01003, July 1999. (UM-CS-1999-048)
[ PostScript ]
[ PDF ]
Patterns in Property Specifications for Finite-State Verification
Matthew B. Dwyer,
George S. Avrunin,
James C. Corbett,
21st International Conference on Software Engineering (ICSE 1999), Los Angeles, CA, pp. 411-420, May 1999. (UM-CS-1998-035)
[ PostScript ]
[ PDF ]
[ ACM ]
Data Flow Analysis for Checking Properties of Concurrent Java Programs
Gleb Naumovich,
George S. Avrunin,
Lori A. Clarke,
21st International Conference on Software Engineering (ICSE 1999), Los Angeles, CA, pp. 399-410, May 1999. (UM-CS-1998-022)
[ PostScript ]
[ PDF ]
Using Partial Order Techniques to Improve Performance of Data Flow Analysis Based Verification
Gleb Naumovich,
Lori A. Clarke,
Jamieson M. Cobleigh,
ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 1999) ,Toulouse, France, pp. 57-65, September 1999. (UM-CS-1999-024)
[ PostScript ]
[ PDF ]
Efficient Composite Data Flow Analysis Applied to Concurrent Programs
Gleb Naumovich,
Lori A. Clarke,
Leon J. Osterweil,
ACM SIGPLAN SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 1998), Montreal, Quebec, Canada, pp. 51-58, June 1998. (UM-CS-1998-082)
Replaces UM-CS-1997-043.
[ PostScript ]
[ PDF ]
A Conservative Data Flow Algorithm for Detecting all Pairs of Statements that may Happen in Parallel
Gleb Naumovich,
George S. Avrunin,
6TH ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 6), Lake Buena Vista, FL, pp. 24-34, November 1998. (UM-CS-1998-023)
[ PostScript ]
[ PDF ]
Property Specification Patterns for Finite-State Verification
Matthew B. Dwyer,
George S. Avrunin,
James C. Corbett,
2nd Workshop on Formal Methods in Software Practice (FMSP 1998), Clearwater Beach, FL, pp. 7-15, March 1998. (UM-CS-1997-049)
[ PostScript ]
[ PDF ]
Applying Static Analysis to Software Architectures
Gleb Naumovich,
George S. Avrunin,
Lori A. Clarke,
Leon J. Osterweil,
5th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 5) and the 6th European Software Engineering Conference (ESEC 1997), Zurich, Switzerland, Springer Verlag Lecture Notes In Computer Science #1301, pp. 77-93, Sept. 1997. (UM-CS-1997-008)
[ PostScript ]
[ PDF ]
An Empirical Comparison of Static Concurrency Analysis Techniques
A.T. Chamillard,
Lori A. Clarke,
George S. Avrunin,
Department of Computer Science, University of Massachusetts, Amherst, MA 01003, May 1997 (Revised). (UM-CS-1996-084)
[ PostScript ]
[ PDF ]
Verification of Communication Protocols Using Data Flow Analysis
Gleb Naumovich,
Lori A. Clarke,
Leon J. Osterweil,
4th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 4), San Francisco, CA, pp. 93-105, October 1996. (UM-CS-1996-027)
[ PostScript ]
[ PDF ]
A Flexible Architecture for Building Data Flow Analyzers
Matthew B. Dwyer,
Lori A. Clarke,
18th International Conference on Software Engineering (ICSE 1996), Berlin, Germany, pp. 554-564, March 1996. (UM-CS-1995-079)
[ PostScript ]
[ PDF ]
Data Flow Analysis for Verifying Correctness Properties of Concurrent Programs
Matthew B. Dwyer,
Doctoral Thesis, Department of Computer Science, University of Massachusetts, Amherst, MA 01003, September 1995. (THESIS-DWYER)
[ PostScript ]
[ PDF ]
Data Flow Analysis Frameworks for Concurrent Programs
Matthew B. Dwyer,
Department of Computer Science, University of Massachusetts, Amherst, MA 01003, July 1995. (UM-CS-1995-062)
[ PostScript ]
[ PDF ]
Automatic Generation of Inequality Systems for Constrained Expression Analysis
George S. Avrunin,
Ugo A. Buy,
James C. Corbett,
Department of Computer Science, University of Massachusetts, Amherst, MA 01003, May 1990. (UM-CS-1990-032)
[ PostScript ]
[ PDF ]
Notice: We present this material to ensure timely and wide dissemination of our work.
All persons copying this material must adhere to the terms of the relevant copyrights
|
This site is maintained by the