search

dnWalker-project / dnWalker

1 stars 0 forks source link

Modular symbolic expressions and translation to Z3 #74

Open benjamin-hejl opened 1 year ago

benjamin-hejl commented 1 year ago

Add special expression which would have an identifier (string?) and array of operands. When translating the expression into Z3, a custom translator would generate the Z3 expressions. May be useful for leveraging theories implemented in Z3 - theory of strings, lists, sets...

kfrajtak commented 1 year ago

Rand is handled in model-checking mode, but the execution may be broken and not applicable in concolic execution and test case generation. It works for System.Int32 System.Random::Next(System.Int32) only when all options are explored.

See dnWalker.NativePeers.SystemRandom.