Abstract
With the growing maturity in hardware verification methods, there has been great interest in applying them to verification of software programs. Aside from issues of scale and complexity, there are many differences between the two domains in the underlying problem of searching for bugs. In this talk, I will describe our experiences with this transition, with emphasis on methods that worked and those that did not.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (2001)
Clarke, E.M., et al.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: IEEE International Conference on Computer-Aided Design (2006)
Ganai, M.K., Gupta, A., Ashar, P.: DiVer. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 575–580. Springer, Heidelberg (2005)
Ivančić, F., Shlyakhter, I., Gupta, A., Ganai, M.K., Kahlon, V., Wang, C., Yang, Z.: Model checking c programs using f-soft. In: IEEE International Conference on Computer Design (2005)
Ivančić, F., et al.: F-Soft. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 301–306. Springer, Heidelberg (2005)
Kurshan, R.P.: Computer-aided Verification of Coordinating Processes: the Automata-theoretic Approach. Princeton University Press, Princeton (1995)
Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. STTT 7(2), 156–173 (2005)
Sankaranarayanan, S., et al.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 3–17. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gupta, A. (2008). From Hardware Verification to Software Verification: Re-use and Re-learn. In: Yorav, K. (eds) Hardware and Software: Verification and Testing. HVC 2007. Lecture Notes in Computer Science, vol 4899. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77966-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-77966-7_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77964-3
Online ISBN: 978-3-540-77966-7
eBook Packages: Computer ScienceComputer Science (R0)