Abstract
Saturn is a boolean satisfiability (SAT) based framework for static bug detection. Saturn targets software written in C and is designed to support a wide range of property checkers.
Supported by NSF grant CCF-0430378.
Chapter PDF
Similar content being viewed by others
References
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)
Aiken, A., Foster, J.S., Kodumal, J., Terauchi, T.: Checking and inferring local non-aliasing. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pp. 129–140 (June 2003)
Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Das, M., Lerner, S., Seigle, M.: Path-sensitive program verification in polynomial time. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, Berlin, Germany (June 2002)
Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system specific, programmer-written compiler extensions. In: Proceedings of Operating Systems Design and Implementation, OSDI (September 2000)
Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pp. 1–12 (June 2002)
Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, Berlin, Germany (June 2002)
Henzinger, T.A., Jhala, R., Majumdar, R.: Lazy abstraction. In: Proceedings of the 29th Annual Symposium on Principles of Programming Languages, POPL (January 2002)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Ivancic, F., Yang, Z., Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. In: Proceedings of 1st International Symposium on Leveraging Applications of Formal Methods, ISoLA (2004)
Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Proceedings of the 2000 ACM SIGSOFT International Symposium on Software Testing and Analysis (2000)
Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of the 40th Design Automation Conference (2003)
Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, p. 213. Springer, Heidelberg (2002)
Semeria, L., Micheli, G.D.: SpC: synthesis of pointers in C, application of pointer analysis to the behavioral synthesis from C. In: Proceedings of 21st IEEE/ACM International Conference on Computer Aided Design, ICCAD (1998)
Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Proceedings of the 32th Annual Symposium on Principles of Programming Languages, POPL (January 2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xie, Y., Aiken, A. (2005). Saturn: A SAT-Based Tool for Bug Detection. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_13
Download citation
DOI: https://doi.org/10.1007/11513988_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)