Publications of Mehmet Erkan Keremoglu
Articles in conference or workshop proceedings

Conditional Model Checking: A Technique to Pass Information between Verifiers.
In Tevfik Bultan and
Martin Robillard, editors,
Proceedings of the 20th ACM SIGSOFT International Symposium on the
Foundations of Software Engineering (FSE 2012, Cary, NC, November 1017),
2012.
ACM.
doi:10.1145/2393596.2393664
Keyword(s):
CPAchecker,
Software Model Checking
Publisher's Version
PDF
Supplement
Abstract
Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a spaceout, timeout, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the modelchecking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P usually a state predicate such that the program satisfies the specification under the condition P that is, as long as the program does not leave the states in which P is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.BibTeX Entry
@inproceedings{FSE12, author = {Dirk Beyer and Thomas A. Henzinger and M. Erkan Keremoglu and Philipp Wendler}, title = {Conditional Model Checking: {A} Technique to Pass Information between Verifiers}, booktitle = {Proceedings of the 20th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE~2012, Cary, NC, November 1017)}, editor = {Tevfik Bultan and Martin Robillard}, pages = {}, year = {2012}, publisher = {ACM}, isbn = {9781450316149}, doi = {10.1145/2393596.2393664}, url = {https://www.sosylab.org/research/cpacmc/}, pdf = {https://www.sosylab.org/research/pub/2012FSE.Conditional_Model_Checking.pdf}, abstract = {Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a spaceout, timeout, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the modelchecking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P usually a state predicate such that the program satisfies the specification under the condition P that is, as long as the program does not leave the states in which P is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.}, keyword = {CPAchecker,Software Model Checking}, } 
CPAchecker: A Tool for Configurable Software Verification.
In G. Gopalakrishnan and
S. Qadeer, editors,
Proceedings of the 23rd International Conference on
Computer Aided Verification (CAV 2011, Snowbird, UT, July 1420),
LNCS 6806,
pages 184190,
2011.
SpringerVerlag, Heidelberg.
doi:10.1007/9783642221101_16
Keyword(s):
CPAchecker,
Software Model Checking
Publisher's Version
PDF
Supplement
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, implements the interface of configurable program analysis (CPA). The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs. In software verification, it takes a considerable amount of effort to convert a verification idea into actual experimental results  we aim at accelerating this process. We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this flexible and easytoextend platform, and that it advances the field by making it easier to perform practical experiments. The tool is implemented in Java and runs as commandline tool or as Eclipse plugin. CPAchecker implements CPAs for several abstract domains. We evaluate the efficiency of the current version of our tool on softwareverification benchmarks from the literature, and compare it with other stateoftheart model checkers. CPAchecker is an opensource toolkit and publicly available.BibTeX Entry
@inproceedings{CAV11, author = {Dirk Beyer and M. Erkan Keremoglu}, title = {{{\sc CPAchecker}}: A Tool for Configurable Software Verification}, booktitle = {Proceedings of the 23rd International Conference on Computer Aided Verification (CAV~2011, Snowbird, UT, July 1420)}, editor = {G.~Gopalakrishnan and S.~Qadeer}, pages = {184190}, year = {2011}, series = {LNCS~6806}, publisher = {SpringerVerlag, Heidelberg}, isbn = {9783642221095}, doi = {10.1007/9783642221101_16}, sha256 = {0b9016de32b714f799da2cf19d3bf8f96cc33069db70beb2e22bbca07c58e2ee}, url = {https://cpachecker.sosylab.org}, 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, implements the interface of configurable program analysis (CPA). The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs. In software verification, it takes a considerable amount of effort to convert a verification idea into actual experimental results  we aim at accelerating this process. We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this flexible and easytoextend platform, and that it advances the field by making it easier to perform practical experiments. The tool is implemented in Java and runs as commandline tool or as Eclipse plugin. CPAchecker implements CPAs for several abstract domains. We evaluate the efficiency of the current version of our tool on softwareverification benchmarks from the literature, and compare it with other stateoftheart model checkers. CPAchecker is an opensource toolkit and publicly available.}, keyword = {CPAchecker,Software Model Checking}, } 
Predicate Abstraction with AdjustableBlock Encoding.
In Proceedings of the 10th International Conference on
Formal Methods in ComputerAided Design
(FMCAD 2010, Lugano, October 2023),
pages 189197,
2010.
FMCAD.
Keyword(s):
CPAchecker,
Software Model Checking
PDF
Supplement
Abstract
Several successful software model checkers are based on a technique called singleblock encoding (SBE), which computes costly predicate abstractions after every single program operation. Largeblock encoding (LBE) computes abstractions only after a large number of operations, and it was shown that this significantly improves the verification performance. In this work, we present adjustableblock encoding (ABE), a unifying framework that allows to express both previous approaches. In addition, it provides the flexibility to specify any block size between SBE and LBE, and also beyond LBE, through the adjustment of one single parameter. Such a unification of different concepts makes it easier to understand the fundamental properties of the analysis, and makes the differences of the variants more explicit. We evaluate different configurations on example C programs, and identify one that is currently the best.BibTeX Entry
@inproceedings{FMCAD10, author = {Dirk Beyer and M.~Erkan Keremoglu and Philipp Wendler}, title = {Predicate Abstraction with AdjustableBlock Encoding}, booktitle = {Proceedings of the 10th International Conference on Formal Methods in ComputerAided Design (FMCAD~2010, Lugano, October 2023)}, pages = {189197}, year = {2010}, publisher = {FMCAD}, isbn = {}, url = {http://www.sosylab.org/~dbeyer/cpaabe/}, pdf = {https://www.sosylab.org/research/pub/2010FMCAD.Predicate_Abstraction_with_AdjustableBlock_Encoding.pdf}, abstract = {Several successful software model checkers are based on a technique called singleblock encoding (SBE), which computes costly predicate abstractions after every single program operation. Largeblock encoding (LBE) computes abstractions only after a large number of operations, and it was shown that this significantly improves the verification performance. In this work, we present adjustableblock encoding (ABE), a unifying framework that allows to express both previous approaches. In addition, it provides the flexibility to specify any block size between SBE and LBE, and also beyond LBE, through the adjustment of one single parameter. Such a unification of different concepts makes it easier to understand the fundamental properties of the analysis, and makes the differences of the variants more explicit. We evaluate different configurations on example C programs, and identify one that is currently the best.}, keyword = {CPAchecker,Software Model Checking}, annote = {Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems}, doinone = {DOI not available}, }Additional Infos
Won the NRW Young Scientist Award 2010 in Dynamic Intelligent Systems 
Software Model Checking via LargeBlock Encoding.
In Proceedings of the 9th International Conference on
Formal Methods in ComputerAided Design
(FMCAD 2009, Austin, TX, November 1518),
pages 2532,
2009.
IEEE Computer Society Press, Los Alamitos (CA).
doi:10.1109/FMCAD.2009.5351147
Keyword(s):
CPAchecker,
Software Model Checking
Publisher's Version
PDF
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 controlflow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach singleblock 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 largeblock 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 abstractsuccessor 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 stateoftheart SMT solvers, which can symbolically compute abstract largeblock successors. Our experiments on benchmark C programs show that the largeblock encoding outperforms the singleblock encoding.BibTeX Entry
@inproceedings{FMCAD09, author = {Dirk Beyer and Alessandro Cimatti and Alberto Griggio and M.~Erkan Keremoglu and Roberto Sebastiani}, title = {Software Model Checking via LargeBlock Encoding}, booktitle = {Proceedings of the 9th International Conference on Formal Methods in ComputerAided Design (FMCAD~2009, Austin, TX, November 1518)}, pages = {2532}, year = {2009}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {9781424449668}, doi = {10.1109/FMCAD.2009.5351147}, url = {}, pdf = {https://www.sosylab.org/research/pub/2009FMCAD.Software_Model_Checking_via_LargeBlock_Encoding.pdf}, 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 controlflow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach singleblock 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 largeblock 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 abstractsuccessor 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 stateoftheart SMT solvers, which can symbolically compute abstract largeblock successors. Our experiments on benchmark C programs show that the largeblock encoding outperforms the singleblock encoding.}, keyword = {CPAchecker,Software Model Checking}, }
Internal reports

Conditional Model Checking.
Technical report MIP1107, Department of Computer Science and Mathematics (FIM),
University of Passau (PA),
September
2011.
Keyword(s):
CPAchecker,
Software Model Checking
PDF
Supplement
Abstract
Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a spaceout, timeout, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the modelchecking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P usually a state predicate such that the program satisfies the specification under the condition P that is, as long as the program does not leave states in which P is satisfied. We are of course interested in model checkers that return conditions P that are as weak as possible. Instead of outcome (1), the model checker will return P = true; instead of (2), the condition P will return the part of the state space that satisfies the specification; and in case (3), the condition P can summarize the work that has been performed by the model checker before spaceout, timeout, or giving up. If complete verification is necessary, then a different verification method or tool may be used to focus on the states that violate the condition. We give such conditions as input to a conditional model checker, such that the verification problem is restricted to the part of the state space that satisfies the condition. Our experiments show that repeated application of conditional model checkers, using different conditions, can significantly improve the verification results, statespace coverage, and performance.BibTeX Entry
@techreport{TR1107PA11, author = {Dirk Beyer and Thomas A. Henzinger and M. Erkan Keremoglu and Philipp Wendler}, title = {Conditional Model Checking}, number = {MIP1107}, year = {2011}, url = {https://www.sosylab.org/~dbeyer/cpacmc/}, pdf = {https://arxiv.org/abs/1109.6926}, abstract = {Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a spaceout, timeout, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the modelchecking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P usually a state predicate such that the program satisfies the specification under the condition P that is, as long as the program does not leave states in which P is satisfied. We are of course interested in model checkers that return conditions P that are as weak as possible. Instead of outcome (1), the model checker will return P = true; instead of (2), the condition P will return the part of the state space that satisfies the specification; and in case (3), the condition P can summarize the work that has been performed by the model checker before spaceout, timeout, or giving up. If complete verification is necessary, then a different verification method or tool may be used to focus on the states that violate the condition. We give such conditions as input to a conditional model checker, such that the verification problem is restricted to the part of the state space that satisfies the condition. Our experiments show that repeated application of conditional model checkers, using different conditions, can significantly improve the verification results, statespace coverage, and performance.}, keyword = {CPAchecker,Software Model Checking}, annote = {An abbreviated version of this article appeared in Proc. FSE 2012.}, institution = {Department of Computer Science and Mathematics (FIM), University of Passau (PA)}, month = {September}, }Additional Infos
An abbreviated version of this article appeared in Proc. FSE 2012. 
Software Model Checking via LargeBlock Encoding.
Technical report SFUCS200909, School of Computing Science (CMPT),
Simon Fraser University (SFU),
April
2009.
Keyword(s):
CPAchecker,
Software Model Checking
PDF
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 controlflow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach singleblock 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 largeblock 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 abstractsuccessor 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 stateoftheart SMT solvers, which can symbolically compute abstract largeblock successors. Our experiments on benchmark C programs show that the largeblock encoding outperforms the singleblock encoding.BibTeX Entry
@techreport{TR009SFU09, author = {Dirk Beyer and Alessandro Cimatti and Alberto Griggio and M. Erkan Keremoglu and Roberto Sebastiani}, title = {Software Model Checking via LargeBlock Encoding}, number = {SFUCS200909}, year = {2009}, url = {}, pdf = {https://arxiv.org/abs/0904.4709}, 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 controlflow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach singleblock 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 largeblock 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 abstractsuccessor 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 stateoftheart SMT solvers, which can symbolically compute abstract largeblock successors. Our experiments on benchmark C programs show that the largeblock encoding outperforms the singleblock encoding.}, keyword = {CPAchecker,Software Model Checking}, annote = {}, institution = {School of Computing Science (CMPT), Simon Fraser University (SFU)}, month = {April}, } 
CPAchecker: A Tool for Configurable Software Verification.
Technical report SFUCS200902, School of Computing Science (CMPT),
Simon Fraser University (SFU),
January
2009.
Keyword(s):
CPAchecker,
Software Model Checking
PDF
Supplement
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 commandline tool or as Eclipse plugin. 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 explicitvalue domains. Binaries and the source code of CPAchecker are publicly available as free software.BibTeX Entry
@techreport{TR002SFU09, author = {Dirk Beyer and M. Erkan Keremoglu}, title = {{CPAchecker}: A Tool for Configurable Software Verification}, number = {SFUCS200902}, year = {2009}, url = {http://www.sosylab.org/~dbeyer/CPAchecker/}, pdf = {https://arxiv.org/abs/0902.0019}, 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 commandline tool or as Eclipse plugin. 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 explicitvalue domains. Binaries and the source code of CPAchecker are publicly available as free software.}, keyword = {CPAchecker,Software Model Checking}, annote = {}, institution = {School of Computing Science (CMPT), Simon Fraser University (SFU)}, month = {January}, }
Theses and projects (PhD, MSc, BSc, Project)

Towards Scalable Software Analyisis Using Combinations and Conditions with CPAchecker.
PhD Thesis, Simon Fraser University, Software Systems Lab,
2011.
Keyword(s):
CPAchecker,
Software Model Checking
PDF
BibTeX Entry
@misc{ErkanCMC, author = {Mehmet Erkan Keremoglu}, title = {Towards Scalable Software Analyisis Using Combinations and Conditions with {{\sc CPAchecker}}}, year = {2011}, pdf = {http://summit.sfu.ca/system/files/iritems1/12363/etd7320_MKeremoglu.pdf}, keyword = {CPAchecker,Software Model Checking}, annote = {Now at Microsoft, Redmond, USA}, howpublished = {PhD Thesis, Simon Fraser University, Software Systems Lab}, }Additional Infos
Now at Microsoft, Redmond, USA
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.