Web application firewall (WAF) plays an integral role nowadays to protect web applications from various malicious injection attacks such as SQL injection, XML injection, and PHP injection, to name a few. However, given the evolving sophistication of injection attacks and the increasing complexity of tuning a WAF, it is challenging to ensure that the WAF is free of injection vulnerabilities such that it will block all malicious injection attacks without wrongly affecting the legitimate message. Automatically testing the WAF is, therefore, a timely and essential task. In this paper, we propose DaNuoYi, an automatic injection testing tool that simultaneously generates test inputs for multiple types of injection attacks on a WAF. Our basic idea derives from the cross-lingual translation in the natural language processing domain. In particular, test inputs for different types of injection attacks are syntactically different but may be semantically similar. Sharing semantic knowledge across multiple programming languages can thus stimulate the generation of more sophisticated test inputs and discovering injection vulnerabilities of the WAF that are otherwise difficult to find. To this end, in DaNuoYi, we train several injection translation models by using multi-task learning that translates the test inputs between any pair of injection attacks. The model is then used by a novel multi-task evolutionary algorithm to co-evolve test inputs for different types of injection attacks facilitated by a shared mating pool and domain-specific mutation operators at each generation. We conduct experiments on three real-world open-source WAFs and six types of injection attacks, the results reveal that DaNuoYigenerates up to 3:8× and 5:78× more valid test inputs (i.e., bypassing the underlying WAF) than its state-of-the-art single-task counterparts and the context-free grammar-based injection construction.

Defining test oracles is crucial and central to test development, but manual construction of oracles is expensive. While recent neural-based automated test oracle generation techniques have shown promise, their real-world effectiveness remains a compelling question requiring further exploration and understanding. This paper investigates the effectiveness of TOGA, a recently developed neural-based method for automatic test oracle generation. TOGA utilizes EvoSuite-generated test inputs and generates both exception and assertion oracles. In a Defects4j study, TOGA outperformed specification, search, and neural-based techniques, detecting 57 bugs, including 30 unique bugs not detected by other methods. To gain a deeper understanding of its applicability in real-world settings, we conducted a series of external, extended, and conceptual replication studies of TOGA.

As software development teams adopt DevSecOps practices, application security is increasingly the responsibility of development teams, who are required to set up their own Static Application Security Testing (SAST) infrastructure.

We present RAPID, an industrial-strength analysis developed at AWS that aims to help developers by providing automatic, fast and actionable feedback about correct usage of cloud-service APIs. RAPID’s design is based on the insight that cloud service APIs are structured around short-lived request- and response-objects whose usage patterns can be specified as value-dependent type-state automata and be verified by combining local type-state with global value-flow analyses. We describe various challenges that arose to deploy RAPID at scale. Finally, we present an evaluation that validates our design choices, deployment heuristics, and shows that RAPID is able to quickly and precisely report a wide variety of useful API misuse violations in large, industrial-strength code bases.

Inferring the input grammar accepted by a program is central for a variety of software engineering problems, including parsers verification, grammar-based fuzzing, communication protocol inference, and documentation. Sound and complete active learning techniques have been developed for several classes of languages and the corresponding automaton representation, however there are outstanding challenges that are limiting their effective application to the inference of input grammars. We focus on active learning techniques based on $$L^*$$ and propose two extensions of the Minimally Adequate Teacher framework that allow the efficient learning of the input language of a program in the form of symbolic automata, leveraging the additional information that can extracted from concolic execution. Upon these extensions we develop two learning algorithms that reduce significantly the number of queries required to converge to the correct hypothesis.

Merging execution paths is a powerful technique for reducing path explosion in symbolic execution. One approach, introduced and dubbed “veritesting” by Avgerinos et al., works by translating abounded control flow region into a single constraint. This approach is a convenient way to achieve path merging as a modification to a pre-existing single-path symbolic execution engine. Previous work evaluated this approach for symbolic execution of binary code, but different design considerations apply when building tools for other languages. In this paper, we extend the previous approach for symbolic execution of Java.

