Automated Verification of Security Protocol Implementations (2008)
Sagar Chaki & Anupam Datta
This report presents a method that combines software model checking with a standard protocol security model (including a symbolic attacker) to provide analogous guarantees about protocol implementations as previous work does for protocol specifications.

Verification of Evolving Software via Component Substitutability (2005)
Sagar Chaki, Edmund Clarke, Natasha Sharygina, & Nishant Sinha

This report presents an automated and compositional procedure to solve the component substitutability problem. In particular, techniques are developed that exploit the results of previous verification efforts and focus only on the portions of the system that have changed (components). These new techniques incorporate model checking into development processes in a much less cumbersome manner than previous verification techniques.

Efficient Verification of Sequential and Concurrent C Programs (2004)
Sagar Chaki, Edmund Clarke, Alex Groce, Joel Ouaknine, Ofer Strichman, & Karen Yorav
The state-space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. We attempt to address these issues in the context of verifying concurrent (message-passing) C programs against safety specifications. We describe our approach in detail, and report on some very encouraging experimental results obtained with our tool MAGIC.

Predicate Abstraction with Minimum Predicates (2004)
Sagar Chaki, Edmund Clarke, Alex Groce, & Ofer Strichman

Predicate abstraction is a popular abstraction technique employed in formal software verification. Our experiments show that predicate minimization can result in a significant reduction of both verification time and memory usage compared to earlier methods.

An Expressive Verification Framework for State/Event Systems (2004)
Sagar Chaki, Edmund Clarke, Orna Grumberg, Joel Ouaknine, Natasha Sharygina, Tayssir Touili, & Helmut Veith
Specification languages for concurrent software systems need to combine practical algorithmic efficiency with high expressive power and the ability to reason about both states and events. We address this question by defining a new branching-time temporal logic SE-A which integrates both state-based and action-based properties. For experimental evaluation, we have integrated the presented algorithms in the software verification tool MAGIC.

State/Event-Based Software Model Checking (2004)
Sagar Chaki, Edmund Clarke, Joel Ouaknine, Natasha Sharygina, & Nishant Sinha

We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning.

Automated, Compositional and Iterative Deadlock Detection (2004)
Sagar Chaki, Edmund Clarke, Joel Ouaknine, & Natasha Sharygina

We present an algorithm to detect deadlocks in concurrent message-passing programs. Even though deadlock is inherently non-compositional and its absence is not preserved by standard abstractions, our framework employs both abstraction and compositional reasoning to alleviate the state space explosion problem.

Automated Assume-Guarantee Reasoning for Simulation Conformance (2005)
Sagar Chaki, Edmund Clarke, Nishant Sinha, & Prasanna Thati

This paper addresses the issue of efficiently automating assume-guarantee reasoning for simulation conformance between finite state systems and specifications. The authors focus on a non-circular assume-guarantee proof rule. We have implemented this framework in the COMFORT toolkit and we report encouraging results (over an order of magnitude improvement in memory consumption) on non-trivial benchmarks.

Certifying the Absence of Buffer Overflows (2006)
Sagar Chaki & Scott Hissam
This report presents a technique for certifying the safety of buffer manipulations in C programs. The approach is based on two key ideas: (1) using a certifying model checker to automatically verify that a buffer manipulation is safe and (2) validating the resulting invariant and proving it with a decision procedure based on Boolean satisfiability.

Precise Buffer Overflow Detection via Model Checking (2005)
Sagar Chaki & Scott Hissam
This white paper discusses an approach for precise detection of buffer overflows in C source code using model checking in combination with predicate abstraction and iterative counterexample driven refinement. It also compares and contrasts such an approach with existing buffer overflow detection techniques.

The ComFoRT Reasoning Framework (2005)
Sagar Chaki, James Ivers, Natasha Sharygina, & Kurt Wallnau

This paper provides a short description of the ComFoRT reasoning framework. It identifies the tools and techniques used to generate models from design specifications and to formally verify the models with temporal logic model checking.

Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach (2003)
Sagar Chaki, Joel Ouaknine, Karen Yorav, & Edmund Clarke

