Equivalence checking plays a crucial role in formal verification to ensure the correctness of concurrent systems. However, this method cannot be scaled as easily with the increasing complexity of systems due to the state explosion problem. This article presents an efficient procedure, based on heuristic search, for checking Milner's strong and weak equivalence; to achieve higher efficiency, we actually search for a difference between two processes to be discovered as soon as possible, thus the heuristics aims to find a counterexample, even if not the minimum one, to prove nonequivalence. The presented algorithm builds the system state graph on-the-fly, during the checking, and the heuristics promotes the construction of the more promising subgraph. The heuristic function is syntax based, but the approach can be applied to different specification languages such as CCS, LOTOS, and CSP, provided that the language semantics is based on the concept of transition. The algorithm to explore the search space of the problem is based on a greedy technique; GreASE (Greedy Algorithm for System Equivalence), the tool supporting the approach, is used to evaluate the achieved reduction of both state-space size and time with respect to other verification environments.

We propose the technique of Adaptive Allele Consolidation, that greatly improves the performance of the Lange-Goradia algorithm for genotype elimination in pedigrees, while still producing equivalent output. Genotype elimination consists in removing from a pedigree those genotypes that are impossible according to the Mendelian law of inheritance. This is used to find errors in genetic data and is useful as a preprocessing step in other analyses (such as linkage analysis or haplotype imputation). The problem of genotype elimination is intrinsically combinatorial, and Allele Consolidation is an existing technique where several alleles are replaced by a single “lumped” allele in order to reduce the number of combinations of genotypes that have to be considered, possibly at the expense of precision. In existing Allele Consolidation techniques, alleles are lumped once and for all before performing genotype elimination. The idea of Adaptive Allele Consolidation is to dynamically change the set of alleles that are lumped together during the execution of the Lange-Goradia algorithm, so that both high performance and precision are achieved. We have implemented the technique in a tool called Celer and evaluated it on a large set of scenarios, with good results.

The Java virtual machine embodies a verifier that performs a set of checks on Java bytecode programs before their execution. The verifier carries out an efficient data-flow analysis applied to a type-level abstract interpretation of the code. The implementations of the bytecode verifier presented a significant problem with programs compiled with the Sun Java compiler (until version 1.4.1): there were legal Java programs which were correctly compiled into a bytecode that was rejected by the verifier. The problem was fixed by removing, in version 1.4.2 and following, some interesting features in the compilation of the try-finally Java construct. Because removing such features has a cost in terms of memory space, in this paper we propose to enhance the bytecode verifier to accept such programs, maintaining the space efficiency of the previous versions of the compiler. We define an abstract interpretation framework in which we model the enhanced version of the verifier. The defined abstract interpretation framework can be considered a good basis for other static analyses of bytecode programs.

Bytecode verification is a key point in the security chain of the Java platform. This feature is only optional in many embedded devices since the memory requirements of the verification process are too high. In this article we propose an approach that significantly reduces the use of memory by a serial/parallel decomposition of the verification into multiple specialized passes. The algorithm reduces the type encoding space by operating on different abstractions of the domain of types. The results of our evaluation show that this bytecode verification can be performed directly on small memory systems. The method is formalized in the framework of abstract interpretation.

This paper presents an approach to analyze stack-based assembly code with respect to leakages of private information. We consider systems implementing a multilevel security policy, where the security levels form a lattice. The approach is based on abstract interpretation of the operational semantics. We consider a representative subset of instructions of conventional stack-based assembly languages. We define a collecting small-step semantics of the language, enhanced to convey the level of the information flow during execution: this is accomplished by annotating each value with the level of the information on which it depends. Then we define an abstract semantics of the language that abstracts from actual data and maintains only the annotations on the security level. We give sufficient conditions the abstract semantics must satisfy to ensure secure information flow. The use of abstract interpretation allows, on one side, being semantics based, to accept as secure a wide class of programs, and on the other side, being rule based, to be automated fully. In fact we show how it may be combined with a model checking technique, where the conditions for security are described by temporal logic formulae that can be automatically checked on the abstract representation of the program.

Abstract A method is presented for checking secure information flow in Java bytecode, assuming a multilevel security policy that assigns security levels to the objects. The method exploits the type‐level abstract interpretation of standard bytecode verification to detect illegal information flows. We define an algorithm transforming the original code into another code in such a way that a typing error detected by the Verifier on the transformed code corresponds to a possible illicit information flow in the original code. We present a prototype tool that implements the method and we show an example of application. Copyright © 2004 John Wiley & Sons, Ltd.

Abstract A method is proposed for checking security properties in programs written in high‐level languages. The method is based on the model checking technique. The SMV tool is used. The representation of the program is a Kripke structure modelling the control flow graph enriched with security information. The properties considered are secure information flow and the absence of covert channels caused by program termination. The formulae expressing these security properties are given using the logic CTL. Copyright © 2003 John Wiley & Sons, Ltd.

When an applet is sent over the internet, Java Virtual Machine code is transmitted and remotely executed. Because untrusted code can be executed on the local computer running the web browser security problems may arise. We present a method to check illicit flows in Java bytecode, that exploits the type-level abstract interpretation of bytecode verification. We present an algorithm transforming a bytecode into another one that, when abstractly executed by the standard bytecode verifier, reveals illicit information flows. We show an example of application of the method.