Abstract Path-merging is a known technique for accelerating symbolic execution. One technique, named “veritesting” by Avgerinos et al. uses summaries of bounded control-flow regions and has been shown to accelerate symbolic execution of binary code. But, when applied to symbolic execution of Java code, veritesting needs to be extended to summarize dynamically dispatched methods and exceptional control-flow. Such an extension of veritesting has been implemented in Java Ranger by implementing as an extension of Symbolic PathFinder, a symbolic executor for Java bytecode. In this paper, we briefly describe the architecture of Java Ranger and describe its setup for SV-COMP 2020.

Abstract COASTAL is a program analysis tool for Java programs. It combines concolic execution and fuzz testing in a framework with built-in concurrency, allowing the two approaches to cooperate naturally.

This paper gives a brief overview of Java Pathfinder, or jpf-core. We describe the architecture of JPF, its strengths, and how it was set up for SV-COMP 2019.

This paper describes the benchmark entry for Symbolic Pathfinder, a symbolic execution tool for Java bytecode. We give a brief description of the tool and we describe the particular run configuration that was used in the SV-COMP competition. Furthermore, we comment on the competition results and we outline some directions for future work.

The paper Test Input Generation With Java PathFinder was published in the International Symposium on Software Testing and Analysis (ISSTA) 2004 Proceedings, and has now been selected to receive the ISSTA 2018 Retrospective Impact Paper Award. The paper described black-box and white-box techniques for the automated testing of software systems. These techniques were based on model checking and symbolic execution and incorporated in the Java PathFinder analysis tool. The main contribution of the paper was to describe how to perform efficient test input generation for code manipulating complex data that takes into account complex method preconditions and evaluate the techniques for generating high coverage tests.

As feature-rich Android applications (apps for short) are increasingly popularized in security-sensitive scenarios, methods to verify their security properties are highly desirable. Existing approaches on verifying Android apps often have limited effectiveness. For instance, static analysis often suffers from a high false-positive rate, whereas approaches based on dynamic testing are limited in coverage. In this work, we propose an alternative approach, which is to apply the software model checking technique to verify Android apps. We have built a general framework named DroidPF upon Java PathFinder (JPF), towards model checking Android apps. In the framework, we craft an executable mock-up Android OS which enables JPF to dynamically explore the concrete state spaces of the tested apps; we construct programs to generate user interaction and environmental input so as to drive the dynamic execution of the apps; and we introduce Android specific reduction techniques to help alleviate the state space explosion. DroidPF focuses on common security vulnerabilities in Android apps including sensitive data leakage involving a non-trivial flow- and context-sensitive taint-style analysis. DroidPF has been evaluated with 131 apps, which include real-world apps, third-party libraries, malware samples and benchmarks for evaluating app analysis techniques like ours. DroidPF precisely identifies nearly all of the previously known security issues and nine previously unreported vulnerabilities/bugs.

Recently there has been a proliferation of automated program repair (APR) techniques, targeting various programming languages. Such techniques can be generally classified into two families: syntactic- and semantics-based. Semantics-based APR, on which we focus, typically uses symbolic execution to infer semantic constraints and then program synthesis to construct repairs conforming to them. While syntactic-based APR techniques have been shown success- ful on bugs in real-world programs written in both C and Java, semantics-based APR techniques mostly target C programs. This leaves empirical comparisons of the APR families not fully explored, and developers without a Java-based semantics APR technique. We present JFix, a semantics-based APR framework that targets Java, and an associated Eclipse plugin. JFix is implemented atop Symbolic PathFinder, a well-known symbolic execution engine for Java programs. It extends one particular APR technique (Angelix), and is designed to be sufficiently generic to support a variety of such techniques. We demonstrate that semantics-based APR can indeed efficiently and effectively repair a variety of classes of bugs in large real-world Java programs. This supports our claim that the framework can both support developers seeking semantics-based repair of bugs in Java programs, as well as enable larger scale empirical studies comparing syntactic- and semantics-based APR targeting Java. The demonstration of our tool is available via the project website at: https://xuanbachle.github.io/semanticsrepair/

