[klee-dev] About KLEE

[eric.rizzi at huskers.unl.edu]

Hey Suresh,

I'm not sure that what you are looking for exists. Klee is designed to test programs and create test suites. It will find assertion violations and other common errors. If you're looking to verify that a particular path through the program is semantically correct, however, you're going to have to find some type of specification for each program.   From that point, you could use the inputs/ouputs generated by Klee to make sure they all match the specifications.  As I said, however, I don't know where you will be able to find any formal specifications for core-utils.


The only option I can think of is to use some competing implementation of the core-utils and verify that they each produce the same outputs given the same inputs.


Hope that helps,

Eric Rizzi

________________________________
From: klee-dev-bounces at imperial.ac.uk <klee-dev-bounces at imperial.ac.uk> on behalf of suresh_khatiwada <suresh_khatiwada at yahoo.com>
Sent: Saturday, May 30, 2015 5:43 AM
To: klee-dev at imperial.ac.uk
Subject: [klee-dev] About KLEE


How can we plan to construct oracles while testing Coreutils using KLEE?

Sent on the go with Vodafone
-------------- next part --------------
HTML attachment scrubbed and removed