The Java Virtual Machine embodies a verifier which performs a set of checks on bytecode programs before their execution. The verifier performs a data-flow analysis applied to a type-level abstract interpretation of the code. The current implementations of the bytecode verifier present a significant problem: there are legal Java programs which are correctly compiled into a bytecode that is rejected by the verifier. Also the more powerful verification techniques proposed in several papers suffer from the same problem. In this paper we propose to enhance the bytecode verifier to accept such programs, maintaining the efficiency of current implementations. The enhanced version is based on a domain of types which is more expressive than the one used in standard verification.

Abstract A well‐known problem in the verification of concurrent systems based on model checking is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. A reduction technique to reduce state explosion in deadlock checking is presented. The method is based on an automatic syntactic simplification of a calculus of communicating systems (CCS) specification, which keeps the parts of the program structure that may lead to a deadlock and deletes the other parts. Copyright © 2002 John Wiley & Sons, Ltd.

Free flight has been proposed as a future alternative to the current policy in air traffic management (ATM) where aircraft follow predefined corridors. In free flight pilots can choose their own optimal routes, altitudes and velocities but are also responsible for the safe and fair resolution of trajectory conflicts. This would require a safe distributed control system were the trajectories that aircraft follow are as optimal as possible respecting sufficient safety distances. We model aircraft behaviour using non-determinism in such a way that reachability analysis provides the optimal trajectories of the aircraft. We compare the obtained results with the conflict resolution solutions proposed in the literature.

We present the formal verification of a multicast protocol for mobile computing. The protocol supports reliable and totally ordered communication within a set of processes running on mobile hosts. Mobile hosts communicate with a wired infrastructure through wireless links. The protocol is specified in Calculus of Communicating Systems and checked using the Concurrency Workbench tool. The protocol was chosen as a case study to evaluate the usefulness of a methodology, by means of which a property is checked on a reduced system, where the reduction is driven by the formula expressing the property itself. The reduction is obtained by transforming the program into one having a smaller representation. The approach is based on a logic, the selective mu-calculus, which has the characteristic that each formula allows the immediate pointing out of the parts of the system that do not alter the truth value of the formula itself, and thus can be ignored. We show and discuss the experimental results obtained.

In this paper we present a verification framework to check properties of full CCS terms. These properties are expressed in an action-based logic, and the proof technique is model checking, based on the transition system corresponding to the CCS term. Our approach also allows some kinds of properties to be proved if the transition systems are infinite. Of course, in these cases we only have a semi-decision method. The idea is to use (a sequence of) finite-state transition systems which approximate the, possibly infinite, transition system corresponding to a term. To this end we define a particular notion of approximation, suitable in proving liveness and safety properties of the process terms. Then we show that the class of provable properties might also depend on the way chains of approximations are built and we provide a set of notions to compare and choose among different approximation chains.

LOTOS is a formal specification language for concurrent and distributed systems. Basic LOTOS is the version of LOTOS without value-passing. A widely used approach to the verification of temporal properties is model checking. Often, in this approach the formal specification is translated into a labeled transition system on which formulae expressing properties are checked. A problem with this verification technique is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. In this paper we show how, given a set ρ of actions, it is possible to automatically obtain for a Basic LOTOS program a reduced transition system to which only the arcs labeled by actions in ρ belong. The set ρ of actions plays a fundamental role in conjunction with a temporal logic defined by the authors in a previous paper: selective mu-calculus. The reduced system with respect to ρ preserves the truth value of all selective mu-calculus formulae with actions from the set ρ. We act at both syntactic and semantic levels. From a syntactic point of view, we define a set of transformation rules obtaining a smaller program. On the semantic side, we define a non-standard semantics which dynamically reduces the transition system during generation. We present a tool implementing both the syntactic and the semantic reduction. Copyright © 1999 John Wiley & Sons, Ltd.

A specification language is introduced, able to define the behavior of concurrent programs. The language is particularly devoted to describing distributed applications, mainly with respect to scheduling problems. For this purpose, the language allows visibility of the past history of a computation and such history may be explicitly used to derive the choices on the future behavior of the computation itself and to define the values exchanged at each communication. A behavior is a partial order on events (communications) accomplished by processes, while the values of the communications are specified by a functional language. The most noticeable characteristic of specifications written in this language is the capability to be easily translated into executable concurrent programs (written into a CSP-like concurrent language), so obtaining an early prototype for these programs. An algorithm is described to accomplish the translation. An environment is provided to support static semantics checks on specifications, while dynamic testing and debugging are accomplished using interactive tools of the concurrent language environment.>

The authors discuss issues related to the debugging of concurrent programs. A set of desirable characteristics for a debugger for concurrent languages is deduced from a review of the differences between the debugging of concurrent programs and that of sequential ones. A debugger for concurrent language based upon CSP is then described. The debugger makes it possible to compare a description of the expected program behavior to the actual behaviour. The description of the behavior is given in terms of expressions composed by events and/or assertions on the process state. The developed formalism is able to describe behaviors at various levels of abstraction. Lastly, some guidelines for the implementation of the debugger are given and a detailed example of program debugging is analyzed.