We introduce a new technique for inferring program invariants that uses symbolic states generated by symbolic execution. Symbolic states, which consist of path conditions and constraints on local variables, are a compact description of sets of concrete program states and they can be used for both invariant inference and invariant verification. Our technique uses a counterexample-based algorithm that creates concrete states from symbolic states, infers candidate invariants from concrete states, and then verifies or refutes candidate invariants using symbolic states. The refutation case produces concrete counterexamples that prevent spurious results and allow the technique to obtain more precise invariants. This process stops when the algorithm reaches a stable set of invariants. We present Symlnfer, a tool that implements these ideas to automatically generate invariants at arbitrary locations in a Java program. The tool obtains symbolic states from Symbolic PathFinder and uses existing algorithms to infer complex (potentially nonlinear) numerical invariants. Our preliminary results show that Symlnfer is effective in using symbolic states to generate precise and useful invariants for proving program safety and analyzing program runtime complexity. We also show that Symlnfer outperforms existing invariant generation systems.

A notable class of techniques for automatic program repair is known as semantics-based. Such techniques, e.g., Angelix, infer semantic specifications via symbolic execution, and then use program synthesis to construct new code that satisfies those inferred specifications. However, the obtained specifications are naturally incomplete, leaving the synthesis engine with a difficult task of synthesizing a general solution from a sparse space of many possible solutions that are consistent with the provided specifications but that do not necessarily generalize. We present S3, a new repair synthesis engine that leverages programming-by-examples methodology to synthesize high-quality bug repairs. The novelty in S3 that allows it to tackle the sparse search space to create more general repairs is three-fold: (1) A systematic way to customize and constrain the syntactic search space via a domain-specific language, (2) An efficient enumeration- based search strategy over the constrained search space, and (3) A number of ranking features based on measures of the syntactic and semantic distances between candidate solutions and the original buggy program. We compare S3’s repair effectiveness with state-of-the-art synthesis engines Angelix, Enumerative, and CVC4. S3 can successfully and correctly fix at least three times more bugs than the best baseline on datasets of 52 bugs in small programs, and 100 bugs in real-world large programs.

Current dynamic analysis tools for Android applications do not get good code coverage since they can only explore a subset of the behaviors of the applications and do not have full control over the environment in which they execute. In this work we use model checking to systematically explore application paths while reducing the analysis size using state matching and backtracking. In particular, we extend the Java PathFinder (JPF) model checking environment for Android. We describe the difficulties one needs to overcome to make this a reality as well as our current approaches to handling these issues. We obtain significantly higher coverage using shorter event sequences on a representative sample of Android apps, when compared to Dynodroid and Sapienz, the current state-of-the-art dynamic analysis tools for Android applications.

Mutation operators have been studied at length to determine which ones are the ``best" at some metric (for example creates the least equivalent mutants, creates hard-to-kill mutants, etc.). These studies though have focused on specific test suites, where the test inputs and oracles are fixed, which leads to results that are strongly influenced by the test suites and thus makes the conclusions potentially less general. In this paper we consider all test inputs and we assume we have no prior knowledge about the likelihood of any specific inputs. We will also show how varying the strength of the oracle have a big impact on the results. We only consider a few mutation operators (mostly relational), only a handful of programs to mutate (amenable to probabilistic symbolic execution), and only consider how likely it is that a mutant is killed. A core finding is that the likelihood of reaching the source line where the mutation is applied, is an important contributor to the likelihood of killing the mutant and when we control for this we can see which operators create mutations that are too easy versus very hard to kill.

