![[Back]](/icons/back.gif){kind=icon}
Back to George Avrunin's home page
Designing property specifications to improve the safety of the blood transfusion process. Elizabeth A. Henneman, Rachel Cobleigh, George S. Avrunin, Lori A. Clarke, Leon J. Osterweil, and Philip L. Henneman. Transfusion Medicine Reviews, to appear.
Plug-and-play architectural design and verification. Shangzhu Wang, George S. Avrunin, and Lori A. Clarke. In Rogerio de Limos, Felicita Di Giandomenico, Cristina Gacek, Henry Muccini, and Marlon Vieira, editors, Architecting Dependable Systems V, number 5135 in LNCS, pages 273--297. Springer, 2008.
Analyzing medical processes. Bin Chen, George S. Avrunin, Elizabeth A. Henneman, Lori A. Clarke, Leon J. Osterweil, and Philip L. Henneman. In Proceedings of the 30th International Conference on Software Engineering, pages 623-632, Leipzig, May 2008.
Using software technology to improve the quality of medical processes (Keynote Address). Lori A. Clarke, George S. Avrunin, and Leon J. Osterweil. In Companion of the 30th International Conference on Software Engineering, pages 889-898, Leipzig, May 2008.
Combining symbolic execution with model checking to verify parallel numerical programs. Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, and Lori A. Clarke. ACM Transactions on Software Engineering and Methodology, 17(2): Article 10, 1--34, 2008.
Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. Jaimeson M. Cobleigh, George S. Avrunin, and Lori A. Clarke. ACM Transactions on Software Engineering and Methodology, 17(2): Article 7, 1--52, 2008.
Verification of halting properties for MPI programs using nonblocking operations. Stephen F. Siegel and George S. Avrunin. In Franck Capello, Thomas Herault, and Jack Dongarra, editors Recent Advances in Parallel Virtual Machine and Message Passing Interface: 14th European PVM/MPI Users' Group Meeting, volume 4757 of Lecture Notes in Computer Science, pages 326-334, Paris, October 2007.
Rigorously defining and analyzing medical processes: An experience report. Stefan Christov, Bin Chen, George S. Avrunin, Lori A. Clarke, Leon J. Osterweil, David Brown, Lucinda Cassells, and Wilson Mertens. In Workshop on Model-Based Trustworthy Health Information Systems, Nashville, September 2007.
Engineering medical processs to improve their safety: An experience report. Leon J. Osterweil, George S. Avrunin, Bin Chen, Lori A. Clarke, Rachel L. Cobleigh, Elizabeth A. Henneman, and Philip L. Henneman. In J. Ralyte, S. Brinkemper, and B. Henderson-Seelers, editors Proceedings of the IFIP WG8.1 Working Conference on Situational Method Engineering: Fundamentals and Experiences (ME07), pages 267-282, Geneva, September 2007.
Increasing patient safety and efficiency in transfusion therapy using formal process definitions. Elizabeth A. Henneman, George S. Avrunin, Lori A. Clarke, Leon J. Osterweil, Chester Andrzejewski, Jr., Karen Merrigan, Rachel Cobleigh , Kimberly Frederick, Ethan Katz-Bassett, and Phillip L. Henneman. Transfusion Medicine Reviews, volume 21, number 1, January 2007, pages 49-57.
User guidance for creating precise and accessible property specifications. Rachel L. Cobleigh, George S. Avrunin, and Lori A. Clarke. In Proceedings of the 14th ACM Symposium on the Foundations of Software Engineering, pages 208-218, Portland, OR, November 2006.
Breaking up is hard to do: An investigation of decomposition for assume-guarantee reasoning. Jamieson M. Cobleigh, George S. Avrunin, and Lori A. Clarke. In Lori Pollock and Mauro Pezzé, editors, Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 97-108, Portland, ME, July 2006.
Using model checking with symbolic execution to verify parallel numerical programs. Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, and Lori A. Clarke. In Lori Pollock and Mauro Pezzé, editors, Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 157-168, Portland, ME, July 2006.
Property inference from program executions. Richard M. Chang, George S. Avrunin, and Lori A. Clarke. Technical report UM-CS-2006-26, Department of Computer Science, University of Massachusetts, 2006.
Verification support for plug-and-play architectural design. Shangzhu Wang, George S. Avrunin, and Lori A. Clarke. Technical Report UMCS-2006-32, Department of Computer Science, University of Massachusetts, 2006. Extended abstract in Proceedings the Workshop on the Role of Software Architecture in Testing and Analysis, Portland, ME, July 2006.
Architectural building blocks for plug-and-play system design. Shangzhu Wang, George S. Avrunin, and Lori A. Clarke. In Ian Gorton, George T. Heineman, Ivica Crnkovic, Heinz W. Schmidt, Judith A. Stafford, Clemens A. Szyperski, and Kurt Wallnau, editors, Proceedings of the 9th International SIGSOFT Symposium on Component-Based Software Engineering (CBSE 2006), number 4063 in LNCS, pages 98--113, Västerås, Sweden, June 2006.
Managing space for finite-state verification. Jianbin Tan, George S. Avrunin, and Lori A. Clarke. In Proceedings of the 28th International Conference on Software Engineering, pages 152-161, Shanghai, May 2006.
Automatic fault tree derivation from Little-JIL process definitions. Bin Chen, George S. Avrunin, Lori A. Clarke, and Leon J. Osterweil. In Qing Wang, Dietmar Pfahl, David M. Raffo, and Paul Werinck, editors, Software Process Change: Proceedings of The International Software Process Workshop and the International Workshop on Software Process Simulation and Modeling (SPW/ProSim 2006), number 3966 in LNCS, 150--158, Shanghai, May 2006.
Complex medical processes as context for embedded systems. George S. Avrunin, Lori A. Clakre, Elizabeth A. Henneman, and Leon J. Osterweil. In Proceedings of the Workshop on Innovative Techniqes for Certification of Embedded Systems, San Jose, April 4, 2006. (Proceedings published in SIGBED Review 3(4), 2006.)
Modeling wildcard-free MPI programs for verification. Stephen F. Siegel and George S. Avrunin. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practices of Parallel Programming, pages 95-106, Chicago, June 2005.
Finite-state verification for high performance computing. George S. Avrunin, Stephen F. Siegel, and Andrew R. Siegel. In Proceedings of the Second International Workshop on Software Engineering for High Performance Computing System Applications, pages 68-73, St. Louis, May 2005.
Process programming to support medical safety: A case study on blood transfusion. Lori A. Clarke, Yao Chen, George S. Avrunin, Bin Chen, Rachel Cobleigh, Kim Frederick, Elizabeth A. Henneman, and Leon J. Osterweil. In Proceedings of the Software Process Workshop, Beijing, May 2005, LNCS volume 3840, pages 347-359.
Heuristic-guided counterexample search in FLAVERS. Jianbin Tan, George S. Avrunin, Lori A. Clarke, Shlomo Zilberstein, and Stefan Leue. In Proceedings of the 12th ACM Symposium on the Foundations of Software Engineering, pages 201-210, Newport Beach, CA, November 2004.
Heuristic-based model refinement for FLAVERS. Jianbin Tan, George S. Avrunin, and Lori A. Clarke. In Proceedings of the 26th International Conference on Software Engineering, pages 635-644, Edinburgh, May 2004.
Verification of MPI-based software for scientific computation. Stephen F. Siegel and George S. Avrunin. In Proceedings of the 11th International SPIN Workshop on Model Checking Software, Barcelona, April 2004, LNCS volume 2989, pages 286-303.
From natural language requirements to rigorous property specifications. Rachel L. Smith, George S. Avrunin, and Lori A. Clarke. In Workshop on Software Engineering for Embedded Systems (SEES 2003): From Requirements to Implementation, pages 40-46, Chicago, IL, September 2003.
Analysis of MPI programs. Stephen F. Siegel and George Avrunin. Technical Report UM-CS-2003-036, Department of Computer Science, University of Massachusetts Amherst. 2003.
PROPEL: An approach supporting property elucidation. Rachel L. Smith, George S. Avrunin, Lori A. Clarke, and Leon J. Osterweil. In Proceedings of the 24th International Conference on Software Engineering, Orlando, FL, May 2002, pages 11-21.
A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel for rendezvous-based concurrent programs. Gleb Naumovich and George S. Avrunin.
Improving the precision of INCA by eliminating solutions with spurious cycles. Stephen F. Siegel and George S. Avrunin. IEEE Transactions on Software Engineering, volume 28, number 2, February 2002, pages 115-128.
Improving the precision of INCA by preventing spurious cycles. Stephen F. Siegel and George S. Avrunin. In M. J. Harrold, editor, Proceedings of the International Symposium on Software Testing and Analysis (ISSTA '00), Portland, OR, August 2000, pages 191-200.
Benchmarking finite-state verifiers. George S. Avrunin, James C. Corbett, and Matthew B. Dwyer. Software Tools for Technology Transfer, 2(4):317-320, 2000.
Comparing finite-state verification techniques for concurrent software. George S. Avrunin, James C. Corbett, Matthew B. Dwyer, Corina S. Pasareanu, and Stephen F. Siegel. Technical Report UM-CS-1999-069, Department of Computer Science, University of Massachusetts, November 1999.
An efficient algorithm for computing MHP information for concurrent Java programs. Gleb Naumovich, George S. Avrunin, and Lori A. Clarke. In O. Nierstrasz and M. Lemoine, editors, Software Engineering--ESEC/FSE '99. 7th European Software Engineering Conference held jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, volume 1687 of Lecture Notes in Computer Science, pages 338-354, Toulouse, September 1999. Springer-Verlag.
Patterns in property specifications for finite-state verification. Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. In Proceedings of the Twenty-First International Conference on Software Engineering, pages 411-420, Los Angeles, May 1999.
Data flow analysis for checking properties of concurrent Java programs. Gleb Naumovich, George S. Avrunin, and Lori A. Clarke. In Proceedings of the Twenty-First International Conference on Software Engineering, pages 399-410, Los Angeles, May 1999.
A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel. Gleb Naumovich and George S. Avrunin. In Proceedings of 6th International Symposium on the Foundations of Software Engineering, pages 24-34, November 1998.
Analyzing partially-implemented real-time systems. George S. Avrunin, James C. Corbett, and Laura K. Dillon. IEEE Transactions on Software Engineering, 24(8):602-614, August 1998. (This is a revised and expanded version of a paper of the same title appearing in the Proceedings of the International Conference on Software Engineering, Boston, May 1997, 228-238.)
Property specification patterns for finite-state verification. Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. In Mark Ardis, editor, Proceedings of FMSP '98, the Second Workshop on Formal Methods in Software Practice, pages 7-15, Clearwater Beach, FL, March 1998.
Applying static analysis to software architectures. Gleb Naumovic, George S. Avrunin, Lori A. Clarke, and Leon J. Osterweil. In Mehdi Jazayeri and Helmut Schauer, editors, Software Engineering--ESEC/FSE '97, volume 1301 of Lecture Notes in Computer Science, pages 77-93, Zurich, September 1997. Springer Verlag.
An empirical comparison of static concurrency analysis techniques. A. T. Chamillard, Lori A. Clarke, and George S. Avrunin. Technical Report 96-84, Department of Computer Science, University of Massachusetts, 1996. Revised May 1997.
Symbolic model checking using algebraic geometry. George S. Avrunin. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification, 8th International Conference, volume 1102 of Lecture Notes in Computer Science, pages 26-37, New Brunswick, NJ, July/August 1996. Springer-Verlag.
Using integer programming to verify general safety and liveness properties. James C. Corbett and George S. Avrunin. Formal Methods in System Design, 6:97-123, January 1995.
Towards scalable compositional analysis. James C. Corbett and George S. Avrunin. In David Wile, editor, Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 53-61, New Orleans, December 1994. ACM Press (Proceedings appeared in Software Engineering Notes, 19(5)).
Automated derivation of time bounds in uniprocessor concurrent systems. George S. Avrunin, James C. Corbett, Laura K. Dillon, and Jack C. Wileden. IEEE Transactions on Software Engineering, 20(9):708-719, September 1994.
Real-time state machines and circuit verification with modal functions. Victor Yodaiken and George S. Avrunin. Technical Report 93-04, Department of Computer Science, University of Massachusetts at Amherst, 1993.
Nilpotency degree of cohomology rings in characteristic two. George S. Avrunin and Jon F. Carlson. Proc. Amer. Math. Soc., 118(2):239-343, 1993.
A practical method for bounding the time between events in concurrent real-time systems. James C. Corbett and George S. Avrunin. In Thomas Ostrand and Elaine Weyuker, editors, Proceedings of the 1993 International Symposium on Software Testing and Analysis (ISSTA), pages 110-116, Cambridge, MA, June 1993. ACM Press (Proceedings appeared in Software Engineering Notes, 18(3)).
Sharpening bounds on the time between events in maximally parallel systems. George S. Avrunin. Technical Report 92-69, Department of Computer Science, University of Massachusetts at Amherst, 1992.
Automated analysis of concurrent systems with the constrained expression toolset. George S. Avrunin, Ugo A. Buy, James C. Corbett, Laura K. Dillon, and Jack C. Wileden. IEEE Transactions on Software Engineering, 17(11):1204-1222, November 1991.
Experiments with an improved constrained expression toolset. George S. Avrunin, Ugo A. Buy, James C. Corbett, Laura K. Dillon, and Jack C. Wileden. In Proceedings of the Symposium on Testing, Analysis, and Verification (TAV4), pages 178-187. ACM SIGSOFT, October 1991.
Integer programming in the analysis of concurrent systems. George S. Avrunin, Ugo A. Buy, and James C. Corbett. In Kim Guldstand Larsen and Arne Skou, editors, Computer Aided Verification, 3rd International Workshop Proceedings, volume 575 of Lecture Notes in Computer Science, pages 92-102, Aalborg, Denmark, July 1991. Springer-Verlag.
Improvements in automated analysis of concurrent and real-time software. George S. Avrunin and Jack C. Wileden. In André M. van Tilborg and Gary M. Koob, editors, Foundations of Real-Time Computing: Formal Specifications and Methods, chapter 8, pages 195-215. Kluwer Academic Publishers, 1991.
Automatic generation of inequality systems for constrained expression analysis. George S. Avrunin Ugo Buy and James Corbett. Technical Report 90-32, Department of Computer and Information Science, University of Massachusetts, Amherst, 1990.
Constrained expression analysis of real-time systems. George S. Avrunin, Laura K. Dillon, and Jack C. Wileden. Technical Report 89-50, Department of Computer and Information Science, University of Massachusetts, 1989.
Experiments with automated constrained expression analysis of concurrent software systems. George S. Avrunin, Laura K. Dillon, and Jack C. Wileden. In Richard A. Kemmerer, editor, Proceedings of the ACM SIGSOFT '89 Third Symposium on Software Testing, Analysis and Verification, pages 124-130, December 1989. Appeared as Software Engineering Notes, 14(8).
The Structure of Conflict. Clyde H. Coombs and George S. Avrunin. Lawrence Erlbaum Associates, Hillsdale, NJ, 1988.
A prototype inequality generator. George S. Avrunin. Software Development Laboratory Memo 88-1, Department of Computer and Information Science, University of Massachusetts, Amherst, June 1988.
Constrained expressions: Toward broad applicability of analysis methods for distributed software systems. Laura K. Dillon, George S. Avrunin, and Jack C. Wileden. ACM Trans. Prog. Lang. Syst., 10(3):374-402, July 1988.
Toward automating analysis support for developers of distributed software. Jack C. Wileden and George S. Avrunin. In Proceedings of the Eighth International Conference on Distributed Computing Systems, pages 350-357. IEEE Computer Society Press, June 1988.
Experiments in constrained expression analysis. George S. Avrunin. Technical Report 87-125, Department of Computer and Information Science, University of Massachusetts, Amherst, 1987.
Constrained expressions: Adding analysis capabilities to design methods for concurrent software systems. George S. Avrunin, Laura K. Dillon, Jack C. Wileden, and William E. Riddle. IEEE Trans. Softw. Eng., SE-12(2):278-292, 1986. Reprinted in: S. M. Shatz and J.-P. Wang, eds., Tutorial: Distributed-Software Engineering, IEEE Computer Society Press, Washington, DC (1989), pp. 258-271.
Describing and analyzing distributed software system designs. George S. Avrunin and Jack C. Wileden. ACM Trans. Prog. Lang. Syst., 7(3):380-403, July 1985.
Algebraic techniques for the analysis of concurrent systems. George S. Avrunin and Jack C. Wileden. In Proceedings of the Sixteenth Hawaii International Conference on Systems Sciences, pages 51-57, 1983.
Quillen stratification for modules. George S. Avrunin and Leonard L. Scott. Invent. Math., 66:277-286, 1982.
A Quillen stratification theorem for modules. George S. Avrunin and Leonard L. Scott. Bull. Amer. Math. Soc. (N.S.), 6:75-78, 1982.
Generic cohomology for twisted groups. George S. Avrunin. Trans. Amer. Math. Soc., 268:247-253, 1981.
Annihilators of cohomology modules. George S. Avrunin. J. Algebra, 69:150-154, 1981.
The image of the restriction map on 2-cohomology. George S. Avrunin. Arch. Math. (Basel), 34:502-508, 1980.
2-cohomology of some unitary groups. George S. Avrunin. Ill. J. Math., 24:317-332, 1980.
A vanishing theorem for second degree cohomology. George S. Avrunin. J. Algebra, 53:382-388, 1978.
A theorem on single-peaked preference functions in one dimension. Clyde H. Coombs and George S. Avrunin. J. Math. Psych., 16:261-266, 1977.
Single-peaked functions and the theory of preference. Clyde H. Coombs and George S. Avrunin. Psych. Rev., 84:216-230, 1977. Reprinted in: E. D. Lantermann and H. Feger, eds., Similarity and Choice, Hans Huber Publishers, Bern (1980), pp. 182-207.
Back to George Avrunin's home page