Exploring Different Constraint-Based Modelings for Program Verification

1. Aït-Kaci, H., Berstel, B., Junker, U., Leconte, M., Podelski, A.: Satisfiability Modulo Structures as Constraint Satisfaction: An Introduction. In: Procs. of JFLA, 8 pages (2007)

   Google Scholar 

2. Armando, A., Mantovani, J., Platania, L.: Bounded Model Checking of C Programs using a SMT solver instead of a SAT solver Technical Report, AI-Lab, DIST, University of Genova, 16 pages (December 19, 2005)

   Google Scholar 

3. Bouquet, F., Dadeau, F., Legeard, B., Utting, M.: JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 551–556. Springer, Heidelberg (2005)

   Google Scholar 

4. 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)

   Google Scholar 

5. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)

   Google Scholar 

6. Gotlieb, A., Botella, B., Rueher, M.: Automatic Test Data Generation using Constraint Solving Techniques. In: Proc. ISSTA 1998, ACM SIGSOFT, vol. 2, pp. 53–62 (1998)

   Google Scholar 

7. Leconte, M., Berstel, B.: Extending a CP Solver with Congruences as Domains for Program Verification. In: Procs. of CSTVA 2006, 1st Workshop on Constraints in Software Testing, Verification and Analysis, Nantes (2006)

   Google Scholar 

8. Collavizza, H., Rueher, M.: Software Verification using Constraint Programming Techniques. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 182–196. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

9. Cytron, R., Ferrante, J., Rosen, B., Wegman, M., Zadeck, K.: Efficently Computing Static Single Assignment Form and the Control Dependence Graph. Transactions on Programming Languages and Systems 13(4), 451–490 (1991)

   Article  Google Scholar 

10. Ganai, M., Gupta, A., Ashar, P.: DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 575–580. Springer, Heidelberg (2005)

    Google Scholar 

11. Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. of DAC, pp. 530–535 (2001)

    Google Scholar 

12. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT an SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM (to appear)

    Google Scholar 

13. Sy, N.T., Deville, Y.: Automatic test data generation for programs with integer and float variables. In: Proc of. 16th IEEE International Conference on Automated Software Engineering(ASE 2001), IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

Download references