Model checking C programs using F-SOFT

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

doi:10.1109/ICCD.2005.77

Model checking C programs using F-SOFT

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

70 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 language	English (US)
Title of host publication	Proceedings - 2005 IEEE International Conference on Computer Design
Subtitle of host publication	VLSI in Computers and Processors, ICCD 2005
Pages	297-308
Number of pages	12
DOIs	https://doi.org/10.1109/ICCD.2005.77
State	Published - 2005
Event	2005 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 2005 - San Jose, CA, United States Duration: Oct 2 2005 → Oct 5 2005

Publication series

Name	Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors
Volume	2005
ISSN (Print)	1063-6404

Other

Other	2005 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 2005
Country/Territory	United States
City	San Jose, CA
Period	10/2/05 → 10/5/05

All Science Journal Classification (ASJC) codes

Hardware and Architecture
Electrical and Electronic Engineering

Access to Document

10.1109/ICCD.2005.77

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). Article 1524168 (Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors; Vol. 2005). https://doi.org/10.1109/ICCD.2005.77

@inproceedings{6dd586dc2fbb4780987d4f70f297f505,

title = "Model checking C programs using F-SOFT",

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.",

author = "Franjo Ivan{\v c}i{\'c} and Ilya Shlyakhter and Aarti Gupta and Ganai, {Malay K.} and Vineet Kahlon and Chao Wang and Zijiang Yang",

year = "2005",

doi = "10.1109/ICCD.2005.77",

language = "English (US)",

isbn = "0769524516",

series = "Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors",

pages = "297--308",

booktitle = "Proceedings - 2005 IEEE International Conference on Computer Design",

note = "2005 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 2005 ; Conference date: 02-10-2005 Through 05-10-2005",

}

Ivančić, F, Shlyakhter, I, Gupta, A, Ganai, MK, 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., 1524168, Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors, vol. 2005, pp. 297-308, 2005 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 2005, San Jose, CA, United States, 10/2/05. https://doi.org/10.1109/ICCD.2005.77

Model checking C programs using F-SOFT. / Ivančić, Franjo; Shlyakhter, Ilya; Gupta, Aarti et al.
Proceedings - 2005 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 2005. 2005. p. 297-308 1524168 (Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors; Vol. 2005).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Model checking C programs using F-SOFT

AU - Ivančić, Franjo

AU - Shlyakhter, Ilya

AU - Gupta, Aarti

AU - Ganai, Malay K.

AU - Kahlon, Vineet

AU - Wang, Chao

AU - Yang, Zijiang

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33745956208&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33745956208&partnerID=8YFLogxK

U2 - 10.1109/ICCD.2005.77

DO - 10.1109/ICCD.2005.77

M3 - Conference contribution

AN - SCOPUS:33745956208

SN - 0769524516

SN - 9780769524511

T3 - Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors

SP - 297

EP - 308

BT - Proceedings - 2005 IEEE International Conference on Computer Design

T2 - 2005 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 2005

Y2 - 2 October 2005 through 5 October 2005

ER -

Ivančić F, Shlyakhter I, Gupta A, Ganai MK, Kahlon V, Wang C et al. Model checking C programs using F-SOFT. In Proceedings - 2005 IEEE International Conference on Computer Design: VLSI in Computers and Processors, ICCD 2005. 2005. p. 297-308. 1524168. (Proceedings - IEEE International Conference on Computer Design: VLSI in Computers and Processors). doi: 10.1109/ICCD.2005.77

Model checking C programs using F-SOFT

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this