Cloud systems have become ubiquitous today -- they are used to store and process the tremendous amounts of data being generated by Internet users. These systems run on hundreds of commodity machines, and have a huge amount of non-determinism (thousands of threads and hundreds of processes) in their execution. Therefore, bugs that occur in cloud systems are hard to understand, reproduce, and fix. The state-of-the-art of debugging in the industry is to log messages during execution, and refer to those messages later in case of errors. In ReproLite, we augment the already widespread process of debugging using logs by enabling testers to quickly and easily specify the conjectures that they form regarding the cause of an error (or bug) from execution logs, and to also automatically validate those conjectures.

We present an efficient data race prediction algorithm that uses lock-reordering based incremental search on time-stamped lock histories for solving multiple races effectively. We balance prediction accuracy, coverage, and performance with a specially designed pairwise reachability algorithm that can store and re-use past search results, thereby, amortizing the cost of reasoning over redundant and overlapping search space. Compared to graph-based search algorithms, our algorithm incurs much smaller overhead due to amortization, and can potentially be used while a program under test is executing. To demonstrate such a possibility, we implemented our approach as an incremental Predictive Analysis (iPA) module in a predictive testing framework. Our approach can handle traces with a few hundreds to half a million events, and predict known/unknown real data races with a performance penalty of less than 4% in addition to what is incurred by runtime race detectors.

Testing and debugging multi-threaded programs are notoriously difficult due to non-determinism not only in inputs but also in OS schedules. In practice, dynamic analysis and failure replay systems instrument the program to record events of interest in the test execution, e.g., program inputs, accesses to shared objects, synchronization operations, context switches, etc. To reduce the overhead of logging during runtime, these testing and debugging efforts have proposed tradeoffs for sampling or selective logging, at the cost of reducing coverage or performing more expensive search offline.

We present a symbolic testing tool BEST for finding atomicity violations. We automatically infer and generate potential atomicity properties from an observed run of a multi-threaded program, and use precise modeling and constraint-based symbolic search to find atomicity violating schedules in the most generalization of the observed run. We focus mainly on the tool scalability by devising various simplification steps to reduce the formula and the search space by orders-of-magnitude. To that effect, we also introduce a new notion of atomicity that is useful and simple to check. We demonstrate the effectiveness of the combined techniques on several public C/C++/Java benchmarks in finding known/unknown atomicity bugs.

We present a tool BEST (Binary instrumentation-based Error-directed Symbolic Testing) for predicting concurrency violations.1We automatically infer potential concurrency violations such as atomicity violations from an observed run of a multi-threaded program, and use precise modeling and constraint-based symbolic (non-enumerative) search to find feasible violating schedules in a generalization of the observed run. We specifically focus on tool scalability by devising POR-based simplification steps to reduce the formula and the search space by several orders-of-magnitude. We have successfully applied the tool to several publicly available C/C++/Java programs and found several previously known/unknown concurrency related bugs. The tool also has extensive visual support for debugging.

Abstract Predictive analysis aims at detecting concurrency errors during runtime by monitoring a concrete execution trace of a concurrent program. In recent years, various models based on the happens-before causality relations have been proposed for predictive analysis. However, these models often rely on only the observed runtime events and typically do not utilize the program source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted traces often suffer from the interleaving explosion problem. In this paper, we introduce a precise predictive model based on both the program source code and the observed execution events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events of the given trace. Rather than explicitly enumerating and checking the interleavings, our method conducts the search using a novel encoding and symbolic reasoning with a satisfiability modulo theory solver. We also propose a technique to bound the number of context switches allowed in the interleavings during the symbolic search, to further improve the scalability of the algorithm.

State-based model checking methods comprise computing and storing reachable states, while stateless model checking methods directly reason about reachable paths using decision procedures, thereby avoiding computing and storing the reachable states. Typically, state-based methods involve memory-intensive operations, while stateless methods involve time-intensive operations. We propose a divide-and-conquer strategy to combine the complementary strengths of these methods for efficient verification of embedded software. Specifically, our model checking engine uses both state decomposition and state prioritization to guide the combination of a Presburger arithmetic based symbolic traversal algorithm (state-based) and an SMT based bounded model checking algorithm (stateless). These two underlying algorithms are interleaved-based on memory/time bounds and dynamic task partitioning-in order to systematically explore the state space and to avoid storing the entire reachable state set. We have implemented our new method in a tightly integrated verification tool called HMC (Hybrid Model Checker). We demonstrate the efficacy of the proposed method on some industry examples.

