CSSV swMATH ID: 13701 Software Authors: Dor, N., Rodeh, M., Sagiv, M Description: CSSV: Towards a realistic tool for statically detecting all buffer overflows in C. Erroneous string manipulations are a major source of software defects in C programs yielding vulnerabilities which are exploited by software viruses. We present C String Static Verifyer (CSSV), a tool that statically uncovers all string manipulation errors. Being a conservative tool, it reports all such errors at the expense of sometimes generating false alarms. Fortunately, only a small number of false alarms are reported, thereby proving that statically reducing software vulnerability is achievable. CSSV handles large programs by analyzing each procedure separately. To this end procedure contracts are allowed which are verified by the tool.We implemented a CSSV prototype and used it to verify the absence of errors in real code from EADS Airbus. When applied to another commonly used string intensive application, CSSV uncovered real bugs with very few false alarms. Homepage: http://dl.acm.org/citation.cfm?id=781149 Related Software: ASTREE; TVLA; CBMC; SPEED; PPL; Octagon; Consit; Privtrans; Privman; MOPS; CCured; RacerX; aiT; Houdini; SatAbs; ESC/Java; ARMC; SLAM; Dafny; Cibai Cited in: 16 Documents all top 5 Cited by 31 Authors 3 Gupta, Aarti 3 Ivančić, Franjo 2 Gulwani, Sumit 2 Kröning, Daniel 2 Reps, Thomas W. 2 Rival, Xavier 2 Sagiv, Mooly 2 Sankaranarayanan, Sriram 2 Sharygina, Natasha 2 Simon, Axel 2 Tonetta, Stefano 2 Tsitovich, Aliaksei 2 Wintersteiger, Christoph M. 1 Allamigeon, Xavier 1 Ashar, Pranav 1 Balakrishnan, Gogul 1 Bultan, Tevfik 1 Chilimbi, Trishul M. 1 Fähndrich, Manuel 1 Ganai, Malay K. 1 Godard, Wenceslas 1 Hymans, Charles 1 Ibarra, Oscar H. 1 King, Andy 1 Lev-Ami, Tal 1 Logozzo, Francesco 1 McCloskey, Bill 1 Mehra, Krishna K. 1 Shlyakhter, Ilya 1 Yang, Zijiang 1 Yu, Fang Cited in 3 Serials 1 Theoretical Computer Science 1 Science of Computer Programming 1 Formal Methods in System Design Cited in 2 Fields 16 Computer science (68-XX) 1 Numerical analysis (65-XX) Citations by Year