Automated Methods for Verification of Concurrent Software Systems

University Of Illinois At Chicago, Chicago IL

Investigators

Abstract

CCR 9988884 Title: Automated Methods in the Analysis and Verification of Concurrent Systems PI: A. Prasad Sistla Abstract: The project investigates various methods, based on temporal logic model-checking, for automated analysis of concurrent and distributed systems including security verification of Internet based applications such as e-commerce. Hybrid techniques, employing symmetry and partial order based methods, will be investigated for containing the state explosion and for checking both safety and liveness properties. The project also considers work on verification of systems composed of arbitrary number of processes. Verification of such systems with different network topologies will be explored. As part of this work, induction based techniques as well as algorithmic techniques will be developed. The security verification will consider different security properties, intruder and protocol models. The project emphasizes both basic research as well as experimental work in the form of implementation and application to real-world problems.