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

Digital Library

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

Topics: Software Architecture

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

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

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

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.