@all Thanks a lot for your awesome comments and feedback.
Besides compiler, emulator, and hypervisor, there is a symbolic execution engine in selfie that we are working on and would love to get feedback from you. The goal is to teach, eventually, a more formal approach when reasoning about correctness already in undergraduate classes. But the engine is also a research vehicle, especially the bounded model checking part.
Besides compiler, emulator, and hypervisor, there is a symbolic execution engine in selfie that we are working on and would love to get feedback from you. The goal is to teach, eventually, a more formal approach when reasoning about correctness already in undergraduate classes. But the engine is also a research vehicle, especially the bounded model checking part.