We present a testing approach for object oriented programs, which encompasses a testing criterion and an automated test generation technique. The criterion, that we call field-exhaustive testing, requires a user-provided limit n on the size of data domains, and is based on the idea of considering enough inputs so as to exhaustively cover the extension of class fields, within the limit n. Intuitively, the extension of a field f is the binary relation established between objects and their corresponding values for field f, in valid instances. Thus, a suite S is field-exhaustive if whenever a field f relates an object o with a value v (i.e., o.f = v) within a valid instance I of size bounded by n, then S contains at least one input I' covering such relationship, i.e., o must also be part of I', and o.f = v must hold in I'. Our test generation technique uses incremental SAT solving to produce small field-exhaustive suites: field-exhaustiveness can be achieved with a suite containing at most # F x n2 inputs, where # F is the number of fields in the class under test.

Lazy Initialization (LI) allows symbolic execution to effectively deal with heap-allocated data structures, thanks to a significant reduction in spurious and redundant symbolic structures. Bounded lazy initialization (BLI) improves on LI by taking advantage of precomputed relational bounds on the interpretation of class fields in order to reduce the number of spurious structures even further. In this paper we present bounded lazy initialization with SAT support (BLISS), a novel technique that refines the search for valid structures during the symbolic execution process. BLISS builds upon BLI, extending it with field bound refinement and satisfiability checks. Field bounds are refined while a symbolic structure is concretized, avoiding cases that, due to the concrete part of the heap and the field bounds, can be deemed redundant. Satisfiability checks on refined symbolic heaps allow us to prune these heaps as soon as they are identified as infeasible, i.e., as soon as it can be confirmed that they cannot be extended to any valid concrete heap. Compared to LI and BLI, BLISS reduces the time required by LI by up to four orders of magnitude for the most complex data structures. Moreover, the number of partially symbolic structures obtained by exploring program paths is reduced by BLISS by over 50 percent, with reductions of over 90 percent in some cases (compared to LI). BLISS uses less memory than LI and BLI, which enables the exploration of states unreachable by previous techniques.

Probabilistic software analysis seeks to quantify the likelihood of reaching a target event under uncertain environments. Recent approaches compute probabilities of execution paths using symbolic execution, but do not support nondeterminism. Nondeterminism arises naturally when no suitable probabilistic model can capture a program behavior, e.g., for multithreading or distributed systems.

Probabilistic software analysis aims at quantifying how likely a target event is to occur during program execution. Current approaches rely on symbolic execution to identify the conditions to reach the target event and try to quantify the fraction of the input domain satisfying these conditions. Precise quantification is usually limited to linear constraints, while only approximate solutions can be provided in general through statistical approaches. However, statistical approaches may fail to converge to an acceptable accuracy within a reasonable time.

Symbolic execution techniques have been proposed recently for the probabilistic analysis of programs. These techniques seek to quantify the likelihood of reaching program events of interest, e.g., assert violations. They have many promising applications but have scalability issues due to high computational demand. To address this challenge, we propose a statistical symbolic execution technique that performs Monte Carlo sampling of the symbolic program paths and uses the obtained information for Bayesian estimation and hypothesis testing with respect to the probability of reaching the target events. To speed up the convergence of the statistical analysis, we propose Informed Sampling, an iterative symbolic execution that first explores the paths that have high statistical significance, prunes them from the state space and guides the execution towards less likely paths. The technique combines Bayesian estimation with a partial exact analysis for the pruned paths leading to provably improved convergence of the statistical analysis. We have implemented statistical symbolic execution with informed sampling in the Symbolic PathFinder tool. We show experimentally that the informed sampling obtains more precise results and converges faster than a purely statistical analysis and may also be more efficient than an exact symbolic analysis. When the latter does not terminate symbolic execution with informed sampling can give meaningful results under the same time and memory limits.

We shall conduct a half-day workshop on needed revisions to Software Engineering 2004: Curriculum Guidelines for Undergraduate Degree Programs in Software Engineering (SE 2004). A brief overview of the current guidelines and their revision status will be presented. Workshop attendees will share their experience using the current guidelines and suggest needed changes. We will provide a summary report from the workshop to other CSEE&T attendees at a Birds Of a Feather meeting later during the conference.

