We present Nacpa, a meta-verifier based on parallel portfolio and native compilation of backend verifiers. Nacpa does not implement any software analyses itself, but uses the Java-based CPAchecker as off-the-shelf verification backend in different configurations; each called as a separate, external process. To avoid the overhead of starting the Java Virtual Machine multiple times and to improve the run time on fast-to-solve tasks, we created a natively compiled version of CPAchecker for Nacpa. Nacpa is a conceptually simple framework, yet proves to be competitive in SV-COMP  2025.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Nacpa: Native Checking with Parallel-Portfolio Analyses

  • Thomas Lemberger,
  • Henrik Wachowitz

摘要

We present Nacpa, a meta-verifier based on parallel portfolio and native compilation of backend verifiers. Nacpa does not implement any software analyses itself, but uses the Java-based CPAchecker as off-the-shelf verification backend in different configurations; each called as a separate, external process. To avoid the overhead of starting the Java Virtual Machine multiple times and to improve the run time on fast-to-solve tasks, we created a natively compiled version of CPAchecker for Nacpa. Nacpa is a conceptually simple framework, yet proves to be competitive in SV-COMP  2025.