Static and Dynamic Formal Analysis of Concurrent Systems and Languages: A SemanticsBased Approach

Concurrency is ubiquitous in modern software. The computing base of systems software, including operating systems and databases, has always been highly concurrent and with the introduction of language-level thread primitives in languages like Java and C # and the advent of distributed web services, concurrency has become commonplace even in application software. The design of concurrent software is notoriously error-prone due to the nondeterministic interaction among concurrently executing threads. Therefore, it is important to develop techniques for specifying correctness properties of concurrent software and tools for automatically checking these properties. A burning problem in program verification today is how to model the world of concurrent systems. The excellent models of sequential behavior that have evolved during the past thirty years of sequential program verification do not adequately reflect the nature of a concurrent universe. In this work, we present solutions to the commonly know problems of concurrency by using appropriate semantic models for concurrency, namely rewriting logic, and traces and Petri nets. We argue that using the appropriate semantic model helps one to define the problem in a simple, intuitive, and effective way in the first place, and then provides sound solutions for these now well-defined problems. This work addresses some verification problems for concurrent programs and systems