Solving Constrained Horn Clauses (CHC) is necessitated by numerous fields in formal methods, from verifying software and smart contracts to modeling systems, yet the competitive scene for academic tools remains fairly sparse, especially compared to more popular fields such as software verification. Comparative evaluation as a competition, such as SV-COMP or CHC-COMP, sparks a more cohesive community around fields in formal methods. Lately, a trend has been emerging with tools such as Btor2C that bridge multiple fields together, thus widening this cohesion. Following that example, we propose and perform an experiment, where we use CHC-to-C transformation to apply software verification tools to linear CHC problems. In the process, we help both fields by diversifying the scene of CHC solvers and providing new and valuable benchmarks to aid the development of software verification tools. Using these benchmarks, we uncovered a previously hidden bug in multiple verification tools that can lead to false positive results. By analysing the results of the experiment, we can confidently make a recommendation for developers of software verifiers to consider supporting CHCs via our pre-verification transformation.

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

Solving Constrained Horn Clauses as C Programs with CHC2C

  • Levente Bajczi,
  • Vince Molnár

摘要

Solving Constrained Horn Clauses (CHC) is necessitated by numerous fields in formal methods, from verifying software and smart contracts to modeling systems, yet the competitive scene for academic tools remains fairly sparse, especially compared to more popular fields such as software verification. Comparative evaluation as a competition, such as SV-COMP or CHC-COMP, sparks a more cohesive community around fields in formal methods. Lately, a trend has been emerging with tools such as Btor2C that bridge multiple fields together, thus widening this cohesion. Following that example, we propose and perform an experiment, where we use CHC-to-C transformation to apply software verification tools to linear CHC problems. In the process, we help both fields by diversifying the scene of CHC solvers and providing new and valuable benchmarks to aid the development of software verification tools. Using these benchmarks, we uncovered a previously hidden bug in multiple verification tools that can lead to false positive results. By analysing the results of the experiment, we can confidently make a recommendation for developers of software verifiers to consider supporting CHCs via our pre-verification transformation.