Software model checking has recently been successful in discovering bugs in production software. Most tools have targeted heap related programming mistakes and control-heavy programs. However, real-time and embedded controllers implemented in software are susceptible to computational numeric instabilities. We target verification of numerical programs that use floating-point types, to detect loss of numerical precision incurred in such programs. Techniques based on abstract interpretation have been used in the past for such analysis. We use bounded model checking (BMC) based on Satisfiability Modulo Theory (SMT) solvers, which work on a mixed integer-real model that we generate for programs with floating points. We have implemented these techniques in our software verification platform. We report experimental results on benchmark examples to study the effectiveness of model checking on such problems, and the effect of various model simplifications on the performance of model checking.

In verification of hybrid discrete-continuous and embedded control systems, one encounters decision problems involving non-linear constraints. We propose an efficient decision procedure (CORD) for such decisions problems using CORDIC algorithms, and an off-the-shelf SMT(LA) (Satisfiability Modulo Theory for Linear Arithmetic) solver, for given precision requirements. We first translate the non-linear part of the decision problem to a SMT(LA) formula using CORDIC algorithms, accounting for all the inaccuracies safely. In the translation, we use a normalization scheme, combined with interval bounds to obtain a linearized formula without compromising the precision requirements. On such a linearized formula, we devise a DPLL-style Interval Search Engine (DISE) that explores various combinations of interval bounds using a SMT(LA) solver. In our experiments, we demonstrate the efficacy of our approach, and compare it with a latest state-of-the-art decision procedure.

In practice, verification engines have to solve many checkers in a very tight time budget, especially, when the system to be analyzed is large, with many coverage criteria. To cope with such a situation, we propose improved and light-weight verification techniques that are built over the state-of-the-art engines such as bounded model checking (BMC), induction, and guided-simulation (directed testing). Specifically, we propose using control state reachability (CSR) information—obtained from a given software system—to strengthen our induction-based proof engine. We also propose identifying and using lighthouses (or guide-posts)—intermediate control states—to simplify and reduce BMC instances, and to guide a simulation engine. We schedule these engines suitably to maximize the resource utilization. We implemented our techniques in a tool ACE, and integrated it in an industry strength software verification platform F-Soft to provide a robust and precise analysis framework. We show effectiveness of ACE on several industry and public benchmarks in a comparative study.

Bounded Model Checking (BMC) provides complete design coverage with respect to a correctness property up to a bounded depth. However, with successive unrolling of the design, each BMC instance at depth k becomes bigger in size and harder to solve. We propose a novel scalable approach to decompose disjunctively a BMC instance, into simpler and independent subproblems, based on tunnels i.e., a set of control paths. We simplify each subproblem using slicing, data path simplification and tunnel specific control flow constraints, and solve them independently. We implemented such a tunneling and slicing-based reduction (TSR) approach in Satisfiability-Modulo-Theory (SMT)-based BMC framework. Such a TSR-based approach improves the overall performance of BMC when applied to verification of lowlevel embedded industry programs.

A SystemC simulation kernel consists of a deterministic implementation of the scheduler, whose specification is non-deterministic. To leverage testing of a SystemC TLM design, we focus on automatically exploring all possible behaviors of the design for a given data input. We combine static and dynamic partial order reduction techniques with SystemC semantics to intelligently explore a subset of the possible traces, while still being provably sufficient for detecting deadlocks and safety property violations. We have implemented our exploration algorithm in a framework called Satya and have applied it to a variety of examples including the TAC benchmark. Using Satya, we automatically found an assertion violation in a benchmark distributed as a part of the OSCI repository.

