Home > LASER Publications > Static Analysis > George S. Avrunin
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:
2016
2014
2013
2012
2010
2008
2007
2006
2005
2004
2003
2002
2001
2000
1999
1998
1997
1996
1995
1994
1993
1992
1991
1990
1989
1985

LASER Publications

Static Analysis

by George S. Avrunin

 2014

Insider Threat Identification by Process Analysis
Matt Bishop, Heather M. Conboy, Huong Phan, Borislava I. Simidchieva, George S. Avrunin, Lori A. Clarke, Leon J. Osterweil, Sean Peisert, In Proceedings of the 2014 Workshop on Research for Insider Threat (WRIT) May 18, San Jose, CA (2014), pp. 251-264.. (UM-CS-2014-014)

[ PDF ]

 2013

Modal Abstraction View of Requirements for Medical Devices Used in Healthcare Processes
Heather M. Conboy, George S. Avrunin, Lori A. Clarke, International Conference on Software Engineering, Workshop on Software Engineering in Health Care (SEHC'13), San Francisco, CA, USA, May 20-21, 2013. (UM-CS-2013-010)

[ PDF ] [ Slides ]

 2012

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 ]

 2010

Process-based Derivation of Requirements for Medical Devices
Heather M. Conboy, George S. Avrunin, Lori A. Clarke, IHI '10 Proceedings of the First ACM International Health Informatics Symposium, Arlington, VA, November 11-12, 2010, pp 656-665. (UM-CS-2010-053)

This report replaces UM-CS-2010-034, originally dated June 2010.

[ ACM ] [ PDF ]

An Automatic Failure Mode and Effect Analysis Technique for Processes Defined in the Little-JIL Process Definition Language
Danhua Wang, Jingui Pan, George S. Avrunin, Lori A. Clarke, Bin Chen, The 22nd International Conference on Software Engineering and Knowledge Engineering (SEKE 2010), Page 765-770, San Francisco Bay, USA, July 1-3, 2010. (UM-CS-2010-035)

[ PDF ] [ Slides ]

An Integrated Collection of Tools for Continuously Improving the Processes by Which Health Care is Delivered: A Tool Report
Leon J. Osterweil, George S. Avrunin, Lori A. Clarke, Lecture Notes in Business Information Processing, Vol. 43, 647-653. (UM-CS-2010-029)

Revised paper from the Third International Workshop on Process-oriented Information Systems in Healthcare (ProHealth '09), a workshop of the 7th International Conference on Business Process Management (BPM 2009), Ulm, Germany, September 7, 2009.

[ SpringerLink ] [ PDF ]

A Benchmark for Evaluating the Applicability of Software Engineering Techniques to the Improvement of Medical Processes
Stefan Christov, George S. Avrunin, Lori A. Clarke, Leon J. Osterweil, Elizabeth Henneman, Department of Computer Science, University of Massachusetts, Amherst, MA 01003, January 2010. (UM-CS-2010-010)

[ PDF ]

 2008

Considering the Exceptional: Incorporating Exceptions into Property Specifications
Huong Phan, George S. Avrunin, Lori A. Clarke, Department of Computer Science, University of Massachusetts, Amherst, MA 01003, September 2008. (UM-CS-2008-32)

[ PDF ]

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 ]

Combining Symbolic Execution with Model Checking to Verify Parallel Numerical Programs
Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, Lori A. Clarke, ACM Transactions on Software Engineering and Methodology, Vol. 17, No. 2, April 2008, pp.10:1-10:34. (UM-CS-2008-49)

This is an updated version of TR UM-CS-2007-33. This report is a revised and extended version of UM-CS-2005-15, which appeared in ISSTA 2006.

[ ACM ] [ PDF ]

 2007