This panel will engage participants in a discussion of recent changes in software engineering practice that should be reflected in curriculum guidelines for undergraduate software engineering programs. Current progress in revising the guidelines will be presented, including suggestions to update coverage of agile methods, security and service-oriented computing.

Software reliability analysis tackles the problem of predicting the failure probability of software. Most of the current approaches base reliability analysis on architectural abstractions useful at early stages of design, but not directly applicable to source code. In this paper we propose a general methodology that exploit symbolic execution of source code for extracting failure and success paths to be used for probabilistic reliability assessment against relevant usage scenarios. Under the assumption of finite and countable input domains, we provide an efficient implementation based on Symbolic PathFinder that supports the analysis of sequential and parallel programs, even with structured data types, at the desired level of confidence. The tool has been validated on both NASA prototypes and other test cases showing a promising applicability scope.

Java Pathfinder (JPF) is an open source analysis system that automatically verifies Java programs. The JPF tutorial provides an opportunity to software engineering researchers and practitioners to learn about JPF, be able to install and run JPF, and understand the concepts required to extend JPF. The hands-on tutorial will expose the attendees to the basic architecture framework of JPF, demonstrate the ways to use it for analyzing their artifacts, and illustrate how they can extend JPF to implement their own analyses. One of the defining qualities of JPF is its extensibility. JPF has been extended to support symbolic execution, directed automated random testing, different choice generation, configurable state abstractions, various heuristics for enabling bug detection, configurable search strategies, checking temporal properties and many more. JPF supports these extensions at the design level through a set of stable well defined interfaces. The interfaces are designed to not require changes to the core, yet enable the development of various JPF extensions. In this tutorial we provide attendees a hands on experience of developing different interfaces in order to extend JPF. The tutorial is targeted toward a general software engineering audience-software engineering researchers and practitioners. The attendees need to have a good understanding of the Java programming language and be fairly comfortable with Java program development. The attendees are not required to have any background in Java Pathfinder, software model checking or any other formal verification techniques. The tutorial will be self-contained.

Software Engineering 2004: Curriculum Guidelines for Undergraduate Degree Programs in Software Engineering (SE 2004) [1] is one volume in a set of computing curricula adopted and supported by the ACM and the IEEE Computer Society. In order to keep the software engineering guidelines up to date the two professional societies began a review and revision project in early 2011. This special session will present the results of the review, present a first draft of the revision, and provide time for discussion and input from the computing education community.

The continued development of efficient automated decision procedures has spurred the resurgence of research on symbolic execution over the past decade. Researchers have applied symbolic execution to a wide range of software analysis problems including: checking programs against contract specifications, inferring bounds on worst-case execution performance, and generating path-adequate test suites for widely used library code.

The analysis of constraints plays an important role in many aspects of software engineering, for example constraint satisfiability checking is central to symbolic execution. However, the norm is to recompute results in each analysis. We propose a different approach where every call to the solver is wrapped in a check to see if the result is not already available. While many tools use some form of results caching, the novelty of our approach is the persistence of results across runs, across programs being analyzed, across different analyses and even across physical location. Achieving such reuse requires that constraints be distilled into their essential parts and represented in a canonical form.

We present results for the "Impact Project Focus Area" on the topic of symbolic execution as used in software testing. Symbolic execution is a program analysis technique introduced in the 70s that has received renewed interest in recent years, due to algorithmic advances and increased availability of computational power and constraint solving technology. We review classical symbolic execution and some modern extensions such as generalized symbolic execution and dynamic test generation. We also give a preliminary assessment of the use in academia, research labs, and industry.

Symbolic execution is a powerful static program analysis technique that has been used for the automated generation of test inputs. Directed Automated Random Testing (DART) is a dynamic variant of symbolic execution that initially uses random values to execute a program and collects symbolic path conditions during the execution. These conditions are then used to produce new inputs to execute the program along different paths. It has been argued that DART can handle situations where classical static symbolic execution fails due to incompleteness in decision procedures and its inability to handle external library calls.

