Publications of year 2013

Books and proceedings

  1. Dirk Beyer and Michele Boreale, editors. Proceedings of the 2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems (33rd FORTE / 15th FMOODS), LNCS 7892, 2013. Springer-Verlag, Heidelberg.
    @Proceedings{FORTE13,
    editor = {Dirk Beyer and Michele Boreale},
    title = {Proceedings of the 2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems (33rd FORTE / 15th FMOODS)},
    publisher = {Springer-Verlag, Heidelberg},
    series = {LNCS~7892},
    year = {2013},
    isbn = {978-3-642-38591-9},
    doi = {https://doi.org/10.1007/978-3-642-38592-6},
    
    }
    

Articles in conference or workshop proceedings

  1. Sven Apel, Dirk Beyer, Karlheinz Friedberger, Franco Raimondi, and Alexander von Rhein. Domain Types: Abstract-Domain Selection Based on Variable Usage. In V. Bertacco and A. Legay, editors, Proceedings of the 9th Haifa Verification Conference (HVC 2013, Haifa, Israel, November 5-7), LNCS 8244, pages 262–278, 2013. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    The success of software model checking depends on finding an appropriate abstraction of the program to verify. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types (e.g., `int' and `long') to guide the selection of an appropriate abstract domain for a model checker. Our implementation on top of an existing verification framework determines the domain type for each variable in a pre-analysis step, based on the usage of variables in the program, and then assigns each variable to an abstract domain. Based on a series of experiments on a comprehensive set of verification tasks from international verification competitions, we demonstrate that the choice of the abstract domain per variable (we consider one explicit and one symbolic domain) can substantially improve the verification in terms of performance and precision.

    @InProceedings{HVC13,
    author = {Sven Apel and Dirk Beyer and Karlheinz Friedberger and Franco Raimondi and Alexander von Rhein},
    title = {Domain Types: Abstract-Domain Selection Based on Variable Usage},
    booktitle = {Proceedings of the 9th Haifa Verification Conference (HVC 2013, Haifa, Israel, November 5-7)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {V.~Bertacco and A.~Legay},
    series = {LNCS~8244},
    pages = {262–278},
    year = {2013},
    isbn = {978-3-319-03076-0},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2013-HVC.Domain_Types_Abstract-Domain_Selection_Based_on_Variable_Usage.pdf},
    url = {},
    doi = {10.1007/978-3-319-03077-7_18},
    abstract = { The success of software model checking depends on finding an appropriate abstraction of the program to verify. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types (e.g., `int' and `long') to guide the selection of an appropriate abstract domain for a model checker. Our implementation on top of an existing verification framework determines the domain type for each variable in a pre-analysis step, based on the usage of variables in the program, and then assigns each variable to an abstract domain. Based on a series of experiments on a comprehensive set of verification tasks from international verification competitions, we demonstrate that the choice of the abstract domain per variable (we consider one explicit and one symbolic domain) can substantially improve the verification in terms of performance and precision. },
    
    }
    

  2. Sven Apel, Alexander von Rhein, Philipp Wendler, Armin Grösslinger, and Dirk Beyer. Strategies for Product-Line Verification: Case Studies and Experiments. In D. Notkin, B. H. C. Cheng, and K. Pohl, editors, Proceedings of the 35th International Conference on Software Engineering (ICSE 2013, San Francisco, CA, USA, May 18-26), pages 482-491, 2013. IEEE. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Product-line technology is increasingly used in mission-critical and safety-critical applications. Hence, researchers are developing verification approaches that follow different strategies to cope with the specific properties of product lines. While the research community is discussing the mutual strengths and weaknesses of the different strategies---mostly at a conceptual level---there is a lack of evidence in terms of case studies, tool implementations, and experiments. We have collected and prepared six product lines as subject systems for experimentation. Furthermore, we have developed a model-checking tool chain for C-based and Java-based product lines, called SPLverifier, which we use to compare sample-based and family-based strategies with regard to verification performance and the ability to find defects. Based on the experimental results and an analytical model, we revisit the discussion of the strengths and weaknesses of product-line--verification strategies.

    @InProceedings{ICSE13,
    author = {Sven Apel and Alexander von Rhein and Philipp Wendler and Armin Gr{\"o}{\ss}linger and Dirk Beyer},
    title = {Strategies for Product-Line Verification: Case Studies and Experiments},
    booktitle = {Proceedings of the 35th International Conference on Software Engineering (ICSE~2013, San Francisco, CA, USA, May 18-26)},
    publisher = {IEEE},
    editor = {D.~Notkin and B.~H.~C.~Cheng and K.~Pohl},
    pages = {482-491},
    year = {2013},
    isbn = {978-1-4673-3076-3},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2013-ICSE.Strategies_for_Product-Line_Verification.pdf},
    url = {},
    abstract = { Product-line technology is increasingly used in mission-critical and safety-critical applications. Hence, researchers are developing verification approaches that follow different strategies to cope with the specific properties of product lines. While the research community is discussing the mutual strengths and weaknesses of the different strategies---mostly at a conceptual level---there is a lack of evidence in terms of case studies, tool implementations, and experiments. We have collected and prepared six product lines as subject systems for experimentation. Furthermore, we have developed a model-checking tool chain for C-based and Java-based product lines, called SPLverifier, which we use to compare sample-based and family-based strategies with regard to verification performance and the ability to find defects. Based on the experimental results and an analytical model, we revisit the discussion of the strengths and weaknesses of product-line--verification strategies. },
    
    }
    

  3. Dirk Beyer. Second Competition on Software Verification (Summary of SV-COMP 2013). In N. Piterman and S. Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2013, Rome, Italy, March 16-24), LNCS 7795, pages 594-609, 2013. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    This report describes the 2nd International Competition on Software Verification (SV-COMP 2013), which is the second edition of this thorough evaluation of fully automatic verifiers for software programs. The reported results represent the 2012 state-of-the-art in automatic software verification, in terms of effectiveness and efficiency. The benchmark set of verification tasks consists of eleven categories containing a total of 2315 programs, written in C, and exposing features of integers, heap-data structures, bit-vector operations, and concurrency; the properties include reachability and memory safety. The competition is again organized as a satellite event of TACAS.

    @InProceedings{TACAS13,
    author = {Dirk Beyer},
    title = {Second Competition on Software Verification ({S}ummary of {SV-COMP} 2013)},
    booktitle = {Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS~2013, Rome, Italy, March 16-24)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {N.~Piterman and S.~Smolka},
    series = {LNCS~7795},
    pages = {594-609},
    year = {2013},
    isbn = {978-3-642-36741-0},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2013-TACAS.Second_Competition_on_Software_Verification.pdf},
    url = {http://sv-comp.sosy-lab.org/},
    abstract = { This report describes the 2nd International Competition on Software Verification (SV-COMP 2013), which is the second edition of this thorough evaluation of fully automatic verifiers for software programs. The reported results represent the 2012 state-of-the-art in automatic software verification, in terms of effectiveness and efficiency. The benchmark set of verification tasks consists of eleven categories containing a total of 2315 programs, written in C, and exposing features of integers, heap-data structures, bit-vector operations, and concurrency; the properties include reachability and memory safety. The competition is again organized as a satellite event of TACAS. },
    
    }
    

  4. Dirk Beyer, Andreas Holzer, Michael Tautschnig, and Helmut Veith. Information Reuse for Multi-goal Reachability Analyses. In M. Felleisen and P. Gardner, editors, Proceedings of the 22nd European Symposium on Programming (ESOP 2013, Rome, Italy, March 19-22), LNCS 7792, pages 472-491, 2013. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    It is known that model checkers can generate test inputs as witnesses for reachability specifications (or, equivalently, as counterexamples for safety properties). While this use of model checkers for testing yields a theoretically sound test-generation procedure, it scales poorly for computing complex test suites for large sets of test goals, because each test goal requires an expensive run of the model checker. We represent test goals as automata and exploit relations between automata in order to reuse existing reachability information for the analysis of subsequent test goals. Exploiting the sharing of sub-automata in a series of reachability queries, we achieve considerable performance improvements over the standard approach. We show the practical use of our multi-goal reachability analysis in a predicate-abstraction-based test-input generator for the test-specification language FQL.

    @InProceedings{ESOP13,
    author = {Dirk Beyer and Andreas Holzer and Michael Tautschnig and Helmut Veith},
    title = {Information Reuse for Multi-goal Reachability Analyses},
    booktitle = {Proceedings of the 22nd European Symposium on Programming (ESOP~2013, Rome, Italy, March 19-22)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {M.~Felleisen and P.~Gardner},
    series = {LNCS~7792},
    pages = {472-491},
    year = {2013},
    isbn = {978-3-642-37035-9},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2013-ESOP.Information_Reuse_for_Multi-goal_Reachability_Analyses.pdf},
    url = {},
    abstract = { It is known that model checkers can generate test inputs as witnesses for reachability specifications (or, equivalently, as counterexamples for safety properties). While this use of model checkers for testing yields a theoretically sound test-generation procedure, it scales poorly for computing complex test suites for large sets of test goals, because each test goal requires an expensive run of the model checker. We represent test goals as automata and exploit relations between automata in order to reuse existing reachability information for the analysis of subsequent test goals. Exploiting the sharing of sub-automata in a series of reachability queries, we achieve considerable performance improvements over the standard approach. We show the practical use of our multi-goal reachability analysis in a predicate-abstraction-based test-input generator for the test-specification language FQL. },
    
    }
    

  5. Dirk Beyer and Stefan Löwe. Explicit-State Software Model Checking Based on CEGAR and Interpolation. In V. Cortellessa and D. Varro, editors, Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE 2013, Rome, Italy, March 20-22), LNCS 7793, pages 146-162, 2013. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Abstraction, counterexample-guided refinement, and interpolation are techniques that are essential to the success of predicate-based program analysis. These techniques have not yet been applied together to explicit-value program analysis. We present an approach that integrates abstraction and interpolation-based refinement into an explicit-value analysis, i.e., a program analysis that tracks explicit values for a specified set of variables (the precision). The algorithm uses an abstract reachability graph as central data structure and a path-sensitive dynamic approach for precision adjustment. We evaluate our algorithm on the benchmark set of the Competition on Software Verification 2012 (SV-COMP'12) to show that our new approach is highly competitive. We also show that combining our new approach with an auxiliary predicate analysis scores significantly higher than the SV-COMP'12 winner.

    @InProceedings{FASE13,
    author = {Dirk Beyer and Stefan L{\"o}we},
    title = {Explicit-State Software Model Checking Based on {CEGAR} and Interpolation},
    booktitle = {Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE~2013, Rome, Italy, March 20-22)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {V.~Cortellessa and D.~Varro},
    series = {LNCS~7793},
    pages = {146-162},
    year = {2013},
    isbn = {978-3-642-37056-4},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2013-FASE.Explicit-State_Software_Model_Checking_Based_on_CEGAR_and_Interpolation.pdf},
    url = {},
    abstract = { Abstraction, counterexample-guided refinement, and interpolation are techniques that are essential to the success of predicate-based program analysis. These techniques have not yet been applied together to explicit-value program analysis. We present an approach that integrates abstraction and interpolation-based refinement into an explicit-value analysis, i.e., a program analysis that tracks explicit values for a specified set of variables (the precision). The algorithm uses an abstract reachability graph as central data structure and a path-sensitive dynamic approach for precision adjustment. We evaluate our algorithm on the benchmark set of the Competition on Software Verification 2012 (SV-COMP'12) to show that our new approach is highly competitive. We also show that combining our new approach with an auxiliary predicate analysis scores significantly higher than the SV-COMP'12 winner. },
    
    }
    

  6. Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, and Philipp Wendler. Precision Reuse for Efficient Regression Verification. In B. Meyer, L. Baresi, and M. Mezini, editors, Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2013, St. Petersburg, Russia, August 18-26), pages 389-399, 2013. ACM. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions.

    @InProceedings{FSE13,
    author = {Dirk Beyer and Stefan L{\"o}we and Evgeny Novikov and Andreas Stahlbauer and Philipp Wendler},
    title = {Precision Reuse for Efficient Regression Verification},
    booktitle = {Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on Foundations of Software Engineering (ESEC/FSE 2013, St. Petersburg, Russia, August 18-26)},
    publisher = {ACM},
    editor = {B.~Meyer and L.~Baresi and M.~Mezini},
    pages = {389-399},
    year = {2013},
    isbn = {},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2013-FSE.Precision_Reuse_for_Efficient_Regression_Verification.pdf},
    url = {},
    doi = {10.1145/2491411.2491429},
    abstract = { Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions. },
    
    }
    

  7. Dirk Beyer and Andreas Stahlbauer. BDD-Based Software Model Checking with CPAchecker. In A. Kucera et al., editor, Proceedings of the Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2012, Znojmo, Czech Republic, October 26-28), LNCS 7721, pages 1-11, 2013. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    @InProceedings{MEMICS12,
    author = {Dirk Beyer and Andreas Stahlbauer},
    title = {{BDD}-Based Software Model Checking with {{\sc CPAchecker}}},
    booktitle = {Proceedings of the Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS~2012, Znojmo, Czech Republic, October 26-28)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {A.~Kucera~et~al.},
    series = {LNCS~7721},
    pages = {1-11},
    year = {2013},
    isbn = {978-3-642-36044-2},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2013-MEMICS.BDD-Based_Software_Model_Checking_with_CPAchecker.pdf},
    url = {},
    
    }
    

  8. Dirk Beyer and Philipp Wendler. Reuse of Verification Results: Conditional Model Checking, Precision Reuse, and Verification Witnesses. In E. Bartocci and C. R. Ramakrishnan, editors, Proceedings of the 2013 International Symposium on Model Checking of Software (SPIN 2013, Stony Brook, NY, USA, July 8-9), LNCS 7976, pages 1-17, 2013. Springer-Verlag, Heidelberg. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Verification is a complex algorithmic task, requiring large amounts of computing resources. One approach to reduce the resource consumption is to reuse information from previous verification runs. This paper gives an overview of three techniques for such information reuse. Conditional model checking outputs a condition that describes the state space that was successfully verified, and accepts as input a condition that instructs the model checker which parts of the system should be verified; thus, later verification runs can use the output condition of previous runs in order to not verify again parts of the state space that were already verified. Precision reuse is a technique to use intermediate results from previous verification runs to accelerate further verification runs of the system; information about the level of abstraction in the abstract model can be reused in later verification runs. Typical model checkers provide an error path through the system as witness for having proved that a system violates a property, and a few model checkers provide some kind of proof certificate as a witness for the correctness of the system; these witnesses should be such that the verifiers can read them and ---with less computational effort--- (re-) verify that the witness is valid.

    @InProceedings{SPIN13,
    author = {Dirk Beyer and Philipp Wendler},
    title = {Reuse of Verification Results: Conditional Model Checking, Precision Reuse, and Verification Witnesses},
    booktitle = {Proceedings of the 2013 International Symposium on Model Checking of Software (SPIN~2013, Stony Brook, NY, USA, July 8-9)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {E.~Bartocci and C.~R.~Ramakrishnan},
    series = {LNCS~7976},
    pages = {1-17},
    year = {2013},
    isbn = {},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2013-SPIN.Reuse_of_Verification_Results.pdf},
    url = {http://sv-comp.sosy-lab.org/},
    doi = {10.1007/978-3-642-39176-7_1},
    abstract = { Verification is a complex algorithmic task, requiring large amounts of computing resources. One approach to reduce the resource consumption is to reuse information from previous verification runs. This paper gives an overview of three techniques for such information reuse. Conditional model checking outputs a condition that describes the state space that was successfully verified, and accepts as input a condition that instructs the model checker which parts of the system should be verified; thus, later verification runs can use the output condition of previous runs in order to not verify again parts of the state space that were already verified. Precision reuse is a technique to use intermediate results from previous verification runs to accelerate further verification runs of the system; information about the level of abstraction in the abstract model can be reused in later verification runs. Typical model checkers provide an error path through the system as witness for having proved that a system violates a property, and a few model checkers provide some kind of proof certificate as a witness for the correctness of the system; these witnesses should be such that the verifiers can read them and ---with less computational effort--- (re-) verify that the witness is valid. },
    
    }
    

  9. S. Löwe. CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation (Competition Contribution). In N. Piterman and S. Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2013, Rome, Italy, March 16-24), LNCS 7795, pages 610-612, 2013. Springer. [ Info ] Keyword(s): Software Model Checking.
    @inproceedings{CPACHECKEREXPLICIT-COMP13,
    author = {S.~L{\"{o}}we},
    title = {{{\sc CPAchecker}} with Explicit-Value Analysis Based on {CEGAR} and Interpolation (Competition Contribution)},
    booktitle = {Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS~2013, Rome, Italy, March 16-24)},
    editor = {N.~Piterman and S.~Smolka},
    series = {LNCS~7795},
    year = {2013},
    pages = {610-612},
    publisher = {Springer},
    keyword = {Software Model Checking},
    isbn = {978-3-642-36741-0},
    url = {https://doi.org/10.1007/978-3-642-36742-7_44},
    doi = {10.1007/978-3-642-36742-7_44},
    
    }
    

  10. P. Wendler. CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution). In N. Piterman and S. Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2013, Rome, Italy, March 16-24), LNCS 7795, pages 613-615, 2013. Springer-Verlag, Heidelberg. [ Info ] Keyword(s): Software Model Checking.
    @inproceedings{CPACHECKERSEQCOM-COMP13,
    author = {P.~Wendler},
    title = {{{\sc CPAchecker}} with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution)},
    booktitle = {Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS~2013, Rome, Italy, March 16-24)},
    editor = {N.~Piterman and S.~Smolka},
    series = {LNCS~7795},
    year = {2013},
    pages = {613-615},
    publisher = {Springer-Verlag, Heidelberg},
    keyword = {Software Model Checking},
    isbn = {978-3-642-36741-0},
    url = {https://doi.org/10.1007/978-3-642-36742-7_45},
    doi = {10.1007/978-3-642-36742-7_45},
    
    }
    

Internal reports

  1. Sven Apel, Dirk Beyer, Karlheinz Friedberger, Franco Raimondi, and Alexander von Rhein. Domain Types: Selecting Abstractions Based on Variable Usage. Technical report MIP-1303, Department of Computer Science and Mathematics (FIM), University of Passau (PA), May 2013. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    The success of software model checking depends on finding an appropriate abstraction of the subject program. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types, such as int or long, in order to guide the selection of an appropriate abstract domain for a model checker. Our implementation determines the domain type for each variable in a pre-processing step, based on the variable usage in the program, and then assigns each variable to an abstract domain. The model-checking framework that we use supports to specify a separate analysis precision for each abstract domain, such that we can freely configure the analysis. We experimentally demonstrate a significant impact of the choice of the abstract domain per variable. We consider one explicit (hash tables for integer values) and one symbolic (binary decision diagrams) domain. The experiments are based on standard verification tasks that are taken from recent competitions on software verification. Each abstract domain has unique advantages in representing the state space of variables of a certain domain type. Our experiments show that software model checkers can be improved with a domain-type guided combination of abstract domains.
    Annotation:
    Online: http://arxiv.org/abs/1305.6640

    @TechReport{TR1303-PA13,
    author = {Sven Apel and Dirk Beyer and Karlheinz Friedberger and Franco Raimondi and Alexander von Rhein},
    title = {Domain Types: Selecting Abstractions Based on Variable Usage},
    institution ={Department of Computer Science and Mathematics (FIM), University of Passau (PA)},
    number = {MIP-1303},
    month = {May},
    year = {2013},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2013-PA-TR1303.Domain_Types_Selecting_Abstractions_Based_on_Variable_Usage.pdf},
    url = {},
    abstract = { The success of software model checking depends on finding an appropriate abstraction of the subject program. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types, such as int or long, in order to guide the selection of an appropriate abstract domain for a model checker. Our implementation determines the domain type for each variable in a pre-processing step, based on the variable usage in the program, and then assigns each variable to an abstract domain. The model-checking framework that we use supports to specify a separate analysis precision for each abstract domain, such that we can freely configure the analysis. We experimentally demonstrate a significant impact of the choice of the abstract domain per variable. We consider one explicit (hash tables for integer values) and one symbolic (binary decision diagrams) domain. The experiments are based on standard verification tasks that are taken from recent competitions on software verification. Each abstract domain has unique advantages in representing the state space of variables of a certain domain type. Our experiments show that software model checkers can be improved with a domain-type guided combination of abstract domains. },
    annote = {Online:  http://arxiv.org/abs/1305.6640 
    }, }

  2. Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, and Philipp Wendler. Reusing Precisions for Efficient Regression Verification. Technical report MIP-1302, Department of Computer Science and Mathematics (FIM), University of Passau (PA), May 2013. [ PDF ] Keyword(s): Software Model Checking.
    Abstract:
    Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems, namely, 59 device drivers with 1119 revisions from the Linux kernel.
    Annotation:
    Online: http://arxiv.org/abs/1305.6915

    @TechReport{TR1302-PA13,
    author = {Dirk Beyer and Stefan L{\"o}we and Evgeny Novikov and Andreas Stahlbauer and Philipp Wendler},
    title = {Reusing Precisions for Efficient Regression Verification},
    institution ={Department of Computer Science and Mathematics (FIM), University of Passau (PA)},
    number = {MIP-1302},
    month = {May},
    year = {2013},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2013-PA-TR1302.Reusing_Precisions_for_Efficient_Regression_Verification.pdf},
    url = {},
    abstract = { Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems, namely, 59 device drivers with 1119 revisions from the Linux kernel. },
    annote = {Online:  http://arxiv.org/abs/1305.6915 
    }, }

Theses (PhD, MSc, BSc, Project)

  1. Matthias Dangl. Light-Weight Invariant Generation for Software Verification with CPAchecker. Master's Thesis, University of Passau, Software Systems Lab, 2013. [ PDF ]
    @misc{MatthiasInvariantGeneration,
    author = {Matthias Dangl},
    title = {Light-Weight Invariant Generation for Software Verification with {{\sc CPAchecker}}},
    howpublished = {Master's Thesis, University of Passau, Software Systems Lab},
    year = {2013},
    pdf = {https://www.sosy-lab.org/research/msc/2015.Dangl.Light-Weight_Invariant_Generation_for_Software_Verification_with_CPAchecker.pdf},
    
    }
    

  2. Matthias Dittrich. Bit-Precise Predicate Analysis with CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2013.
    @misc{DittrichBitprecisePredicate,
    author = {Matthias Dittrich},
    title = {Bit-Precise Predicate Analysis with {{\sc CPAchecker}}},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2013},
    field = {Computer Science},
    
    }
    




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