Engineering Medical Processes to Improve Their Safety: An Experience Report
Leon J. Osterweil, George S. Avrunin, Bin Chen, Lori A. Clarke, Rachel Cobleigh, Elizabeth A. Henneman, Philip L. Henneman, Proceedings IFIP Working Group 8.1 Working Conference on Situational Method Engineering: Fundamentals and Experiences, J. Ralyte, S. Brinkkemper, and B. Henderson-Sellers, eds., Springer, Sept. 2007, Vol. 244, pp. 267-282. (Method Engineering 2007, Geneva. (UM-CS-2007-35)

[ Springer ] [ PDF ] [ Slides ]

 2006

User Guidance for Creating Precise and Accessible Property Specifications
Rachel L. Cobleigh, George S. Avrunin, Lori A. Clarke, ACM SIGSOFT 14th International Symposium on Foundations of Software Engineering (FSE14), Portland, OR, pp. 208-218, November 2006. (UM-CS-2006-27)

This is an updated version originally dated April 2006.

[ ACM ] [ PDF ] [ Slides ]

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 ]

Using Model Checking with Symbolic Execution to Verify Parallel Numerical Programs
Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, Lori A. Clarke, ACM SIGSOFT 2006 International Symposium on Software Testing and Analysis (ISSTA '06) Portland, ME, pp. 157 - 168. (UM-CS-2005-15)

This is a revised and expanded version of UM-CS-2005-15, originally dated Feb. 2005. Please see "Combining Symbolic Execution with Model Checking to Verify Parallel Numerical Programs" UM-CS-2008-49 for a revised and extended version of this report.

[ ACM ] [ PDF ] [ 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 ]

Architectural Building Blocks for Plug-and-Play System Design
Shangzhu Wang, George S. Avrunin, Lori A. Clarke, 9th International Symposium on Component-Based Software Engineering (CBSE'06), Vasteras, Sweden. Springer-Verlag Lecture Notes in Computer Science, Vol. 4063, pp. 98-113, June 29-July 1, 2006. (UM-CS-2005-34)

[ SpringerLink ] [ PDF ] [ Slides ]

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 ]

Automatic Fault Tree Derivation from Little-JIL Process Definitions
Bin Chen, George S. Avrunin, Lori A. Clarke, Leon J. Osterweil, 2006 Software Process Workshop (SPW 2006) and 2006 Process Simulation Workshop (PROSIM 2006), Shanghai, China, Springer-Verlag LNCS, Vol. 3966, pp. 150-158, May, 2006. (UM-CS-2006-01)

[ SpringerLink ] [ PDF ] [ Slides ]

Property Inference from Program Executions
Richard M. Chang, George S. Avrunin, Lori A. Clarke, Department of Computer Science, University of Massachusetts, Amherst, MA 01003, April 2006. (UM-CS-2006-26)

[ PDF ]

Complex Medical Processes as Context for Embedded Systems
George S. Avrunin, Lori A. Clarke, Elizabeth A. Henneman, Leon J. Osterweil, ACM SIGBED Review, special issue from the Workshop on Innovative Techniques for Certification of Embedded Systems, Vol. 3, Issue 4, pp. 9-14, October 2006.. (UM-CS-2006-31)

[ ACM ] [ PDF ] [ Slides ]

 2004

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 ]

Modeling MPI Programs for Verification
Stephen F. Siegel, George S. Avrunin, Department of Computer Science, University of Massachusetts, Amherst, MA 01003, September 2004. (UM-CS-2004-075)

This is an updated and extended version of the report: "Analysis of MPI Programs" (UM-CS-2003-060).

[ PDF ]

Heuristic-Based Model Refinement for FLAVERS
Jianbin Tan, George S. Avrunin, Lori A. Clarke, 26th International Conference on Software Engineering (ICSE 2004), Edinburgh, Scotland, pp. 635-644, May 2004. (UM-CS-2003-029)

[ ACM ] [ PDF ]

Verification of MPI-based Software for Scientific Computation
Stephen F. Siegel, George S. Avrunin, Model Checking Software: 11th International SPIN Workshop, Barcelona, Spain, Springer Verlag Lecture Notes in Computer Science, Vol. 2989, pp. 286-303, April 2004. (UM-CS-2004-087)

[ SpringerLink ] [ PDF ]

 2003

Analysis of MPI Programs
Stephen F. Siegel, George S. Avrunin, Department of Computer Science, University of Massachusetts, Amherst, MA 01003, November 2003. (UM-CS-2003-060)

