SymDiff: A language-agnostic semantic diff tool for imperative programs. In this paper, we describe SymDiff, a language-agnostic tool for equivalence checking and displaying semantic (behavioral) differences over imperative programs. The tool operates on an intermediate verification language Boogie, for which translations exist from various source languages such as C, C# and x86. We discuss the tool and the front-end interface to target various source languages. Finally, we provide a brief description of the front-end for C programs.
Keywords for this software
References in zbMATH (referenced in 11 articles )
Showing results 1 to 11 of 11.
- He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
- D’Argenio, Pedro R.; Barthe, Gilles; Biewer, Sebastian; Finkbeiner, Bernd; Hermanns, Holger: Is your software on dope? Formal analysis of surreptitiously “enhanced” programs (2017)
- Fuhs, Carsten; Kop, Cynthia; Nishida, Naoki: Verifying procedural programs via constrained rewriting induction (2017)
- Wood, Tim; Drossopolou, Sophia; Lahiri, Shuvendu K.; Eisenbach, Susan: Modular verification of procedure equivalence in the presence of memory allocation (2017)
- Barthe, Gilles; Crespo, Juan Manuel; Kunz, César: Product programs and relational program logics (2016)
- Ciob^acă, Ştefan; Lucanu, Dorel; Rusu, Vlad; Roşu, Grigore: A language-independent proof system for full program equivalence (2016)
- Lucanu, Dorel; Rusu, Vlad: Program equivalence by circular reasoning (2015)
- Fedyukovich, Grigory; Sery, Ondrej; Sharygina, Natasha: Evolcheck: incremental upgrade checker for C (2013)
- Hawblitzel, Chris; Kawaguchi, Ming; Lahiri, Shuvendu K.; Reb^elo, Henrique: Towards modularly comparing programs using automated theorem provers (2013)
- Bjørner, Nikolaj: Taking satisfiability to the next level with Z3 (abstract) (2012)
- Lahiri, Shuvendu K.; Hawblitzel, Chris; Kawaguchi, Ming; Reb^elo, Henrique: SYMDIFF: a language-agnostic semantic diff tool for imperative programs (2012) ioport