Title :
Automatic formal verification of software: Fundamental concepts
Author_Institution :
Dept. of Comput. Sci., Univ. of British Columbia, Vancouver, BC, Canada
Abstract :
Formal verification of software is undergoing a renaissance, as highly successful, automatic formal techniques developed for hardware verification are combining with classical software analysis techniques to produce practical, useful tools that scale to large, complicated software. This paper briefly introduces the fundamental concepts behind this renaissance.
Keywords :
formal verification; systems analysis; hardware verification; software analysis techniques; software automatic formal verification; Computer science; Counting circuits; Formal verification; Hardware; Logic; Software systems; Software testing; Software tools; Very large scale integration; Vocabulary;
Conference_Titel :
Communications, Circuits and Systems, 2009. ICCCAS 2009. International Conference on
Conference_Location :
Milpitas, CA
Print_ISBN :
978-1-4244-4886-9
Electronic_ISBN :
978-1-4244-4888-3
DOI :
10.1109/ICCCAS.2009.5250313