The state space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. We attempt to address this problem in the context of verifying concurrent (message-passing) C programs against safety specifications. To our knowledge, this is the first compositional use of CEGAR in the context of model checking concurrent C programs.

Assume-Guarantee Reasoning for Deadlock (2006)
Sagar Chaki & Nishant Sinha

In this report, the learning-based automated assume-guarantee paradigm is extended to perform compositional deadlock detection. A learning algorithm L^F is developed that constructs the minimal deterministic failure automaton accepting any unknown regular failure set using a minimally adequate teacher.

Assume-Guarantee Reasoning for Deadlock (2006)
Sagar Chaki & Nishant Sinha. Proceedings of the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD), page 134-141, November 12-16, 2006

We extend the learning-based automated assume guarantee paradigm to perform compositional deadlock detection. We define Failure Automata, a generalization of finite automata that accept regular failure sets. We develop a learning algorithm L^F that constructs the minimal deterministic failure automaton accepting any unknown regular failure set using a minimally adequate teacher. We show how L^F can be used for compositional regular failure language containment, and deadlock detection, using non-circular and circular assume guarantee rules. We present an implementation of our techniques and encouraging experimental results on several non-trivial benchmarks.

Optimized L*-Based Assume-Guarantee Reasoning (2007)
Sagar Chaki & Ofer Strichman

In this paper, we suggest three optimizations to the L*-based automated Assume-Guarantee reasoning algorithm for the compositional verification of concurrent systems.

