Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

Edmund Clarke
December 2005 - Technical Report Verification of Evolving Software via Component Substitutability Analysis

Topics: Software Architecture

Authors: Sagar Chaki, Edmund Clarke, Natasha Sharygina, Nishant Sinha

This 2005 report describes the application of the SEI Architecture Tradeoff Analysis Method (ATAM) to the U.S. Army's Warfighter Information Network-Tactical (WIN-T) system.

September 2005 - Technical Report SAT-Based Predicate Abstraction of Programs

Authors: Edmund Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav (IBM)

This note presents technical details of a SAT-based predicate abstraction technique used in ComFoRT (component formal reasoning technology).

June 2005 - White Paper Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog

Authors: Daniel Kroening, Natasha Sharygina, Edmund Clarke

This paper proposes to use predicate abstraction for verifying RTL Verilog, a technique successfully used for software verification.

October 2004 - White Paper Predicate Abstraction with Minimum Predicates

Authors: Sagar Chaki, Edmund Clarke

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