rune icon indicating copy to clipboard operation
rune copied to clipboard

Published 20 hours ago • verified publisher icon sushant94

Scalability and radeco IL

Open sushant94 opened this issue 8 years ago • 2 comments

Current implementation of context uses SMTLIB2 directly. This is not scalable on the long run as we do not perform any optimizations on the constraints that are generated before feeding it into the backend SMT solver. This can be fixed by leveraging radeco IL from radeco IL and performing static analysis / optimizations before feeding the constraints to a solver.

As an added part of this task, concrete values must be treated differently from symbolic values. This reduces unnecessary constraints from being generated in the first place.

sushant94 avatar Apr 02 '16 19:04 sushant94

It's better to use http://why3.lri.fr/ Why3 markup language can be converted to SMTLIB2 using special drivers, and then use it with Alt-ergo, CVC3, CVC4, and Z3, etc... https://www.lri.fr/~marche/MPRI-2-36-1/install.html check this. Also, interactive proof assistant (like Coq) can be used http://why3.lri.fr/doc-0.87.3/manual010.html

j123123 avatar Jun 13 '17 15:06 j123123

@j123123 Sorry, was on vacation and took a while to reply. Thanks for that, I'm taking a look at it.

sushant94 avatar Jun 26 '17 23:06 sushant94