sally

sally copied to clipboard

Add sally to our Homebrew Tap

1

Title says it all really.

ianamason

Parse errors

2

It seems sally can only parse examples from `/test/regess/*`. Whenever running the mcmt cases from the `examples` folder, I got the following information: `Parse error: ../../examples/honeywell/Ex3.mcmt:28:20: ` And the sal...

rainoftime

C++ API for sally?

1

Hi, is there any plan for providing C++ api for creating and verifying a transition system?

rainoftime

Integrate crab into Sally

1

I've added some boilerplate to the "ai" branch. Notes: - The code for crab integration should be added to `src/ai/crab/crab.{h.cpp}`. - Any options for the module should be added to...

dddejan

Invariants learned from abstract interpretation should be used in the IC3 engine.

dddejan

Multi-property solving

2

Sally seems to process process queries sequentially. For k-induction, it's often beneficial to attack problems simultaneously so that they can be used to strengthen each other. We can simulate this...

agacek

- memory consumption is starting to show on deep examples. - model usege creates too many value terms, these need to be collected

dddejan

only named files and strings

dddejan

The need for CUDD (presumably [this](https://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddIntro.html)) is not documented. More, CUDD has all-but-disappeared from the internet. Following the build steps yeids: ``` $ cmake .. -- GMP library: /usr/lib/x86_64-linux-gnu/libgmp.so --...

TomMD