Sample

Main content

Sample (Static Analyzer of Multiple Programming LanguagEs) is a generic static analyzer based on the abstract interpretation theory. This analyzer is generic with respect to:

  1. the heap analysis that approximates all runtime heap structures (we have already implemented some common analyses, and the interface of TVLA. Recently, we have developed and implemented a novel analysis capable of inferring precise invariants combining heap and value information),
  2. the semantic domain that infers the property of interest (that can be about numerical information like Apron, string values, types, ...),
  3. 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).

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

 

 
 
Page URL: http://www.pm.inf.ethz.ch/research/sample.html
Sun Mar 26 09:49:14 CEST 2017
© 2017 Eidgenössische Technische Hochschule Zürich