Abstract
Formal verification techniques are not yet widely used in the software industry, perhaps because software tends to be more complex than hardware, and the penalty for bugs is often lower (software can be patched after the release). Instead, a large amount of time and money is being spent on software testing, which misses many subtle errors, especially in concurrent programs. Increased use of concurrency, e.g., due to the popularity of web services, and the surge of complex viruses which exploit security vulnerabilities of software, make the problem of creating a verifying compiler for production-quality code essential and urgent.
Chapter PDF
Similar content being viewed by others
References
Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)
Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: “Theorem Proving for Predicate Abstraction Refinement”. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, Springer, Heidelberg (2004)
Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)
Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001)
Ball, T., Rajamani, S.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)
Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: “Multi-Valued Symbolic Model-Checking”. ACM Transactions on Software Engineering and Methodology 12(4), 1–38 (2003)
Chechik, M., Devereux, B., Gurfinkel, A.: χChek: A Multi-Valued Model-Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 505–509. Springer, Heidelberg (2002)
Cook, B., Podelski, A., Rybalchenko, A.: Abstraction Refinement for Termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 87–101. Springer, Heidelberg (2005)
Dechter, R.: Constraint Processing. Morgan Kaufmann, San Francisco (2003)
Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM Transactions on Programming Languages and Systems 2(19), 253–291 (1997)
Elrad, T., Filman, R., Bader, A.: Aspect-Oriented Programming: Introduction. Communications of the ACM, pp. 29–32 (October 2001)
Gurfinkel, A., Chechik, M.: Proof-like Counterexamples. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 160–175. Springer, Heidelberg (2003)
Gurfinkel, A., Chechik, M.: Why Waste a Perfectly Good Abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 212–226. Springer, Heidelberg (2006)
Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Gurfinkel, A., Wei, O., Chechik, M.: Systematic Construction of Abstractions for Model-Checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 381–397. Springer, Heidelberg (2005)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from Proofs. In: Proceedings of 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), Venice, Italy, January 2004, pp. 232–244. ACM Press, New York (2004)
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proceedings of 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002), Portland, Oregon, January 2002, pp. 58–70. ACM Press, New York (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.: Extreme Model Checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 332–358. Springer, Heidelberg (2004)
Kroening, D., Groce, A., Clarke, E.: Counterexample Guided Abstraction Refinement via Program Execution. In: Proceedings of International Conference on Formal Engineering Methods, November 2004, pp. 224–238 (2004)
Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: Proceedings of 3rd Annual Symposium on Logic in Computer Science (LICS 1988), pp. 203–210. IEEE Computer Society Press, Los Alamitos (1988)
Reps, T.W., Sagiv, M., Wilhelm, R.: Static Program Analysis via 3-Valued Logic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 15–30. Springer, Heidelberg (2004)
Uchitel, S., Chechik, M.: Merging Partial Behavioural Models. In: Proceedings of 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering, November 2004, pp. 43–52 (2004)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. Journal of Automated Software Engineering 10(2) (April 2003)
Wei, O., Gurfinkel, A., Chechik, M.: Identification and Counter Abstraction for Full Virtual Symmetry. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 285–300. Springer, Heidelberg (2005)
Whittle, J., Schumann, J.: Generating Statechart Designs from Scenarios. In: Proceedings of 22nd International Conference on Software Engineering (ICSE 2000), May 2000, pp. 314–323. ACM Press, New York (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Chechik, M., Gurfinkel, A. (2008). Model-Checking Software Using Precise Abstractions. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_37
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)