Automated Methods for Verification of Concurrent Software Systems

点击翻译按钮获取中文摘要

CCR 9988884 Title: Automated Methods in the Analysis and Verification of Concurrent Systems PI: A. Prasad SistlaAbstract: The project investigates various methods, based on temporal logic model-checking, for automatedanalysis of concurrent and distributed systems includingsecurity verification of Internet based applications suchas e-commerce.Hybrid techniques, employing symmetry and partial order basedmethods, will be investigated for containingthe 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 systemswith different network topologies will be explored. As part of this work, induction based techniques as well asalgorithmic techniques will be developed. The security verification willconsider different security properties, intruder and protocol models.The project emphasizes both basic research as well as experimental work in the form of implementationand application to real-world problems.