The Symbolic Execution Debugger (SED) is a debugging and visualization tool based on KeY’s symbolic execution engine that can be used, just like a standard debugger, without any specialist knowledge. Now, the SED has successfully been applied by Aniket Kulkarni from Tata Consultancy Services in the validation of an industrial software component. He concludes that the “SED tool is useful for applying Symbolic Execution techniques as visual feedback is given to the developer”.
If you are interested in this practical perspective of using formal methods, you can find Aniket’s article on ACM DL. More information on the SED is available in the Symbolic Debugging section on our website.
