Model checking C programs using F-SOFT

Franjo Ivančić, Ilya Shlyakhter, Aarti Gupta, Malay K. Ganai, Vineet Kahlon, Chao Wang, Zijiang Yang

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

60 Scopus citations

Abstract

With the success of formal verification techniques like equivalence checking and model checking for hardware designs, there has been growing interest in applying such techniques for formal analysis and automatic verification of software programs. This paper provides a brief tutorial on model checking of c programs. The essential approach is to model the semantics of c programs in the form of finite state systems by using suitable abstractions. The use of abstractions is key, both for modeling programs as finite state systems and for reducing the model sizes in order to manage verification complexity. We provide illustrative details of a verification platform called F-SOFT, which provides a range of abstractions for modeling software, and uses customized SAT-based and BDD-based model checking techniques targeted for software.

Original languageEnglish (US)
Title of host publicationProceedings - 2005 IEEE International Conference on Computer Design
Subtitle of host publicationVLSI in Computers and Processors, ICCD 2005
Pages297-308
Number of pages12
DOIs
StatePublished - Dec 1 2005
Externally publishedYes
Event2005 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 2005 - San Jose, CA, United States
Duration: Oct 2 2005Oct 5 2005

Publication series

NameProceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors
Volume2005
ISSN (Print)1063-6404

Other

Other2005 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 2005
CountryUnited States
CitySan Jose, CA
Period10/2/0510/5/05

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Model checking C programs using F-SOFT'. Together they form a unique fingerprint.

  • Cite this

    Ivančić, F., Shlyakhter, I., Gupta, A., Ganai, M. K., Kahlon, V., Wang, C., & Yang, Z. (2005). Model checking C programs using F-SOFT. In Proceedings - 2005 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 2005 (pp. 297-308). [1524168] (Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors; Vol. 2005). https://doi.org/10.1109/ICCD.2005.77