Static and dynamic formal analysis of concurrent systems and languages: A semantics-based approach

Concurrency is ubiquitous in modern 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. In this dissertation, 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. The approaches presented here fall into two main category of static versus dynamic verification.; In the dynamic category, we use rewriting logic as a true concurrency model to specify concurrent programs and systems. We developed the tool JavaFAN based on rewriting logic semantics of Java at both language and bytecode level. We provide a methodology in which formal semantics is then used as a basis to develop formal analyses tools for analyzing programs in any language, in the case of JavaFAN tool for Java programs at both levels. We furthermore advance these ideas by developing a generic partial order reduction module that with minimum effort can be added to any language specification and automatically enrich it with POR capabilities. We take this idea even further by providing reduction methods that can work on the specification of any concurrent system. Experimental result suggest that these methods are very effective in practice.; In the static category, the focus of this work is to provide an appropriate notion of static abstraction for concurrent programs, called control net, based on Petri nets which is used to show how two very important static analyses problems in the context of concurrency, namely atomicity and dataflow analyses can be defined for the partially-ordered runs generated by the control net, and how clean algorithmic solutions can be provided to solve these problems. Experimental results suggest that these solutions are feasible in practice.