Analysis of execution traces plays a fundamental role in many program analysis approaches, such as runtime verification, testing, monitoring, and specification mining. Execution traces are frequently parametric, i.e., they contain events with parameter bindings. Each parametric trace usually consists of many meaningful trace slices merged together, each slice corresponding to one parameter binding. This gives a semantics-based solution to parametric trace analysis. A general-purpose parametric trace slicing technique is introduced, which takes each event in the parametric trace and dispatches it to its corresponding trace slices. This parametric trace slicing technique can be used in combination with any conventional, non-parametric trace analysis technique, by applying the later on each trace slice. As an instance, a parametric property monitoring technique is then presented. The presented parametric trace slicing and monitoring techniques have been implemented and extensively evaluated. Measurements of runtime overhead confirm that the generality of the discussed techniques does not come at a performance expense when compared with existing parametric trace monitoring systems.

Many C programs assume the use of implicit domain-specific information. A common example is units of measurement, where values can have both a standard C type and an associated unit. However, since there is no way in the C language to represent this additional information, violations of domain-specific policies, such as unit safety violations, can be difficult to detect. In this paper we present a static analysis, based on the use of an abstract C semantics defined using rewriting logic, for the detection of unit violations in C programs. In contrast to typed approaches, the analysis makes use of annotations present in C comments on function headers and in function bodies, leaving the C language unchanged. Initial evaluation results show that performance scales well, and that errors can be detected without imposing a heavy annotation burden.

Specifications carrying formal parameters that are bound to concrete data at runtime can effectively and elegantly capture multi-object behaviors or protocols. Unfortunately, parametric specifications are not easy to formulate by nonexperts and, consequently, are rarely available. This paper presents a general approach for mining parametric specifications from program executions, based on a strict separation of concerns: (1) a trace slicer first extracts sets of independent interactions from parametric execution traces; and (2) the resulting non-parametric trace slices are then passed to any conventional non-parametric property learner. The presented technique has been implemented in jMiner, which has been used to automatically mine many meaningful and non-trivial parametric properties of OpenJDK 6.

Recent developments in runtime verification and monitoring show that parametric regular and temporal logic specifications can be efficiently monitored against large programs. However, these logics reduce to ordinary finite automata, limiting their expressivity. For example, neither can specify structured properties that refer to the call stack of the program. While context-free grammars (CFGs) are expressive and well-understood, existing techniques for monitoring CFGs generate large runtime overhead in real-life applications. This paper demonstrates that monitoring parametric CFGs is practical (with overhead on the order of 12% or lower in most cases). We present a monitor synthesis algorithm for CFGs based on an LR(1) parsing algorithm, modified to account for good prefix matching. In addition, a logic-independent mechanism is introduced to support matching against the suffixes of execution traces.

Parametric properties provide an effective and natural means to describe object-oriented system behaviors, where the parameters are typed by classes and bound to object instances at runtime. Efficient monitoring of parametric properties, in spite of increasingly growing interest due to applications such as testing and security, imposes a highly non-trivial challenge on monitoring approaches due to the potentially huge number of parameter instances. Existing solutions usually compromise their expressiveness for performance or vice versa. In this paper, we propose a generic, in terms of specification formalism, yet efficient, solution to monitoring parametric specifications. Our approach is based on a general algorithm for slicing parametric traces and makes use of static knowledge about the desired property to optimize monitoring. The needed knowledge is not specific to the underlying formalism and can be easily computed when generating monitoring code from the property. Our approach works with any specification formalism, providing better and extensible expressiveness. Also, a thorough evaluation shows that our technique outperforms other state-of-art techniques optimized for particular logics or properties.

Analysis of execution traces plays a fundamental role in many program analysis approaches. Execution traces are frequently parametric, i.e., they contain events with parameter bindings. Each parametric trace usually consists of many trace slices merged together, each slice corresponding to a parameter binding. Several techniques have been proposed to analyze parametric traces, but they have limitations: some in the specification formalism, others in the type of traces they support, moreover, they share common notions, intuitions, even techniques and algorithms, suggesting that a fundamental understanding of parametric trace analysis is needed. This foundational paper gives the first solution to parametric trace analysis that is unrestricted by the type of parametric properties or traces that can be analyzed. First, a general purpose parametric trace slicing technique is discussed, which takes each event in the parametric trace and distributes it to its corresponding trace slices. This parametric trace slicing technique can be used in combination with any conventional, non-parametric trace analysis, by applying the latter on each trace slice. An online monitoring technique is then presented based on the slicing technique, providing a logic-independent solution to runtime verification of parametric properties. The presented monitoring technique has been implemented and extensively evaluated. The results confirm that the generality of the discussed techniques does not come at a performance expense when compared with existing monitoring systems.

