A visual studio plug-in for CProver

Mohamed Nassim Seghir, Daniel Kroening

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In recent years, automatic software verification has emerged as a complementary approach to program testing for enhancing software quality. Finding bugs is the ultimate aim of software verification tools. How do we best support the programmer who has to diagnose and understand those bugs? Unfortunately, most of the existing tools do not offer enough support for error diagnosis. We have developed a plug-in which implements a graphical user interface for the CProver tools within the Visual Studio IDE. Our plug-in enables visual debugging and error trace simulating within C programs as well as co-debugging C programs in tandem with wave-form views of hardware designs. Another feature of our plug-in is background verification. Each time a program source is saved, the verification process is silently triggered in background. If an error is found, its location is highlighted in the program. The user interacts directly with the program source to obtain information about the error.
Original languageEnglish
Title of host publicationDeveloping Tools as Plug-ins (TOPI), 2013 3rd International Workshop on
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages43-48
Number of pages6
DOIs
Publication statusPublished - 2013

Fingerprint

Dive into the research topics of 'A visual studio plug-in for CProver'. Together they form a unique fingerprint.

Cite this