We describe the Impendulo tool for fine-grained analyses of programmer behavior. The initial design goal was to create a system to answer the following simple question: "What kind of mistakes do programmers make and how often do they make these mistakes?" However it quickly became apparent that the tool can be used to also analyze other fundamental software engineering questions, such as, how good are static analysis tools at finding real errors?, what is the fault finding capability of automated test generation tools?, what is the influence of a bad specification?, etc. We briefly describe the tool and some of the insights gained from using it.

Programming languages designed specifically for multi-agent systems represent a new programming paradigm that has gained popularity over recent years, with some multi-agent programming languages being used in increasingly sophisticated applications, often in critical areas. To support this, we have developed a set of tools to allow the use of model-checking techniques in the verification of systems directly implemented in one particular language called AgentSpeak. The success of model checking as a verification technique for large software systems is dependent partly on its use in combination with various state-space reduction techniques, an important example of which is property-based slicing. This article introduces an algorithm for property-based slicing of AgentSpeak multi-agent systems. The algorithm uses literal dependence graphs, as developed for slicing logic programs, and generates a program slice whose state space is stuttering-equivalent to that of the original program; the slicing criterion is a property in a logic with LTL operators and (shallow) BDI modalities. In addition to showing correctness and characterizing the complexity of the slicing algorithm, we apply it to an AgentSpeak program based on autonomous planetary exploration rovers, and we discuss how slicing reduces the model-checking state space. The experiment results show a significant reduction in the state space required for model checking that agent, thus indicating that this approach can have an important impact on the future practicality of agent verification.

This paper describes an analysis approach based on a combination of static and dynamic techniques to find run-time errors in Java code. It uses symbolic execution to find constraints under which an error (e.g., a null pointer dereference, array out of bounds access, or assertion violation) may occur and then solves these constraints to find test inputs that may expose the error. It only alerts the user to the possibility of a real error when it detects the expected exception during a program run. The analysis is customizable in two important ways. First, we can adjust how deeply to follow calls from each top-level method. Second, we can adjust the path termination condition for the symbolic execution engine to be either a bound on the path condition length or a bound on the number of times each instruction can be revisited. We evaluated the tool on a set of benchmarks from the literature as well as a number of real-world systems that range in size from a few thousand to 50,000 lines of code. The tool discovered all known errors in the benchmarks (as well as some not previously known) and reported on average 8 errors per 1000 lines of code for the industrial examples. In both cases the interprocedural call depth played little role in the error detection. That is, an intraprocedural analysis seems adequate for the class of errors we detect.

We propose an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. The method does not require an abstract transition relation to be generated, but instead executes the concrete transitions while storing abstract versions of the concrete states, as specified by a set of abstraction predicates. For each explored transition the method checks, with the help of a theorem prover, whether there is any loss of precision introduced by abstraction. The results of these checks are used to decide termination or to refine the abstraction by generating new abstraction predicates. If the (possibly infinite) concrete system under analysis has a finite bisimulation quotient, then the method is guaranteed to eventually explore an equivalent finite bisimilar structure. We illustrate the application of the approach for checking concurrent programs.

The popularity of object-oriented programming has led to the wide use of container libraries. It is important for the reliability of these containers that they are tested adequately. We describe techniques for automated test input generation of Java container classes. Test inputs are sequences of method calls from the container interface. The techniques rely on state matching to avoid generation of redundant tests. Exhaustive techniques use model checking with explicit or symbolic execution to explore all the possible test sequences up to predefined input sizes. Lossy techniques rely on abstraction mappings to compute and store abstract versions of the concrete states; they explore underapproximations of all the possible test sequences.We have implemented the techniques on top of the Java PathFinder model checker and we evaluate them using four Java container classes. We compare state matching based techniques and random selection for generating test inputs, in terms of testing coverage. We consider basic block coverage and a form of predicate coverage - that measures whether all combinations of a predetermined set of predicates are covered at each basic block. The exhaustive techniques can easily obtain basic block coverage, but cannot obtain good predicate coverage before running out of memory. On the other hand, abstract matching turns out to be a powerful approach for generating test inputs to obtain high predicate coverage. Random selection performed well except on the examples that contained complex input spaces, where the lossy abstraction techniques performed better.

