Support the generation of violation witness in graphML format in SPF
- Mentors
- Yannic Noller, Elena Sherman, Soha Hussein
- Organization
- The JPF team
- Technologies
- android, java, jvm, Distributed System, Java Pathfinder, Symbolic PathFinder
- Topics
- model checking, symbolic execution, program analysis, formal verification
Our final goal of this project is to obtain missing scores for Symbolic PathFinder(SPF) in SV-COMP. There are two main reasons why SPF is losing many points. First, there are too many unconfirmed results. Even though we provided correct results, we’re losing points because these results cannot be verified by witness validators. To address this, we should support generation of violation witness in a format that witness validators can verify. Second, there are incorrect results. To deal with this problem, we will analyze why SPF outputs wrong answers for certain task and repair SPF to work correctly. In addition, we will categorize why SPF outputs some incorrect results.