Bounded Model Checking (BMC) is incomplete without a completeness threshold (CT) bound. Previous methods, using recurrence diameter for obtaining CT, check for existence of a longest loop-free path at every depth k. For terminating software programs, we propose an efficient method for obtaining CT that requires solving a formula of size O(k) at some depths only, as compared to previous methods that require solving a formula of O(k2) (or O(klogk)) size at every depth. We augment previous methods for BMC simplifications using model transformation and control flow information, with context-sensitive analysis. This results in more BMC simplifications and further reduction in the number of CT checks. We have implemented our techniques in a Satisfiability Modulo Theory (SMT)-based BMC framework. Our controlled experiments on real-world software programs show that our proposed formulation provides significant improvements over previous approaches.

Embedded software are becoming more and more pervasive in our lives, and many application domains have very high reliability requirements. Ensuring high software quality while still maintaining software productivity is a challenging task. In order to address this challenge, more formal analysis and automated verification techniques are needed in addition to standard software testing.

Error diagnosis, which is the process of identifying the root causes of bugs in software, is a time-consuming process. In general, it is hard to automate error diagnosis due to the unavailability of a full ldquogoldenrdquo specification of the system behavior in realistic software development. We propose a repair-based proof-guided error diagnosis (PED) framework, that provides a first-line attack to find the root causes of the errors in programs by pin-pointing the possible error-sites (buggy statements), and suggesting possible repair fixes. Our framework does not need a complete system specification. Instead, it automatically ldquominesrdquo partial specifications of the intended program behavior from the proofs obtained by static program analysis for standard safety checkers. It uses these partial specifications along with the multiple error traces provided by a model checker to narrow down the possible error sites. It also exploits inherent correlations among the program statements. To capture common programming mistakes, it directs the search to those statements that could be buggy due to simple copy-paste operations or syntactic mistakes such as using les instead of <. To further improve debugging, it prioritizes the repair solutions. We implemented and integrated the PED tool as a plug-in module to a software verification framework. We show the efficacy of such a framework on public benchmarks.

This paper presents a lightweight interval analysis technique for determining the lower and upper bounds for program variables and its application in improving software model checking techniques. The experiments demonstrate that it is an effective approach to alleviate the state explosion problem in software model checking.

Current industry trends in system design - multiple clocks, clocks with arbitrary frequency ratios, multi-phased clocks, gated clocks, and level-sensitive latches, combined with clocked - pose additional challenges to verification efforts. We propose an integrated solution that improves SAT-based bounded model checking (BMC) by orders of magnitude, for verification of synchronous multi-clock systems with clocked LTL properties. Our main contributions are: a) efficient clock modeling schemes to handle clock related challenges uniformly; b) generation of automatic schedules and clock constraints to avoid unnecessary unrolling and loop-checks in BMC; c) dynamic simplification of BMC problem instances with clock constraints; and d) customized BMC translations - with incremental formulations and learning - to directly handle PSL-style clocked specifications. We demonstrate the effectiveness of our approach on some OpenCores multi-clock system benchmarks.

Design and verification of systems at the Register-Transfer (RT) or behavioral level require the ability to reason at higher levels of abstraction. Difference logic consists of an arbitrary Boolean combination of propositional variables and difference predicates and therefore provides an appropriate abstraction. In this paper, we present several new optimization techniques for efficiently deciding difference logic formulas. We use the lazy approach by combining a DPLL Boolean SAT procedure with a dedicated graph-based theory solver, which adds transitivity constraints among difference predicates on a "need-to" basis. Our new optimization techniques include flexible theory constraint propagation, selective theory deduction, and dynamic predicate learning. We have implemented these techniques in our lazy solver. We demonstrate the effectiveness of the proposed techniques on public benchmarks through a set of controlled experiments.

SAT-based Bounded Model Checking (BMC) has been found promising in finding deep bugs in industry designs and scaling well with design sizes. However, it has limitations due to requirement of finite data paths, inefficient translations and loss of high-level design information during the BMC problem formulation. These shortcomings inherent in Boolean-level BMC can be avoided by using high-level BMC. We propose a novel framework for high-level BMC, which includes several techniques that extract high-level design information from EFSM models to make the verification model "BMC friendly", and use it on-the-fly to simplify the BMC problem instances. Such techniques overcome the inherent limitations of Boolean-level BMC, while allowing integration of state-of-the-art techniques for BMC. In our controlled experiments we found signficant performance improvements achievable by the proposed techniques.

