LinuxQuestions.org
Help answer threads with 0 replies.
Go Back   LinuxQuestions.org > Forums > Linux Forums > Linux - Software > Linux - Kernel
User Name
Password
Linux - Kernel This forum is for all discussion relating to the Linux kernel.

Notices


Reply
  Search this Thread
Old 06-15-2014, 08:03 AM   #1
ahmadnouralizadeh
LQ Newbie
 
Registered: Dec 2013
Posts: 15

Rep: Reputation: Disabled
SMT Solver in Linux Kernel


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!
 
Old 06-22-2014, 09:08 AM   #2
sundialsvcs
LQ Guru
 
Registered: Feb 2004
Location: SE Tennessee, USA
Distribution: Gentoo, LFS
Posts: 8,606
Blog Entries: 4

Rep: Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996
... in ... the kernel?!
 
Old 06-23-2014, 09:17 AM   #3
ahmadnouralizadeh
LQ Newbie
 
Registered: Dec 2013
Posts: 15

Original Poster
Rep: Reputation: Disabled
Yes.
I want to solve constraints for conditionals while the kernel is running. So a constraint solver should be called during kernel execution.
 
Old 06-23-2014, 01:22 PM   #4
sundialsvcs
LQ Guru
 
Registered: Feb 2004
Location: SE Tennessee, USA
Distribution: Gentoo, LFS
Posts: 8,606
Blog Entries: 4

Rep: Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996Reputation: 2996
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.
 
Old 06-24-2014, 05:33 AM   #5
ahmadnouralizadeh
LQ Newbie
 
Registered: Dec 2013
Posts: 15

Original Poster
Rep: Reputation: Disabled
So how is it possible to apply symbolic execution on kernel code?
 
  


Reply

Tags
linux, testing


Thread Tools Search this Thread
Search this Thread:

Advanced Search

Posting Rules
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts

BB code is On
Smilies are On
[IMG] code is Off
HTML code is Off



Similar Threads
Thread Thread Starter Forum Replies Last Post
What does solver support linux OS means? hitmen General 1 09-12-2011 12:30 PM
LXer: Electromagnetic Field Solver Suite Tools on Linux LXer Syndicated Linux News 0 10-31-2007 02:40 AM
2.6.4 + which patch + smt?? thehundredthone Linux - Software 0 03-17-2004 02:33 PM

LinuxQuestions.org > Forums > Linux Forums > Linux - Software > Linux - Kernel

All times are GMT -5. The time now is 10:38 PM.

Main Menu
Advertisement
My LQ
Write for LQ
LinuxQuestions.org is looking for people interested in writing Editorials, Articles, Reviews, and more. If you'd like to contribute content, let us know.
Main Menu
Syndicate
RSS1  Latest Threads
RSS1  LQ News
Twitter: @linuxquestions
Facebook: linuxquestions Google+: linuxquestions
Open Source Consulting | Domain Registration