CERT-SEI

Copper Model Checker

Copper is a software model checker for concurrent message-passing C programs. It can be used to analyze whether a program will satisfy its safety, reliability, or security requirements.

At the core of of ComFoRT lies Copper, a software model checker for concurrent C programs whose components communicate via message-passing and shared variables. The development of Copper began originally as collaborative work with the MAGIC project at Carnegie Mellon’s School of Computer Science, but has since become fairly independent.

Copper serves both as a toolbed for developing and nurturing techniques related to software verification and certification, as well as a vehicle for promoting wider adoption of such techniques amongst practitioners. As such, Copper incorporates a range of ideas and algorithms that have reached varying degrees of sophistication. These ideas fall broadly into the following categories, arranged (roughly) in order of decreasing maturity.

Counterexample-Guided Abstraction Refinement. Copper implements a Counterexample-Guided Abstraction Refinement (CEGAR) framework to verify infinite state C programs. In the CEGAR paradigm shown below, finite conservative abstractions (a.k.a. models) of the target program are constructed using predicate abstraction and iteratively refined on the basis of spurious counterexamples. The process continues until either the desired property is found to hold or an actual counterexample is discovered.

The CEGAR framework implemented in Copper

The CEGAR framework implemented in Copper is compositional and targeted specifically towards the verification of concurrent message-passing C programs. More precisely, Copper performs abstraction, counterexample validation, and abstraction refinement in a component-wise manner [1]. Such a modular approach—along with techniques such as two-level abstraction refinement [2] and predicate minimization [3]—enable Copper to alleviate statespace explosion.

State/Event-based Software Model Checking. ComFoRT uses a hybrid state/event-based formalism to model program behavior as well as to specify the behavioral assertions to be verified. In particular, the abstract models constructed by Copper are finite Labeled Kripke Structures (LKSs). An LKS is a state machine whose states are labeled with atomic propositions (denoting constraints on program variables) and whose transitions are labeled with actions (modeling observable events). In addition, we have developed state/event-based linear [4] and branching time [5] temporal logics to specify desired system properties, as well as efficient model checking algorithms to verify specifications expressed in such logics.

SAT-based Predicate Abstraction. Together with colleagues from Carnegie Mellon’s School of Computer Science, we have developed a technique [7,8,9] for computing accurate predicate abstractions of software and hardware written in ANSI-C and SystemC by enumerating assignments to a single SAT instance. Our approach does not require an exponential number of theorem prover calls, unlike most existing predicate abstraction tools. Another advantage of the SAT-based approach is that it enables us to model arithmetic overflow, bit vector manipulations, pointers, and arrays. This is crucial for sound modeling of real-world systems.

Automated Assume-Guarantee Reasoning. We are also working on making the model checking step of the CEGAR loop compositional. In particular, we have investigated the use of learning algorithms to automate assume-guarantee style verification [10,14] of concurrent systems.

Compositional Deadlock Detection. We have developed two compositional algorithms to detect deadlocks in concurrent message-passing programs: one based on iterative abstraction refinement [6], and the other on automated assume-guarantee reasoning [13] via learning.

Software Certification. Copper is a certifying software model checker, capable of generating ranking functions when it is able to prove a safety or liveness claim. So far, we have used this feature of Copper in two projects: one on constructing compact proofs of correctness [15] via a SAT-based theorem prover; and the other on automated generation of certified binaries from software component specifications.

Component Substitutability. We have also proposed a formal notion of substitutability [11] of a software component with another and developed efficient algorithms [12] to check for substitutability between components of evolving concurrent software systems.

Download Copper

To get Copper, visit our Downloads page.  

Additional Information

For more information about Copper, see the Copper User Manual and the Copper Tutorial. Direct technical questions to us at info@sei.cmu.edu.

References

[1] Chaki, Sagar; Clarke, Edmund; Groce, Alex; Ouaknine, Joel; Strichman, Ofer; & Yorav, Karen. “Efficient Verification of Sequential and Concurrent C Programs.” Formal Methods in System Design (FMSD) 25, 2-3 (September-November 2004): 129-166.

[2] Chaki, Sagar; Ouaknine, Joel; Yorav, Karen; Clarke, Edmund. “Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach.”2nd Workshop on Software Model Checking (SoftMC) 2003, ENTCS 89(3). Boulder, Colorado, July 14, 2003. 

[3] Chaki, Sagar; Clarke, Edmund; Groce, Alex; & Strichman, Ofer. “Predicate Abstraction with Minimum Predicates.” Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) 2003 (Lecture Notes in Computer Science [LNSC] volume 2860). L’Aquila, Italy, October 21-24, 2004. 

[4] Chaki, Sagar; Clarke, Edmund; Ouaknine, Joel; Sharygina, Natasha; & Sinha, Nishant. “State/Event-based Software Model Checking.” Fourth International Conference on Integrated Formal Methods (IFM) 2004 (Lecture Notes in Computer Science [LNCS] volume 2999). Kent England, April 4-7, 2004. 

[5] Chaki, Sagar; Clarke, Edmund; Grumberg, Orna; Ouaknine, Joel; Sharygina, Natasha; Touili, Tayssir; & Veith, Helmut. An Expressive Verification Framework for State/Event Systems (CMU-CS-04-145). Pittsburgh, PA: Computer Science Department, School of Computer Science, Carnegie Mellon University, 2004.

[6] Chaki, Sagar; Clarke, Edmund; Ouaknine, Joel; & Sharygina, Natasha. “Automated, Compositional and Iterative Deadlock Detection.” Proceedings of the Second ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) 2004. San Diego, CA, June 22-25, 2004.

[7] Cook, Byron; Kroening, Daniel; & Sharygina, Natasha. “COGENT: Accurate Theorem Proving for Program Verification.” Proceedings of the Computer-Aided Verification (CAV) 2005 Conference

[8] Clarke, Ed; Jain, Himanshu; Kroening, Daniel; & Sharygina, Natasha. “Predicate Abstraction and Refinement Techniques for Verifying Verilog.” Proceedings of the DAC (Design and Automation) 2005 International Conference

[9] Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; & Yorav, Karen. “Predicate Abstraction of ANSI-C Programs Using SAT.” Formal Methods in System Design 25, 2 (2004): 105 - 127. 

[10]  Chaki, Sagar; Clarke, Edmund; Sinha, Nishant; & Thati, Prasanna. “Automated Assume-Guarantee Reasoning for Simulation Conformance.” Proceedings of Computer Aided Verification (CAV), 2005.

[11]  Chaki, Sagar; Sharygina, Natasha; & Sinha, Nishant. "Verification of Evolving Software." Proceedings of the Third Workshop on Specification and Verification of Component-Based Systems (SAVCBS) 2004.

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

[13] Chaki, Sagar; & Sinha, Nishant.  Assume-Guarantee Reasoning for Deadlock.

[14] Chaki, Sagar; & Strichman, Ofer. “ Optimized L*-Based Assume-Guarantee Reasoning.” Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007.

[15] Chaki, Sagar. “ SAT-Based Software Certification.