Symbolic execution based on language transformation

We propose a language-independent symbolic execution  framework for languages endowed with a formal operational semantics based on term rewriting. Starting from a given definition of a language, a new language definition is generated,with the same syntax as the original one, but whose semantical rules are transformed in order to rewrite overlogical formulas denoting possibly infinite sets of program states. Then,the symbolic execution of concrete programs is,by definition, the execution of the same programs with the symbolic semantics. Weprovethatthesymbolicexecutionthusdefinedhasthe properties naturallyexpectedfromit(withrespecttoconcreteprogramexecution). A prototypeimplementationofourapproachwasdevelopedinthe K framework. We demonstratethetool’sgenericitybyinstantiatingitonseverallanguages,andillustrateit on thereachabilityanalysisandmodelcheckingofseveralprograms. 

Sidebar