Abstract
C32SAT is a tool for checking C expressions. It can check whether a given C expression can be satisfied, is tautological, or always defined according to the ISO C99 standard. C32SAT can be used to detect nonportable expressions where program behavior depends on the compiler. Our contribution consists of C32SAT’s functional representation and the way it handles undefined values. Under-approximation is used as optimization.
Chapter PDF
Similar content being viewed by others
Keywords
- Conjunctive Normal Form
- Satisfying Assignment
- Program Behavior
- Predicate Abstraction
- Logical Disjunction
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Biere, A.: The evolution from LIMMAT to NANOSAT. Technical Report 444, Dept. Computer Science, ETH ZĂ¼rich (2004)
Biere, A.: Occurrence lists for 2-watched literal schemes (submitted)
Biere, A., Sinz, C.: Decomposing sat problems into connected components. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 2 (2006)
Brummayer, R., Biere, A.: Local two-level And-Inverter Graph minimization without blowup. In: MEMICS 2006. Proceedings of the 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (2006)
Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Proceedings of TACAS 2007, Springer, Heidelberg (to appear, 2007)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-Cprograms. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)
Cook, B., Kroening, D., Sharygina, N.: Cogent: Accurate theorem proving for program verification. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 296–300. Springer, Heidelberg (2005)
ISO/IEC. Programming languages - C (ISO/IEC 9899:1999(E)) (1999)
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. on CAD of Integrated Circuits and Systems 21(12), 1377–1394 (2002)
Sethi, N., Barret, C.: Cascade: C assertion checker and deductive engine. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 166–169. Springer, Heidelberg (2006)
Tseitin, G.S.: On the complexity of derivation in the propositional calculus. Studies in constructive mathematics and mathematical logic, pp. 115–125 (1968)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brummayer, R., Biere, A. (2007). C32SAT: Checking C Expressions. In: Damm, W., Hermanns, H. (eds) Computer Aided Verification. CAV 2007. Lecture Notes in Computer Science, vol 4590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73368-3_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-73368-3_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73367-6
Online ISBN: 978-3-540-73368-3
eBook Packages: Computer ScienceComputer Science (R0)