Model checking of safety properties has taken a significant lead over non-safety properties in recent years. To bridge the gap, we propose dedicated SAT-based model checking algorithms for properties beyond safety. Previous bounded model checking (BMC) approaches have relied on either converting such properties to safety checking, or finding proofs by deriving termination criteria using loop-free path analysis. Instead, our approach uses a customized SAT-based formulation for bounded model checking of non-safety properties, and determines the completeness bounds for liveness using unbounded SAT-based analysis. Our main contributions are: 1) Customized property translations for LTL formulas for BMC, with novel features that utilize partitioning, learning, and incremental formulation. Customized translations not only improve the BMC performance significantly in comparison to standard monolithic LTL translations, but also allow efficient derivation and use of completeness bounds. Though we discuss the translation schemas for liveness, they can be easily extended to handle other LTL properties as well. 2) Customized formulations for determining completeness bounds for liveness using SAT-based unbounded model checking (UMC) rather than using loop-free path analysis. These formulations comprise greatest fixed-point and least fixed-point computations to efficiently handle nested properties using SAT-based quantification approaches. We show the effectiveness of our overall approach for checking liveness on public benchmarks and several industry designs.

We describe verification techniques for embedded memory systems using efficient memory modeling (EMM), without explicitly modeling each memory bit. We extend our previously proposed approach of EMM in bounded model checking (BMC) for a single read/write port single memory system, to more commonly occurring systems with multiple memories, having multiple read and write ports. More importantly, we augment such EMM to providing correctness proofs, in addition to finding real bugs as before. The novelties of our verification approach are in (a) combining EMM with a proof-based abstraction that preserves the correctness of a property up to a certain analysis depth of SAT-based BMC, and (b) modeling arbitrary initial memory state precisely and thereby providing inductive proofs using SAT-based BMC for embedded memory systems. Similar to the previous approach, we construct a verification model by eliminating memory arrays, but retaining the memory interface signals with their control logic and adding constraints on those signals at every analysis depth to preserve the data forwarding semantics. The size of these EMM constraints depends quadratically on the number of memory accesses and the number of read and write ports; and linearly on the address and data widths and the number of memories. We show the effectiveness of our approach on several industry designs and software programs.

With the success of formal verification techniques like equivalence checking and model checking for hardware designs, there has been growing interest in applying such techniques for formal analysis and automatic verification of software programs. This paper provides a brief tutorial on model checking of C programs. The essential approach is to model the semantics of C programs in the form of finite state systems by using suitable abstractions. The use of abstractions is key, both for modeling programs as finite state systems and for reducing the model sizes in order to manage verification complexity. We provide illustrative details of a verification platform called F-Soft, which provides a range of abstractions for modeling software, and uses customized SAT-based and BDD-based model checking techniques targeted for software.

We describe an efficient approach for SAT-based quantifier elimination that significantly improves the performance of pre-image and fixed-point computation in SAT-based unbounded symbolic model checking (UMC). The proposed method captures a larger set of new states per SAT-based enumeration step during quantifier elimination, in comparison to previous approaches. The novelty of our approach is in the use of circuit-based cofactoring to capture a large set of states, and in the use of a functional hashing based simplified circuit graph to represent the captured states. We also propose a number of heuristics to further enlarge the state set represented per enumeration, thereby reducing the number of enumeration steps. We have implemented our techniques in a SAT-based UMC framework where we show the effectiveness of SAT-based existential quantification on public benchmarks, and on a number of large industry designs that were hard to model check using purely BDD-based techniques. We show several orders of improvement in time and space using our approach over previous CNF-based approaches. We also present controlled experiments to demonstrate the role of several heuristics proposed in the paper. Importantly, we were able to prove using our method the correctness of a safety property in an industry design that could not be proved using other known approaches.

Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) procedures has recently gained popularity as an alternative to BDD-based model checking techniques for finding bugs in large designs. In this paper, we explore the use of learning from BDDs, where learned clauses generated by BDD-based analysis are added to the SAT solver, to supplement its other learning mechanisms. We propose several heuristics for guiding this process, aimed at increasing the usefulness of the learned clauses, while reducing the overheads. We demonstrate the effectiveness of our approach on several industrial designs, where BMC performance is improved and the design can be searched up to a greater depth by use of BDD-based learning.