Many programs make implicit assumptions about data. Common assumptions include whether a variable has been initialized or can only contain non-null references. Domain-specific examples are also common, with many scientific programs manipulating values with implicit units of measurement. However, in languages like C, there is no language facility for representing these assumptions, making violations of these implicit program policies challenging to detect. In this paper, we present a framework for pluggable policies for the C language. The core of the framework is a shared rewrite-logic semantics of C designed for symbolic execution of C programs, and an annotation engine allowing for annotations across multiple policies to be added to C programs. Policies are created by providing a policy specific language, usable in annotations, and policy specific values and semantics. This provides a method to quickly develop new policies, taking advantage of the existing framework components. To illustrate the use of the framework, two case studies in policy development are presented: a basic null pointer analysis, and a more comprehensive analysis to verify unit of measurement safety.

JPREDICTOR is a tool for detecting concurrency errors in JAVA programs. The JAVA program is instrumented to emit property-relevant events at runtime and then executed. The resulting execution trace is collected and analyzed by JPREDICTOR, which extracts a causality relation sliced using static analysis and refined with lock-atomicity information. The resulting abstract model, a hybrid of a partial order and atomic blocks, is then exhaustively analyzed against the property and errors with counter-examples are reported to the user. Thus, JPREDICTOR can "predict" errors that did not happen in the observed execution, but which could have happened under a different thread scheduling. The analysis technique employed in JPREDICTOR is fully automatic, generic (works for any trace property), sound (produces no false alarms) but it is incomplete (may miss errors). Two common types of errors are investigated in this paper: dataraces and atomicity violations. Experiments show that JPREDICTOR is precise (in its predictions), effective and efficient. After the code producing them was executed only once, JPREDICTOR found all the errors reported by other tools. It also found errors missed by other tools, including static race detectors, as well as unknown errors in popular systems like Tomcat and the Apache FTP server.

This paper presents an approach to mine parametric state-based specifications from execution traces, which can involve multiple components. We first discuss a general framework for mining parametric properties from execution traces, which allows one to apply non-parametric mining algorithms to infer parametric specifications without any modification. Then we propose a novel mining algorithm that extends the Probabilistic Finite State Automata (PFSA) approach to infer finite automata that describe system behaviors concisely and precisely from successful executions. The presented technique has been implemented in a prototype tool for Java, called jMiner, which has been applied to a number of real-life programs, including Java library classes and popular open source packages. Our experiments generated many meaningful specifications and revealed problematic behaviors in some programs, showing the effectiveness of our approach.

Predictive runtime analysis has been proposed to improve the effectiveness of concurrent program analysis and testing. By observing one execution trace of the running system, predictive runtime analysis extracts a causality relation among runtime events, which is then used as an abstract model of the program and checked against desired properties. This way, one can predict concurrency errors without actually hitting them and without re-executing the program. The quality of the extracted causality relation directly determines the effectiveness of predictive runtime analysis. This paper presents an efficient and sound approach to compute sliced causality and sliced atomicity. These significantly improve upon existing causalities: irrelevant causal relationships are removed using an apriori static analysis process based on control and data dependence, and on property relevance and atomicity analysis. The algorithms presented in this paper have been implemented and extensively evaluated. The results show that the proposed technique is effective and sound: we found the previously known concurrency bugs as well as some unknown errors in popular systems, like the Tomcat webserver and the Apache FTP server, without any false alarms.

Happen-before causal partial orders have been widely used in concurrent program verification and testing. This paper presents a parametric approach to happen-before causal partial orders. Existing variants of happen-before relations can be obtained as instances of the parametric framework. A novel causal partial order, called sliced causality, is then defined also as an instance of the parametric framework, which loosens the obvious but strict happen-before relation by considering static and dynamic dependence information about the program. Sliced causality has been implemented in a runtime predictive analysis tool for JAVA, named jPREDICTOR, and the evaluation results show that sliced causality can significantly improve the capability of concurrent verification and testing.