Please see "Modeling MPI Programs for Verification" (UM-CS-2004-075) for an updated and extended version of this report.

[ PDF ]

From Natural Language Requirements to Rigorous Property Specifications
Rachel L. Smith, George S. Avrunin, Lori A. Clarke, Monterey Workshop 2003 (Workshop on Software Engineering for Embedded Systems (SEES 2003) From Requirements to Implementation, Chicago, IL, pp. 40-46, September 2003 . (UM-CS-2004-019)

[ PDF ] [ Slides ]

 2002

PROPEL: An Approach Supporting Property Elucidation
Rachel L. Smith, George S. Avrunin, Lori A. Clarke, Leon J. Osterweil, 24th International Conference on Software Engineering (ICSE 2002), Orlando, FL, pp. 11-21, May 2002. (UM-CS-2001-046)

[ PostScript ] [ PDF ]

 2000

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 ]

 1999

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 ]

An Efficient Algorithm for Computing MHP Information for Concurrent Java Programs
Gleb Naumovich, George S. Avrunin, Lori A. Clarke, 7th European Software Engineering Conference (ESEC 1999) and the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 7), Toulouse, France, Springer Verlag Lecture Notes in Computer Science #1687, pp. 338-354, September. (UM-CS-1998-044)

[ PostScript ] [ PDF ] [ ACM ]

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 ]

 1998

Analyzing Partially-Implemented Real-Time Systems
George S. Avrunin, James C. Corbett, Laura K. Dillon, 19th International Conference on Software Engineering (ICSE 1997), Boston, MA, pp. 228-238, August 1996. (UM-CS-1996-062)

Updated version in IEEE Transactions on Software Engineering 24(8), August 1998, pp. 602-614.

[ 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 ]

 1997

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 ]

 1996

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 ]

Symbolic Model Checking Using Algebraic Geometry
George S. Avrunin, Computer Aided Verification (CAV 1996), New Brunswick, NJ, Springer Verlag Lecture Notes in Computer Science #1102, pp. 26-37, July 1996. (UM-CS-1996-018)

[ PostScript ] [ PDF ]

 1994

Towards Scalable Compositional Analysis
James C. Corbett, George S. Avrunin, Second ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 53-61, New Orleans, December 1994. ACM Press (Appeared in Software Engineering Notes, 19(5)). (INCA-1994-A)

Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems
George S. Avrunin, James C. Corbett, Laura K. Dillon, Jack C. Wileden, IEEE Transactions on Software Engineering, 20(9):708-719, September 1994. (INCA-1994-B)

 1993

A Practical Technique for Bounding the Time Between Events in Concurrent Real-Time Systems
James C. Corbett, George S. Avrunin, ACM SIGSOFT 1993 International Symposium on Software Testing and Analysis (ISSTA 1993), Cambridge, MA, pp. 110-116, June 1993. (UM-CS-1993-CA)

[ PDF ]

 1992

Sharpening the Bounds on Time Between Events in Maximally Parallel Systems
George S. Avrunin, Department of Computer Science, University of Massachusetts, Amherst, MA 01003, September 1992. (UM-CS-1992-069)

[ PostScript ] [ PDF ]

 1991

Automated Analysis of Concurrent Systems with the Constrained Expression Toolset
George S. Avrunin, Ugo A. Buy, James C. Corbett, Laura K. Dillon, Jack C. Wileden, IEEE Transactions on Software Engineering, 17(11), pp. 1204-1222, November 1991. (UM-CS-1990-116)

[ Compressed PostScript ] [ PDF ]

 1990

Automated Analysis of Concurrent and Real-time Software
George S. Avrunin, Jack C. Wileden, Foundations of Real-Time Computing: Formal Specifications and Methods Washington, DC Kluwer Academic Publishers, A. M. Van Tilborg, G. M. Koob (eds.), 1991, pp. 195-215 October 1990. (UM-CS-1990-118)

Also appears in the 3rd Annual Workshop on Foundations of Real-Time Computing.

[ 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 Laboratory for Advanced Software Engineering Research.
© 2011 University of Massachusetts AmherstSite Policies