Abstract
Catching bugs in programs is difficult and time-consuming. The effort of debugging and proving correct even small units of code can surpass the effort of programming. Bugs inserted while “programming in the small” can have dramatic consequences for the consistency of a whole software system as shown, e.g., by viruses which can spread by exploiting buffer overflows, a bug which typically arises while coding a small portion of code. To detect this kind of errors, many verification techniques have been put forward such as static analysis and model checking.
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
Preview
Unable to display preview. Download preview PDF.
References
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: Extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) FroCos 2005. LNCS, vol. 3717, pp. 65–80. Springer, Heidelberg (2005)
Armando, A., Ranise, S., Rusinowitch, M.: A Rewriting Approach to Satisfiability Procedures. Information and Computation 183(2), 140–164 (2003)
Déharbe, D., Ranise, S.: Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In: Proc. of the Int. Conf. on Software Engineering and Formal Methods (SEFM 2003), pp. 220–228. IEEE Computer Society, Los Alamitos (2003)
Déharbe, D., Ranise, S.: Satisfiability Solving for Software Verification. In: Proc. of IEEE/NASA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2005) (2005)
Fontaine, P.: Techniques for verification of concurrent systems with invariants. PhD thesis, Institut Montefiore, Université de Liège, Belgium (September 2004)
Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 167–181. Springer, Heidelberg (2006)
Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: On Superposition-Based Satisfiability Procedures and Their Combination. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 594–608. Springer, Heidelberg (2005)
Nelson, G.: Techniques for Program Verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center (June 1981)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. on Programming Languages and Systems 1(2), 245–257 (1979)
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL. A Proof Assistant for Higher-Order Logic. In: Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.) Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Ranise, S., Ringeissen, C., Tran, D.-K.: Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 372–386. Springer, Heidelberg (2005)
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCos 2005. LNCS, vol. 3717, pp. 48–64. Springer, Heidelberg (2005)
Shankar, N., Rueß, H.: Combining shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 1–18. Springer, Heidelberg (2002)
Shostak, R.E.: Deciding combinations of theories. J. of the ACM 31, 1–12 (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Déharbe, D., Fontaine, P., Ranise, S., Ringeissen, C. (2006). Decision Procedures for the Formal Analysis of Software. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds) Theoretical Aspects of Computing - ICTAC 2006. ICTAC 2006. Lecture Notes in Computer Science, vol 4281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11921240_26
Download citation
DOI: https://doi.org/10.1007/11921240_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48815-6
Online ISBN: 978-3-540-48816-3
eBook Packages: Computer ScienceComputer Science (R0)