Releasing the PSYCO: Using Symbolic Search in Interface Generation for Java

Share

Malte Mues, Falk Howar, Kasper Luckow, Temesghen Kahsai, Zvonimir Rakamaric. Java Pathfinder Workshop (JPF 2016), Seattle, WA, USA.
[pdf] [bib]

Abstract: The Java PathFinder extension PSYCO generates interfaces of Java components using a combination of dynamic symbolic execution and automata learning to explore different combinations of method invocations on a component. Such interfaces are useful in contract-based compositional verification of component-based systems. PSYCO relies on testing for validating learned interfaces and currently cannot guarantee that a generated interface is correct. Instead, it simply returns the most recent learned interface once a user-defined time limit is exceeded. In this paper, we report on work that was performed during the 2016 Google Summer of Code. The aim of this work is to extend PSYCO with symbolic search. During symbolic search, PSYCO uses fully symbolic method summaries for exploring the state space of a component symbolically. We plan to eventually use symbolic search to compute a termination criterion for PSYCO that guarantees the correctness of learned interfaces (e.g., by using symbolic search as a basis for symbolically model-checking a component against a learned interface).

Bibtex:

@article{jpf2016-mhlkr,
  author = {Malte Mues and Falk Howar and Kasper Luckow and
    Temesghen Kahsai and Zvonimir Rakamari\'c},
  title = {Releasing the {PSYCO}: Using Symbolic Search in
    Interface Generation for {Java}},
  journal = {ACM SIGSOFT Software Engineering Notes},
  volume = {41},
  number = {6},
  year = {2016},
  month = {November},
  pages = {1--5},
  publisher = {ACM},
  note = {Proceedings of the 2016 Java Pathfinder Workshop (JPF)},
}