Logo des Repositoriums

Auflistung nach Schlagwort "Symbolic Execution"

1 - 4 von 4
  • Konferenzbeitrag
    Badger: Complexity Analysis with Fuzzing and Symbolic Execution
    (Software Engineering and Software Management 2019, 2019) Noller, Yannic; Kersten, Rody; Pasareanu, Corina
    In this work, we report on our recent research results on “Badger: Complexity Analysis with Fuzzing and Symbolic Execution” which was published in the proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis [NKP18]. Badger employs a hybrid software analysis technique that combines fuzzing and symbolic execution for finding performance bottlenecks in software. Our primary goal is to use Badger to discover vulnerabilities which are related to worst-case time or space complexity of an application. To this end, we use a cost-guided fuzzing approach, which produces inputs to increase the code coverage, but also to maximize a resource-related cost function, such as execution time or memory usage. We combine this fuzzing technique with a customized symbolic execution, which is also guided by heuristics that aim to increase the same cost. Experimental evaluation shows that this hybrid approach enables us to use the strengths of both techniques and overcome their individual weaknesses.
  • Zeitschriftenartikel
    Proactive Energy-Aware System Software Design with SEEP
    (Softwaretechnik-Trends: Vol. 33, No. 2, 2013) Hönig, Timo; Eibel, Christopher; Schröder-Preikschat, Wolfgang; Cassens, Björn; Kapitza, Rüdiger
    Timo H¨ onig, Christopher Eibel, and Wolfgang Schr¨ oder-Preikschat Friedrich­Alexander University Erlangen­Nuremberg {thoenig,ceibel,wosch}@cs.fau.de 1 Introduction and Motivation Bj¨ orn Cassens and R¨ udiger Kapitza TU Braunschweig {b.cassens,rkapitza}@tu-bs.de
  • Konferenzbeitrag
    Symbolic Execution for Realizability-Checking of Scenario-based Specifications
    (Software Engineering und Software Management 2018, 2018) Greenyer, Joel; Gutjahr, Timo
    (Extended abstract of: Greenyer, Joel; Gutjahr, Timo: Symbolic Execution for Realizability-Checking of Scenario-Based Specifications. In: 2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS). volume 00, pp. 312–322, Sept. 2017.) Scenario-based specification with the Scenario Modeling Language (SML) is an intuitive approach for formally specifying the behavior of reactive systems. SML is close to how humans conceive and communicate requirements, yet SML is executable and simulation and formal realizability checking can find specification flaws early. The realizability checking complexity is, however, exponential in the number of scenarios and variables. Therefore algorithms relying on explicit-state exploration do not scale and, especially when specifications have message parameters and variables over large domains, fail to unfold their potential. In this paper, we present a technique for the symbolic execution of SML specifications that interprets integer message parameters and variables symbolically. It can be used for symbolic realizability checking and interactive symbolic simulation. We implemented the technique in ScenarioTools. Evaluation shows drastic performance improvements over the explicit-state approach for a range of examples. Moreover, symbolic checking produces more concise counter examples, which eases the comprehension of specification flaws.
  • Textdokument
    A system for SMT based constraint programming in Java
    (INFORMATIK 2017, 2017) Funk, Maurice
    This paper presents a system for constraint programming in Java using translation of JVM bytecode into SMT. This allows the constraints to be written in normal Java, to being interoperable with the rest of the program and lowers the entry barrier to using specialised solvers in applications. Due to the nature of the performed translation, variable assignments for other runtime properties than constraint satisfaction can be found. These include variable assignments that lead to runtime exceptions during normal code execution. We demonstrate that the implemented approach is able to find variable assignments for non-trivial constraints such as a Sudoku puzzle.