05342690

a

05342690 D\'eharbe, David Fontaine, Pascal Ranise, Silvio Ringeissen, Christophe Decision procedures for the formal analysis of software. Barkaoui, Kamel (ed.) et al., Theoretical aspects of computing -- ICTAC 2006. Third international colloquium, Tunis, Tunisia, November 20--24, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-48815-6/pbk). Lecture Notes in Computer Science 4281, 366-370 (2006). 2006 Berlin: Springer EN

doi:10.1007/11921240_26

Summary: 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.