SAT-Based Software Certification (2006)
Sagar Chaki

This paper presents an automated technique for certifying a program's adherence to safety and liveness criteria. The technique consists of two broad stages. In the first stage, a certifying model checker is used to generate a verification condition (VC). In the second stage, a decision procedure based on Boolean satisfiability (SAT) is used to prove the VC. The use of SAT enables us to construct extremely compact proofs..

SAT-Based Software Certification (2006)
Sagar Chaki

This technical note presents a framework for constructing extremely compact proofs of the satisfaction of safety and liveness specifications by source code. The approach is based on a combination of certifying model checking and Boolean satisfiability (SAT) technology.

Verification Across Intellectual Property Boundaries (2007)
Sagar Chaki, Christian Schallhart, & Helmut Veith

This paper presents a cryptographic approach for software certification.

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.

Certified Binaries for Software Components (2007)
Sagar Chaki, James Ivers, Peter Lee, Kurt Wallnau, & Noam Zeilberger

This report presents an approach to automatically certify that binary code satisfies user specifiable behavioral requirements. The approach builds on proof-carrying code and certifying model checking research and generates a proof certificate that can be independently verified, allowing developers to trust the code that is produced without having to trust the tools that produced it.

Model-Driven Construction of Certified Binaries (2007)
Sagar Chaki, James Ivers, Peter Lee, Kurt Wallnau, & Noam Zeilberger

This paper presents a model-driven approach for generating certified binaries (executables) from component specifications.

Predictable Assembly of Substation Automation Systems: An Experiment Report (2002)
Scott Hissam, John Hudak, James Ivers, Mark Klein, Magnus Larsson, Gabriel Moreno, Linda Northrop, Daniel Plakosh, Judith Stafford, Kurt Wallnau, & William Wood

This reports the results of a PECT feasibility study the PACC team performed for ABB in the domain of power substation automation. It is representative of our approach and documents a number of important concepts, especially the notions of co-refinement and empirical validation.

The Potential for Synergy between Certification and Insurance.” First International Workshop on Software Reuse Economics (2002)
Paul Luo Li, Mary Shaw, Kevin Stolarick, & Kurt Wallnau

Written with the help of an expert in actuarial models and insurance, this paper argues that predictability of assembly behavior is a useful prerequisite for for-profit insurance of component quality and behavior.

Statistical Models for Empirical Component Properties and Assembly-Level Property Predictions: Toward Standard Labeling (2002)
Gabriel Moreno, Scott Hissam, & Kurt Wallnau

The paper provides a short tutorial on various types of statistical analyses used to describe measurable properties of components and assembly predictions, leading to a position statement regarding a form of standard component label.

Is Third Party Certification Necessary? (2002)
Judith Stafford & Kurt Wallnau

The paper offers speculations on the roles and interactions among these roles for various stakeholders in certifying properties of software components.

Software Component Certification: 10 Useful Distinctions (2004)
Kurt C. Wallnau

Certification is a practical, proven means of establishing trust in various sorts of things in other disciplines and is, therefore, a natural contender for developing trust in software components. This technical note introduces a series of 10 distinctions that can help in understanding different aspects of certification in the context of software components.