We consider the problem of test input generation for code that manipulates complex data structures. Test inputs are sequences of method calls from the data structure interface. We describe test input generation techniques that rely on state matching to avoid generation of redundant tests. Exhaustive techniques use explicit state model checking to explore all the possible test sequences up to predefined input sizes. Lossy techniques rely on abstraction mappings to compute and store abstract versions of the concrete states; they explore under-approximations of all the possible test sequences. We have implemented the techniques on top of the Java PathFinder model checker and we evaluate them using a Java implementation of red-black trees.

We show how model checking and symbolic execution can be used to generate test inputs to achieve structural coverage of code that manipulates complex data structures. We focus on obtaining branch-coverage during unit testing of some of the core methods of the red-black tree implementation in the Java TreeMap library, using the Java PathFinder model checker. Three different test generation techniques will be introduced and compared, namely, straight model checking of the code, model checking used in a black-box fashion to generate all inputs up to a fixed size, and lastly, model checking used during white-box test input generation. The main contribution of this work is to show how efficient white-box test input generation can be done for code manipulating complex data, taking into account complex method preconditions.

Numerous researchers have reported success in reasoning about properties of small programs using finite-state verification techniques. We believe, as do most researchers in this area, that in order to scale those initial successes to realistic programs, aggressive abstraction of program data will be necessary. Furthermore, we believe that to make abstraction-based verification usable by non-experts significant tool support will be required. In this paper we describe how several different program analysis and transformation techniques are integrated into the Bandera toolset to provide facilities for abstracting Java programs to produce compact, finite-state models that are amenable to verification for example via model checking. We illustrate the application of Bandera's abstraction facilities to analyze a realistic multi-threaded Java program.

We present an iterative technique in which model checking and static analysis are combined to verify large software systems. The role of the static analysis is to compute partial order information which the model checker uses to reduce the state space. During exploration, the model checker also computes aliasing information that it gives to the static analyzer which can then refine its analysis. The result of this refined analysis is then fed back to the model checker which updates its partial order reduction. At each step of this iterative process, the static analysis computes optimistic information which results in an unsafe reduction of the state space. However, we show that the process converges to a fixed point at which time the partial order information is safe and the whole state space is explored.

This paper describes an experiment to use the Spin model checking system to support automated verification of time partitioning in the Honeywell DEOS real-time scheduling kernel. The goal of the experiment was to investigate whether model checking could be used to find a subtle implementation error that was originally discovered and fixed during the standard formal review process. To conduct the experiment, a core slice of the DEOS scheduling kernel was first translated without abstraction from C++ into Promela (the input language for Spin). We constructed an abstract “test-driver” environment and carefully introduced several abstractions into the system to support verification. Several experiments were run to attempt to verify that the system implementation adhered to the critical time partitioning requirements. During these experiments, the known error was rediscovered in the time partitioning implementation. We believe this case study provides several insights into how to develop cost-effective methods and tools to support the software design and implementation review process.

Program analysis, testing and verification are key techniques for building confidence in and increasing the quality of software systems. Such activities typically cost upwards of 50% of total development costs. Automation aims to allow both reduced costs and more thorough analysis, testing and verification and is vital to keep pace with increasing software complexity.

The majority of the work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers and model checkers. In this paper, we give arguments for why we believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy, we have developed a verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing. Part of this work has consisted of building a new Java Virtual Machine that interprets Java bytecode. JPF uses state compression to handle large states, and partial order reduction, slicing, abstraction and run-time analysis techniques to reduce the state space. JPF has been applied to a real-time avionics operating system developed at Honeywell, illustrating an intricate error, and to a model of a spacecraft controller, illustrating the combination of abstraction, run-time analysis and slicing with model checking.