SMT Solver in Linux Kernel

ahmadnouralizadeh · 06-15-2014, 07:03 AM

Is there a way to call an SMT solver such as yices or STP from linux kernel? I want to implement a symbolic execution engine and therefore I need to solve constraints at run time. Thanks in advance!

sundialsvcs · 06-22-2014, 08:08 AM

... in ... the kernel?!

ahmadnouralizadeh · 06-23-2014, 08:17 AM

Yes.

I want to solve constraints for conditionals while the kernel is running. So a constraint solver should be called during kernel execution.

sundialsvcs · 06-23-2014, 12:22 PM

No, it shouldn't.

The kernel must never do "time-consuming things."

Its job is to create the environment in which other software can do such things. But it must never consume much time itself.

ahmadnouralizadeh · 06-24-2014, 04:33 AM

So how is it possible to apply symbolic execution on kernel code?