Publications of year 2009

Articles in conference or workshop proceedings

  1. Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, and Roberto Sebastiani. Software Model Checking via Large-Block Encoding. In Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009, Austin, TX, November 15-18), pages 25-32, 2009. IEEE Computer Society Press, Los Alamitos (CA). [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Several successful approaches to software verification are based on the construction and analysis of an abstract reachability tree (ART). The ART represents unwindings of the control-flow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach single-block encoding (SBE). SBE may result in a huge number of program paths to be explored, which constitutes a fundamental source of inefficiency. We propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; we call this approach large-block encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially. Within this framework, we also investigate symbolic representations: for representing abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; for computing abstract-successor states, in addition to Cartesian predicate abstraction as used in SBE, we investigate the use of Boolean predicate abstraction. The new encoding leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors. Our experiments on benchmark C programs show that the large-block encoding outperforms the single-block encoding.

    @InProceedings{FMCAD09,
    author = {Dirk Beyer and Alessandro Cimatti and Alberto Griggio and M.~Erkan Keremoglu and Roberto Sebastiani},
    title = {Software Model Checking via Large-Block Encoding},
    booktitle = {Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD~2009, Austin, TX, November 15-18)},
    publisher = {IEEE Computer Society Press, Los Alamitos~(CA)},
    pages = {25-32},
    year = {2009},
    isbn = {978-1-4244-4966-8},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2009-FMCAD.Software_Model_Checking_via_Large-Block_Encoding.pdf},
    url = {},
    abstract = { Several successful approaches to software verification are based on the construction and analysis of an abstract reachability tree (ART). The ART represents unwindings of the control-flow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach single-block encoding (SBE). SBE may result in a huge number of program paths to be explored, which constitutes a fundamental source of inefficiency. We propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; we call this approach large-block encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially. Within this framework, we also investigate symbolic representations: for representing abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; for computing abstract-successor states, in addition to Cartesian predicate abstraction as used in SBE, we investigate the use of Boolean predicate abstraction. The new encoding leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors. Our experiments on benchmark C programs show that the large-block encoding outperforms the single-block encoding. },
    
    }
    

Internal reports

  1. Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, and Roberto Sebastiani. Software Model Checking via Large-Block Encoding. Technical report SFU-CS-2009-09, School of Computing Science (CMPT), Simon Fraser University (SFU), April 2009. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    The construction and analysis of an abstract reachability tree (ART) are the basis for a successful method for software verification. The ART represents unwindings of the control-flow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach single-block encoding (SBE). SBE may result in a huge number of program paths to be explored, which constitutes a fundamental source of inefficiency. We propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; we call this approach large-block encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially. Within this framework, we also investigate symbolic representations: for representing abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; for computing abstract-successor states, in addition to Cartesian predicate abstraction as used in SBE, we investigate the use of Boolean predicate abstraction. The new encoding leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors. Our experiments on benchmark C programs show that the large-block encoding outperforms the single-block encoding.
    Annotation:
    Online: http://arxiv.org/abs/0904.4709

    @TechReport{TR009-SFU09,
    author = {Dirk Beyer and Alessandro Cimatti and Alberto Griggio and M. Erkan Keremoglu and Roberto Sebastiani},
    title = {Software Model Checking via Large-Block Encoding},
    institution ={School of Computing Science (CMPT), Simon Fraser University (SFU)},
    number = {SFU-CS-2009-09},
    month = {April},
    year = {2009},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2009-SFU-TR009.Software_Model_Checking_via_Large-Block_Encoding.pdf},
    url = {},
    abstract = { The construction and analysis of an abstract reachability tree (ART) are the basis for a successful method for software verification. The ART represents unwindings of the control-flow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach single-block encoding (SBE). SBE may result in a huge number of program paths to be explored, which constitutes a fundamental source of inefficiency. We propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; we call this approach large-block encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially. Within this framework, we also investigate symbolic representations: for representing abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; for computing abstract-successor states, in addition to Cartesian predicate abstraction as used in SBE, we investigate the use of Boolean predicate abstraction. The new encoding leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors. Our experiments on benchmark C programs show that the large-block encoding outperforms the single-block encoding. },
    annote = {Online:  http://arxiv.org/abs/0904.4709 
    }, }

  2. Dirk Beyer and M. Erkan Keremoglu. CPAchecker: A Tool for Configurable Software Verification. Technical report SFU-CS-2009-02, School of Computing Science (CMPT), Simon Fraser University (SFU), January 2009. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Configurable software verification is a recent concept for expressing different program analysis and model checking approaches in one single formalism. This paper presents CPAchecker, a tool and framework that aims at easy integration of new verification components. Every abstract domain, together with the corresponding operations, is required to implement the interface of configurable program analysis (CPA). The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs. The major design goal during the development was to provide a framework for developers that is flexible and easy to extend. We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this platform and that it advances the field by making it easier to perform practical experiments. The tool is implemented in Java and runs as command-line tool or as Eclipse plug-in. We evaluate the efficiency of our tool on benchmarks from the software model checker BLAST. The first released version of CPAchecker implements CPAs for predicate abstraction, octagon, and explicit-value domains. Binaries and the source code of CPAchecker are publicly available as free software.
    Annotation:
    Online: http://arxiv.org/abs/0902.0019

    @TechReport{TR002-SFU09,
    author = {Dirk Beyer and M. Erkan Keremoglu},
    title = {{CPAchecker}: A Tool for Configurable Software Verification},
    institution ={School of Computing Science (CMPT), Simon Fraser University (SFU)},
    number = {SFU-CS-2009-02},
    month = {January},
    year = {2009},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2009-SFU-TR002.CPAchecker_A_Tool_for_Configurable_Software_Verification.pdf},
    url = {http://www.sosy-lab.org/~dbeyer/CPAchecker/},
    abstract = { Configurable software verification is a recent concept for expressing different program analysis and model checking approaches in one single formalism. This paper presents CPAchecker, a tool and framework that aims at easy integration of new verification components. Every abstract domain, together with the corresponding operations, is required to implement the interface of configurable program analysis (CPA). The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs. The major design goal during the development was to provide a framework for developers that is flexible and easy to extend. We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this platform and that it advances the field by making it easier to perform practical experiments. The tool is implemented in Java and runs as command-line tool or as Eclipse plug-in. We evaluate the efficiency of our tool on benchmarks from the software model checker BLAST. The first released version of CPAchecker implements CPAs for predicate abstraction, octagon, and explicit-value domains. Binaries and the source code of CPAchecker are publicly available as free software. },
    annote = {Online:  http://arxiv.org/abs/0902.0019 
    }, }




Disclaimer:

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.




Last modified: Mon Dec 18 14:34:44 2017


This document was translated from BibTEX by bibtex2html