"Finding Environment Guarantees" (2007)
Marsha Checknik, Mihaela Gheorghiu, & Arie Gurfinkel. Proceedings of 10th International Conference on Fundamental Approaches to Software Engineering (FASE'07), Braga, Portugal, March 2007

In this paper, we identify and formalize a problem related to environment models -- environment guarantees. It captures those cases where the correctness of the component under analysis is due solely to the model of its environment. Environment guarantees provides a model-based analog to a property-based notion of vacuity by identifying cases when the component is irrelevant to satisfaction of a property.

Finding State Solutions to Temporal Queries (2007)
Marsha Checknik, Mihaela Gheorghiu, & Arie Gurfinkel

In this paper, we propose a symbolic query-checking algorithm that finds "state" solutions to a temporal logic query. We argue that our approach generalizes previous specialized techniques, and this generality allows us to find new and interesting applications, such as finding stable states in a gene network. The approach has been implemented on top of the model checker NuSMV.

A Framework for Counterexample Generation and Exploration (2007)
Marsha Chechik & Arie Gurfinkel

In this paper, we present a framework for generating, structuring, and exploring counterexamples produced by a model checker. The counterexamples are presented in a proof-like form that gives the user the navigational flexibility, but without sacrificing any of the intuitiveness and close relation to the model.

Predicate Abstraction and Refinement Techniques for Verifying Verilog (2004)
Ed Clarke, Himanshu Jain, Daniel Kroening, & Natasha Sharygina

Model checking techniques applied to large industrial circuits suffer from the state space explosion problem. A major technique to address this problem is abstraction. This paper proposes to use predicate abstraction for verifying RTL Verilog, a technique successfully used for software verification. We compare the performance of our technique with a modern model checker that implements localization reduction.

Predicate Abstraction of ANSI-C Programs Using SAT (2004)
Edmund Clarke, Daniel Kroening, Natasha Sharygina, & Karen Yorav

Predicate abstraction is a major method for verification of software. However, the generation of the abstract Boolean program from the set of predicates and the original program suffers from an exponential number of theorem prover calls as well as from soundness issues. This paper presents a novel technique that uses an efficient SAT solver for generating the abstract transition relations of ANSI-C programs.

"Dynamic Component Substitutability Analysis”
Sagar Chaki, Edmund Clarke, Natasha Sharygina, & Nishant Sinha. Proceedings of Formal Methods (FM), 2005.

This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. The substitutability approach has been implemented and validated in the COMFORT model checking tool set and we report encouraging results on an industrial benchmark.

Verification of Evolving Software via Component Substitutability Analysis (2008)
Sagar Chaki, Edmund Clarke, Natasha Sharygina, & Nishant Sinha

This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. Our solution contributes two techniques for checking correctness of software upgrades: (1) a technique based on simultaneous use of over-and under-approximations obtained via existential and universal abstractions; (2) a dynamic assume-guarantee reasoning algorithm--previously generated component assumptions are reused and altered on-the-fly to prove or disprove the global safety properties on the updated system. When upgrades are found to be non-substitutable, our solution generates constructive feedback to developers showing how to improve the components. The substitutability approach has been implemented and validated in the ComFoRT reasoning framework, and we report encouraging results on an industrial benchmark.

Three Optimizations for Assume-Guarantee Reasoning with L* (2008)
Sagar Chaki & Ofer Strichman

The learning-based automated Assume---Guarantee reasoning paradigm has been applied in the last few years for the compositional verification of concurrent systems. Specifically, L* has been used for learning the assumption, based on strings derived from counterexamples, which are given to it by a model-checker that attempts to verify the Assume---Guarantee rules. We suggest three optimizations to this paradigm. First, we derive from each counterexample multiple strings to L*, rather than a single one as in previous approaches. This small improvement saves candidate queries and hence model-checking runs. Second, we observe that in existing instances of this paradigm, the learning algorithm is coupled weakly with the teacher. Thus, the learner completely ignores the details of the internal structure of the system and specification being verified, which are available already to the teacher. We suggest an optimization that uses this information in order to avoid many unnecessary membership queries (it reduces the number of such queries by more than an order of magnitude). Finally, we develop a method for minimizing the alphabet used by the assumption, which reduces the size of the assumption and the number of queries required to construct it. We present these three optimizations in the context of verifying trace containment for concurrent systems composed of finite state machines. We have implemented our approach in the ComFoRT tool, and experimented with real-life examples. Our results exhibit an average speedup of between 4 to 11 times, depending on the Assume---Guarantee rule used and the set of activated optimizations.

Algorithmic Analysis of Piecewise FIFO Systems (2007)
Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, & Richard Trefler. Proceedings of 7th International Conference on Formal Methods in Computer Aided Design (FMCAD'07), Austin, TX, USA, November 2007

In this paper, we present two algorithms for computing the set of reachable states of a FIFO system composed of piecewise components. We consider arbitrary systems with a single communication channel, and multi-channel systems with acyclic communication structure.

"Combining Predicate and Numeric Abstraction for Software Model Checking"  (2008)
Arie Gurfinkel & Sagar Chaki. Proceedings of the Sixth NASA Langley Formal Methods Workshop (LFM), April-May 2008.

Lessons Learned Model Checking an Industrial Communications Library (2005)
James Ivers

This report describes early experiments with packaging model checking as a reasoning framework. It describes the verification of an industrial communications library and the problems found with the library and the verification process.

Overview of ComFoRT: A Model Checking Reasoning Framework (2004)
James Ivers & Natasha Sharygina

ComFoRT is a reasoning framework that packages the effectiveness of state-of-the-art model checking in a form that enables users to perform formal verification without becoming a model checking expert. This report describes the techniques used to automate verification of design specifications and the model checking algorithms used within ComFoRT.

Preserving Real Concurrency (2003)
James Ivers & Kurt Wallnau

This paper sketches a method for modeling and composing component behavior (using CCL) in a manner that ensures that model concurrency matches implementation concurrency. This is a refinement of some of the ideas in A Basis for Composition Language (CMU/SEI-2002-TN-026), and is based on UML rather than CSP to promote transition.

Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC (2007)
Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, & Marsha Chechik

In this paper, we explore how resolution proofs from a run of a bounded model checker (BMC) can be mined for temporal vacuity. We present a vacuity detection tool, VaqTree, that uses these methods to detect vacuous variables, decreasing the total number of model-checking runs required to detect all sources of vacuity.

COGENT: Accurate Theorem Proving for Program Verification (2005)
Byron Cook, Daniel Kroening, & Natasha Sharygina

Many symbolic software verification engines such as Slam and ESC/Java rely on automatic theorem provers. This paper describes a theorem prover, Cogent, that accurately supports all ANSI-C expressions. When used by Slam during the model checking of over 300 benchmarks, Cogent’s improved accuracy reduced the number of Slam timeouts by half, increased the number of true errors found, and decreased the number of false errors.