Paper Info
Title
Certification for configurable program analysis
Abstract
Configurable program analysis (CPA) is a generic concept for the formalization of different software analysis techniques in a single framework. With the tool CPAchecker, this framework allows for an easy configuration and subsequent automatic execution of analysis procedures ranging from data-flow analysis to model checking. The focus of the tool CPAchecker is thus on analysis. In this paper, we study configurability from the point of view of software certification. Certification aims at providing (via a prior analysis) a certificate of correctness for a program which is (a) tamper-proof and (b) more efficient to check for validity than a full analysis. Here, we will show how, given an analysis instance of a CPA, to construct a corresponding sound certification instance, thereby arriving at configurable program certification. We report on experiments with certification based on different analysis techniques, and in particular explain which characteristics of an underlying analysis allow us to design an efficient (in the above (b) sense) certification procedure.
Year
DOI
Venue
2014
10.1145/2632362.2632372
SPIN
Keywords
Field
DocType
proof carrying code,software/program verification,certification,program analysis,configuration,semantics of programming languages
Model checking,Software engineering,Software analysis pattern,Computer science,Correctness,Proof-carrying code,Certification path validation algorithm,Program analysis,Certification,CPAchecker
Conference
Citations 
PageRank 
References 
10
0.49
22
Authors
2
Name
Order
Citations
PageRank
Marie-Christine Jakobs1325.51
Heike Wehrheim21013104.85