Sample
Sample (Static Analyzer of Multiple Programming LanguagEs) is a generic static analyzer based on the external pageabstract interpretation theory. This analyzer is generic with respect to:
- the heap analysis that approximates all runtime heap structures (We have developed and implemented a novel analysis capable of inferring precise invariants combining heap and value information),
- the semantic domain that infers the property of interest (that can be about numerical information like external pageApron, string values, types, ...),
- the analyzed language since Sample works on an intermediate language called Simple (we have already developed the translation from Scala and Java bytecode to Simple).
Project Members
The project has been completed. Please contact Peter Müller in case of questions or comments.
Tool Structure
The figure above depicts the overall structure of Sample. Our analyzer can be used by developers to prove properties or infer contracts. It also serves as a platform for researchers, who want to develop, implement, and test new analyses. The main components of Sample are the following:
- The green component ("source code") is the code to be analyzed.
- Blue components represent the part of Sample that can be extended. Researchers can develop and interface translations from various languages to Simple ("compiler to Simple"), the inference of new properties ("semantic analysis"), particular abstractions of heap structures ("heap analysis"), the inference of specific contracts ("contract inference"), and checks of new properties ("property checker"). Sample provides a standard set of these components, like a translation from Scala to Simple and some numerical domains.
- Red components are the core of Sample. These consist of the Simple language, a fixpoint engine that computes an overapproximation of all possible executions, and the representation of the results of the analysis on a control flow graph. These components can neither be modified nor extended.
- Black components represent the output of Sample to developers, such as warnings (if the analysis is not able to prove that all executions respect a given property) or inferred contracts.
Key Publications
- P. Ferrara and P. Müller and M. Novacek: Automatic Inference of Heap Properties Exploiting Value Domains
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2015. [PDF][BIB] - P. Ferrara: Generic Combination of Heap and Value Analyses in Abstract Interpretation
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2014. [PDF][BIB] - P. Ferrara and R. Fuchs and U. Juhasz: TVAL+ : TVLA and Value Analyses Together
Software Engineering and Formal Methods (SEFM), 2012. [PDF] [BIB] - P. Ferrara and P. Müller: Automatic inference of access permissions
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2012. [PDF][BIB]