How SVCOMP benchmark programs are converting to Ocamal programs or to Horn cluases

[ezudheen]

Hi,

I would like to know how you are converting SVCOMP benchmark programs in either C or JAVA to OCamal or Horn Clauses. I understand Hoice can take only Horn Clauses. and r_type can be used for converting OCamal to Horn Clauses.

Thanks Ezudheen

[AdrienChampion]

Hi Ezudheen!

As you said, we convert our OCaml programs to Horn clauses using r_type. However we did not translate the C or Java SV-COMP benchmarks. We use the clauses on https://github.com/sosy-lab/sv-benchmarks (in the clauses directory).

Now if you ask me, I assume going from C to Horn was done with seahorn but I can't say for sure. I don't know about the Java programs though.

Hope that helps!

[ezudheen]

Hi Adrien,

We are planning to compare HOICE with our tool https://arxiv.org/abs/1712.09418 using the latest https://github.com/sosy-lab/sv-benchmarks/tree/master/c/recursive

SVCOMP recursive benchmark suite. Actually our tool performing better on these benchmark compared to the winner on this track https://monteverdi.informatik.uni-freiburg.de/tomcat/Website/?ui=tool&tool=automizer

So we were interested to compare with HOICE also on these benchmarks suites

But the issue is that HOICE need either Ocaml or CHC encoding, and I could not find any tool for converting recursive C programs to CHCs or Ocaml

I had communicated with SeaHorn people, SeaHorn cannot handle recursive programs.

Thanks Ezudheen

On Wed, May 30, 2018 at 6:57 AM, Adrien Champion notifications@github.com wrote:

Hi Ezudheen!

As you said, we convert our OCaml programs to Horn clauses using r_type. However we did not translate the C or Java SV-COMP benchmarks. We use the clauses on https://github.com/sosy-lab/sv-benchmarks (in the clauses directory).

Now if you ask me, I assume going from C to Horn was done with seahorn https://github.com/seahorn/seahorn but I can't say for sure. I don't know about the Java programs though.

Hope that helps!

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hopv/hoice/issues/19#issuecomment-393000669, or mute the thread https://github.com/notifications/unsubscribe-auth/AWCxQjZWhQ5G5ERUWRn0UZ6oWtJX-uPRks5t3fVqgaJpZM4UR-ot .

[AdrienChampion]

I can't really help you, I'm just the developper of hoice... and it only supports Horn clauses in the SMT-LIB 2 format. We separated r_type and hoice exactly to avoid having the kind of problem you're having.

However if you're manipulating Horn clauses in your tool, dumping them in SMT-LIB 2 should be pretty easy. Also, your paper is explicitely about solving Horn clauses: in this context, I think you want to benchmark against z3's Spacer. Meaning you will need to dump your clauses in SMT-LIB 2 or muZ (z3-specific) format. As I discussed already with Daniel, you can go relatively easily from one to the other.

[ezudheen]

Yes your are correct, we can run our tool on available CHC benchmarks

But the primary objective of our tool to handle modular verification (recursive and concurrent programs)

So we were interested to compare Horn-ICE with HIOCE on recursive programs

and here the larger question is how I can run HIOCE on recursive programs?

On Wed, May 30, 2018 at 11:59 AM, Adrien Champion notifications@github.com wrote:

I can't really help you, I'm just the developper of hoice... and it only supports Horn clauses in the SMT-LIB 2 format. We separated r_type and hoice exactly to avoid having the kind of problem you're having.

However if you're manipulating Horn clauses in your tool, dumping them in SMT-LIB 2 should be pretty easy. Also, your paper is explicitely about solving Horn clauses: in this context, I think you want to benchmark against z3's Spacer. Meaning you will need to dump your clauses in SMT-LIB 2 or muZ (z3-specific) format. As I discussed already with Daniel, you can go relatively easily from one to the other.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hopv/hoice/issues/19#issuecomment-393045284, or mute the thread https://github.com/notifications/unsubscribe-auth/AWCxQozFugyiIZKGgSaz4h3pZ6JsBdVKks5t3jw_gaJpZM4UR-ot .

[AdrienChampion]

Assuming you're still talking about C programs, then you can't. Hoice only reads Horn clauses in SMT-LIB 2.

[ezudheen]

OK, I am thinking about manually converting one or two recursive C program to SMT-LIB2

And just have a glimpse of the comparison

On Wed, May 30, 2018 at 12:10 PM, Adrien Champion notifications@github.com wrote:

Assuming you're still talking about C programs, then you can't. Hoice only reads Horn clauses in SMT-LIB 2.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hopv/hoice/issues/19#issuecomment-393047529, or mute the thread https://github.com/notifications/unsubscribe-auth/AWCxQuYuPXQik7-kLuAw6JPrcJIUBgxiks5t3j7XgaJpZM4UR-ot .

[AdrienChampion]

Sure, but it seems to me it would be better to just dump the clauses in SMT-LIB 2 or muZ so that you can compare to hoice easily, and maybe more importantly to z3's spacer which outperforms hoice on a significant number of benchmarks.