Resolution-based proof analysis techniques have been proposed recently to identify a sufficient set of reasons for unsatisfiability derived by a CNF-based SAT solver. We have adapted these techniques to work with a hybrid SAT solver. We use the proof analysis technique with SAT-based BMC, in order to, generate useful abstract models. Our abstraction procedure is used iteratively in a top-down framework, starting from the concrete design, where we apply BMC on increasingly more abstract models. We apply various SAT-based and BDD-based verification methods on these abstract models, in order to obtain proofs of correctness, or to perform deeper searches for counterexamples. We demonstrate the effectiveness of our prototype implementation on several large industry designs.

We propose Satisfiability Checking (SAT) techniques that lead to a consistent performance improvement of up to 3x over state-of-the-art SAT solvers like Chaff on important problem domains in VLSI CAD. We observe that in circuit oriented applications like ATPG and verification, different software engineering techniques are required for the portions of the formula corresponding to learnt clauses compared to the original formula. We demonstrate that by employing the same innovations as in advanced CNF-based SAT solvers, but in a hybrid approach where these two portions of the formula are represented differently and processed separately, it is possible to obtain the consistently highest performing SAT solver for circuit oriented problem domains. We also present controlled experiments to highlight where these gains come from. Once it is established that the hybrid approach is faster, it becomes possible to apply low overhead circuit-based heuristics that would be unavailable in the CNF domain for greater speedup.

Many tasks in computer-aided design (CAD), such as equivalence checking, property checking, logic synthesis, and false paths analysis, require efficient Boolean reasoning for problems derived from circuits. Traditionally, canonical representations, e.g., binary decision diagrams (BDDs), or structural satisfiability (SAT) methods, are used to solve different problem instances. Each of these techniques offer specific strengths that make them efficient for particular problem structures. However, neither structural techniques based on SAT, nor functional methods using BDDs offer an overall robust reasoning mechanism that works reliably for a broad set of applications. The authors present a combination of techniques for Boolean reasoning based on BDDs, structural transformations, an SAT procedure, and random simulation natively working on a shared graph representation of the problem. The described intertwined integration of the four techniques results in a powerful summation of their orthogonal strengths. The presented reasoning technique was mainly developed for formal equivalence checking and property verification but can equally be used in other CAD applications. The authors' experiments demonstrate the effectiveness of the approach for a broad set of applications.

Many tasks in CAD, such as equivalence checking, property checking, logic synthesis, and false paths analysis require efficient Boolean reasoning for problems derived from circuit structures. Traditionally, canonical representations, e. g., BDDs, or SAT- based search methods are used to solve a particular class of problems. In this paper we present a combination of techniques for Boolean reasoning based on BDDs, structural transformations, and a SAT procedure natively working on a shared graph representation of the problem. The described intertwined integration of the three techniques results in a robust summation of their orthogonal strengths. Our experiments demonstrate the effectiveness of the approach.

State explosion is a common problem when verifying large designs. Partial state exploration using guided techniques has become a subject of wide research. We propose a rarity-based metric for state prioritization and several techniques which use the metric for enhanced state space search. These techniques use latch toggle activity and latch support for partitioning the design. The computation overhead for these techniques is minimal. Coverage results on the large industrial designs show the effectiveness of our approach.

We introduce Simulation Verification with Augmentation (SIVA), a tool for checking safety properties on digital hardware designs.SIVA integrates simulation with symbolic techniques for vector generation.Specifically, the core algorithm uses a combination of ATPG and BDDs to generate input vectors which cover behavior not excited by simulation.Experimental results demonstrate considerable improvement in state space coverage compared with either simulation or formal verification in isolation.