|
George Avrunin, Professor; Department Head |
 |
|
|
| Personal Webpage |
|
| Office | LGRT 1623E | | Phone | (413) 545-0510 | | Fax | (413) 545-1801 | | Email | avrunin <at> math.umass.edu | |
| Mailing Address |
| Department of Mathematics and Statistics |
| Lederle Graduate Research Tower |
| University of Massachusetts |
| Amherst, MA 01003-9305 |
|
|
|
|
| Education | | Ph.D. | University of Michigan, 1976 |
|
| | M.A. | University of Michigan, 1974 |
|
| | B.S. | University of Michigan, 1972 |
|
|
|
| Research Interests: Analysis and verification of concurrent and distributed computer systems |
|
| Professor Avrunin's research has ranged from the cohomology and
representation theory of finite groups to utility theory and models of
individual choice and social conflict. Most recently, he has been
developing methods for determining whether any execution of a
concurrent or distributed system can violate a given property or
requirement. This work focuses on finite-state verification: techniques
that involve construction and analysis of suitable finite models that
represent all possible executions of the system under
consideration. As part of this work, he also studies problems related
to the precise specification of the requirements the system must
meet. He is currently involved in projects investigating the
application of finite-state verification techniques to
high-performance scientific computing applications and to complex
medical processes, where formal definition and analysis of the
processes can help reduce both medical errors and cost.
He was General Chair of the 2004 ACM International Symposium on
Software Testing and Analysis, is a member of the editorial board of
the ACM Transactions on Software Engineering and Methodology, and has
served on many program committees for software engineering
conferences. His research has been supported by grants from the
National Science Foundation, the Office of Naval Research, and the
Army Research Office. In 2006, he was named an ACM Distinguished
Scientist. |
|
| Selected Publications |
| S. Wang, G. S. Avrunin, L. A. Clarke. Plug-and-play architectural design and verification.
In R. de
Limos, F. Di Giandomenico, C. Gacek, H.
Muccini, and M. Vieira, editors, Architecting Dependable
Systems V, number 5135 in Lecture Notes in Computer Science, pages 273--297, Springer, 2008.
|
|
| E. A. Henneman, R. L. Cobleigh, G. S. Avrunin, L. A. Clarke, L. J. Osterweil, P. L. Henneman. Designing property specifications to improve the safety of the blood transfusion process. Transfusion Medicine Reviews, 22(4):291-299, 2008. |
|
| B. Chen, G. S. Avrunin,
E. A. Henneman, L. A. Clarke, L. J. Osterweil, P.
L. Henneman. Analyzing medical processes. In Proceedings of the 30th International
Conference on Software Engineering, pages 623-632, Leipzig, May 2008.
|
|
| S. F. Siegel, A. Mironova, G. S. Avrunin, L. A. Clarke. Combining symbolic execution with model checking to verify parallel numerical programs. ACM
Transactions on Software Engineering and Methodology, 17(2):
Article 10, 1-34, 2008. |
|
| J. M. Cobleigh, G. S. Avrunin, L. A. Clarke. Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Transactions on Software
Engineering and Methodology, 17(2): Article 7, 1-52, 2008. |
|
| S. F. Siegel, G. S. Avrunin. Verification of halting properties for MPI programs using
nonblocking operations.
In F. Capello, T. Herault, and J. 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. |
|
| E. A. Henneman, G. S. Avrunin, L. A. Clarke, L. J. Osterweil, C. Andrzejewski, Jr., K. Merrigan, R.Cobleigh, K. Frederick, E. Katz-Basset, P. L. Henneman. Increasing patient safety and efficiency in transfusion therapy using formal process definitions. Transfusion Medicine Reviews, 21(1), 2007, 49-57. |
|
| R. L. Cobleigh, G. S. Avrunin, L. A. Clarke. User guidance for creating precise and accessible property specifications. Proceedings of the 14th ACM SIGSOFT Symposium on the Foundations of Software Engineering, 208-218, Portland, OR, 2006.
|
|
| J. Tan, G. S. Avrunin, L. A. Clarke. Managing space for finite-state verification. Proceedings of the 28th International Conference on Software Engineering, 152-161, Shanghai, 2006. |
|
| S. F. Siegel, G. S. Avrunin. Modeling wildcard-free MPI programs for verification. Proceedings of the ACM Symposium on Principles and Practice of Parallel Programming, 95-106 Chicago, 2005. |
|
| R. L. Smith, G. S. Avrunin, L. A. Clarke, L. J. Osterweil. PROPEL: An approach supporting property elucidation. Proceedings of the 24th International Conference on Software Engineering, 11-21, Orlando, FL, 2002. |
|
| M. B. Dwyer, G. S. Avrunin, J. C. Corbett. Patterns in property specifications for finite-state verification. Proceedings of the 21st International Conference on Software Engineering, 411-420, Los Angeles, 1999. |
|
| G. S. Avrunin. Symbolic model checking using algebraic geometry. Proceedings of the 8th International Conference on Computer-Aided Verification, 26-37, New Brunswick, NJ, 1996. |
|
| J. C. Corbett, G. S. Avrunin. Using integer programming to verify general safety and liveness properties. Formal Methods in System Design, 6:97-123, 1995. |
|
| C. H. Coombs, G. S. Avrunin. The Structure of Conflict, Lawrence Erlbaum Associates, Hillsdale, NJ, 1988. |
|
| G. S. Avrunin, L. L. Scott. Quillen stratification for modules. Inventiones Mathematicae 66:277-286, 1982. |
|
