[klee-dev] Is it possible to implement compositional symbolic execution in KLEE

[Nazir, Tareq Mohammed]

Hi,


Found below link


https://github.com/tum-i4/macke

[https://opengraph.githubassets.com/8e0dac6e7d018e975a14a12be73f158f99de4c22b0fa610dc0502b0245c3b249/tum-i4/macke]<https://github.com/tum-i4/macke>

GitHub - tum-i4/macke: Modular And Compositional analysis with KLEE Engine<https://github.com/tum-i4/macke>
github.com
Modular And Compositional analysis with KLEE Engine - GitHub - tum-i4/macke: Modular And Compositional analysis with KLEE Engine


Thanks and Best Regards,

Tareq Mohammed Nazir

________________________________
From: hb wang <fighter9010 at gmail.com>
Sent: Monday, 24 October 2022 03:50:40
To: Nazir, Tareq Mohammed
Cc: klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] Is it possible to implement compositional symbolic execution in KLEE

Thank you. I have read the paper you recommended.
I know now that compositional analysis can be achieved in KLEE but the details are not discussed in that paper.
Is there any open source code for this?

Nazir, Tareq Mohammed <Tareq.Nazir at aau.at<mailto:Tareq.Nazir at aau.at>> 于2022年10月23日周日 20:44写道：

Hi,


Please find the below paper is this related to the topic : https://dl.acm.org/doi/abs/10.1145/2970276.2970281

[https://dl.acm.org/cms/asset/53e7485c-29f4-4b88-b12f-3ac86ec74c11/2970276.cover.jpg]<https://dl.acm.org/doi/abs/10.1145/2970276.2970281>

MACKE: compositional analysis of low-level vulnerabilities with symbolic execution | Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering<https://dl.acm.org/doi/abs/10.1145/2970276.2970281>
dl.acm.org<http://dl.acm.org>

Thanks and Best Regards,

Tareq Mohammed Nazir

________________________________
From: klee-dev-bounces at imperial.ac.uk<mailto:klee-dev-bounces at imperial.ac.uk> <klee-dev-bounces at imperial.ac.uk<mailto:klee-dev-bounces at imperial.ac.uk>> on behalf of hb wang <fighter9010 at gmail.com<mailto:fighter9010 at gmail.com>>
Sent: Sunday, 23 October 2022 07:44:43
To: klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
Subject: [klee-dev] Is it possible to implement compositional symbolic execution in KLEE

Hi, I'm currently planning to verify an idea about compositional symbolic execution (CSE).
But CSE is not officially supported by KLEE now as far as I know.
So I am eager to know whether it is possible to implement CSE in KLEE.
If so, please give some suggestions about how to implement that. Thank you very much~

-------------- next part --------------
HTML attachment scrubbed and removed