George Avrunin

He/Him

Professor Emeritus

Faculty,
Emeritus Faculty
photo of George Avrunin
Contact
Email
Email
Personal Webpage
Location
LGRT 1335D

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.  Much of his work has involved 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.  His recent work focuses on the modeling and analysis of human-intensive systems, those in which human participants cooperate with hardware and software components to carry out the mission of the system.   Avrunin's work has involved complex medical and election processes, where formal definition and analysis of the processes can help reduce both medical errors and cost and can increase the security of elections, and is currently aimed at providing patient-, clinician-, and context-aware guidance in cardiac surgery.

His research has been supported by grants from the National Science Foundation, the Office of Naval Research, the Army Research Office, the National Institute of Standards and Technology, and the National Institutes of Health.  In 2006, he was named a Distinguished Scientist by the Association for Computing Machinery.  His 1999 paper with M. B. Dwyer and J. C. Corbett won the 2021 Impact Paper Award from the ACM Special Interest Group on Software Engineering for "enabling widespread use of temporal logic for program verification by raising the level of abstraction to common patterns." (The ACM's Guide to the Computing Literature lists the paper as the third-most cited paper in software engineering.)

Professor Avrunin was General Chair of the 2004 ACM International Symposium on Software Testing and Analysis and was a member of the editorial board of the ACM Transactions on Software Engineering and Methodology from 2005 through 2012. He was Associate Head of the Department of Mathematics and Statistics from 2002 to 2008 and 2016 to 2018, and Head from 2008 to 2011, as well as Acting Head in 2005 and 2017.

He was also the lead Principal Investigator on the National Science Foundation Math and Science Partnership grant that provided initial funding for the Western Massachusetts Mathematics Partnership, a partnership of teachers and administrators from local school districts and faculty from area colleges working to improve the teaching and learning of mathematics at all levels in Western Massachusetts.  Although the NSF funding has ended, the WMMP continues to sponsor a variety of activities with support from  Mount Holyoke College and various school districts.  Avrunin continues to participate in the work of the WMMP, including its K-16 Professional Learning Communities.

Education

Ph.D. University of Michigan, 1976

M.A. University of Michigan, 1974

B.S. University of Michigan, 1972

RESEARCH INTERESTS

Modeling and analysis of distributed and concurrent systems, including those with human participants

Selected Publications

  • C. H. Coombs, G. S. Avrunin.  Single-peaked functions and the theory of preference.  Psychological Review 84:216-230, 1977.
  • G. S. Avrunin, L. L. Scott. Quillen stratification for modules. Inventiones Mathematicae 66:277-286, 1982.
  • C. H. Coombs, G. S. Avrunin. The Structure of Conflict, Lawrence Erlbaum Associates, Hillsdale, NJ, 1988.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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, 326-334, Paris, October 2007.
  • 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.
  • W. C. Mertens, S. C. Christov, G. S. Avrunin, L. A. Clarke, L. J. Osterweil, L. J. Cassells, J. L. Marquard. Using process elicitation and validation to understand and improve chemotherapy ordering and delivery. Joint Commission Journal on Quality and Patient Safety, 38(11):497-505, 2012.
  • L. J. Osterweil, M. Bishop, H. M. Conboy, H. Phan, B. I. Simidchieva, G. S. Avrunin, L. A. Clarke, and S. Peisert. Iterative analysis to improve key properties of critical human-intensive processes: An election security example. ACM Transactions on Privacy and Security, 20(2):Article 5, 31 pages, March 2017.
  • G. S. Avrunin, S. C. Christov, L. A. Clarke, H. M. Conboy, L. J. Osterweil, and M. A. Zenati.  Process driven guidance for complex surgical procedures.  In American Medical Informatics Association Annual Symposium, 175-184, November 2018.