Monitoring-Oriented Programming (MOP1) [21, 18, 22, 19] is a formal framework for software development and analysis, in which the developer specifies desired properties using definable specification formalisms, along with code to execute when properties are violated or validated. The MOP framework automatically generates monitors from the specified properties and then integrates them together with the user-defined code into the original system. The previous design of MOP only allowed specifications without parameters, so it could not be used to state and monitor safety properties referring to two or more related objects. In this paper we propose a parametric specification formalism-independent extension of MOP , together with an implementation of JavaMOP that supports parameters. In our current implementation, parametric specifications are translated into AspectJ code and then weaved into the application using off-the-shelf AspectJ compilers; hence, MOP specifications can be seen as formal or logical aspects. Our JavaMOP implementation was extensively evaluated on two benchmarks, Dacapo [14] and Tracematches [8], showing that runtime verification in general and MOP in particular are feasible. In some of the examples, millions of monitor instances are generated, each observing a set of related objects. To keep the runtime overhead of monitoring and event observation low, we devised and implemented a decentralized indexing optimization. Less than 8% of the experiments showed more than 10% runtime overhead; in most cases our tool generates monitoring code as efficient as the hand-optimized code. Despite its genericity, JavaMOP is empirically shown to be more efficient than runtime verification systems specialized and optimized for particular specification formalisms. Many property violations were detected during our experiments; some of them are benign, others indicate defects in programs. Many of these are subtle and hard to find by ordinary testing.

This paper introduces a framework for rapid prototyping of object oriented programming languages and corresponding analysis tools. It is based on formal definitions of language features in rewrite logic, a simple and intuitive logic for concurrency with powerful tool support. A domain-specific front-end consisting of a notation and a technique, called K, allows for compact, modular, expressive and easy to understand and change definitions of language features. The framework is illustrated by first defining KOOL, an experimental concurrent object-oriented language with exceptions, and then by discussing the definition of JAVA. Generic rewrite logic tools, such as efficient rewrite engines and model checkers, can be used on language definitions and yield interpreters and corresponding formal program analyzers at no additional cost.

This paper introduces a framework for rapid prototyping of object oriented programming languages and corresponding analysis tools. It is based on formal definitions of language features in rewrite logic, a simple and intuitive logic for concurrency with powerful tool support. A domain-specific front-end consisting of a notation and a technique, called K, allows for compact, modular, expressive and easy to understand and change definitions of language features. The framework is illustrated by first defining KOOL, an experimen- tal concurrent object-oriented language with exceptions, and then by discussing the definition of JAVA. Generic rewrite logic tools, such as efficient rewrite engines and model checkers, can be used on language definitions and yield interpreters and corresponding formal program analyzers at no additional cost.

Software specifications are of great use for more rigorous software development. They are useful for formal verification and automated testing, and they improve program understanding. In practice, specifications often do not exist and developers write software in an ad-hoc fashion. We describe a new way to automatically infer specifications from code. Our approach infers a likely specification for any method such that the method’s behavior, i.e., its effect on the state and possible result values, is summarized and expressed in terms of some other methods. We use symbolic execution to analyze and relate the behaviors of the considered methods. In our experiences, the resulting likely specifications are compact and human-understandable. They can be examined by the user, used as input to program verification systems, or as input for test generation tools for validation. We implemented the technique for .NET programs in a tool called Axiom Meister. It inferred concise specifications for base classes of the .NET platform and found flaws in the design of a new library.

A runtime analysis technique is presented, which can predict concurrency errors in multithreaded systems by observing potentially non-erroneous executions. It builds upon a novel causal partial order, sliced causality, that weakens the classic but strict “happensbefore” by using both static information about the program, such as controland data-flow dependence, and dynamic synchronization information, such as lock-sets. A vector clock algorithm is introduced to automatically extract a sliced causality from any execution. A memory-efficient procedure then checks all causally consistent potential runs against properties given as monitors. If any of these runs violates a property, it is returned as a “predicted” counter-example. This runtime analysis technique is sound (no false alarms) but not complete (says nothing about code that was not covered). A prototype called jPredictor has been implemented and evaluated on several Java applications with promising results.