Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland, Amsterdam (1954)
MATH
Google Scholar
Amon, T., Borriello, G., Hu, T., Liu, J.: Symbolic Timing Verification of Timing Diagrams Using Presburger Formulas. In: DAC, pp. 226–231 (1997)
Google Scholar
ARIO SMT Solver,
http://www.eecs.umich.edu/~ario
Audemard, G., Bertoli, P., Cimatti, A., Kornilowics, A., Sebastiani, R.: A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 193–208. Springer, Heidelberg (2002)
Google Scholar
Barrett, C., Dill, D., Levitt, J.: Validity Checking for Combinations of Theories with Equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 187–201. Springer, Heidelberg (1996)
Chapter
Google Scholar
Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., van Rossum, P., Schulz, S., Sebastiani, R.: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 317–333. Springer, Heidelberg (2005)
Chapter
Google Scholar
Brinkmann, R., Drechsler, R.: RTL-datapath Verification Using Integer Linear Programming. In: VLSI Design, pp. 741–746 (2002)
Google Scholar
Brzozowski, J.A., Seger, C.J.H.: Asynchronous Circuits. Springer, Heidelberg (1994)
Google Scholar
Chvátal, V.: Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Math. 4, 305–337 (1973)
Article
MATH
MathSciNet
Google Scholar
Dash Inc., XPRESS-MP 15.25.03,
http://www.dashoptimization.com
Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. Tech. Report HPL-2003-148, HP Labs (2003)
Google Scholar
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Chapter
Google Scholar
Filliatre, J.C., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 246–249. Springer, Heidelberg (2001)
Chapter
Google Scholar
Ganapathy, V., Seshia, S.A., Jha, S., Reps, T.W., Bryant, R.E.: Automatic Discovery of API-Level Exploits. In: ICSE (2005)
Google Scholar
Ganesh, V., Berezin, S., Dill, D.L.: Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 171–186. Springer, Heidelberg (2002)
Chapter
Google Scholar
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)
Chapter
Google Scholar
ILOG CPLEX,
http://www.ilog.com/products/cplex
Iyer, M.K., Parthasarathy, G., Cheng, K.-T.: Efficient Conflict-Based Learning in an RTL Circuit Constraint Solver. In: DATE, pp. 666–671 (2005)
Google Scholar
Jaffar, J., Maher, M., Suckey, P., Yap, R.: Beyond Finite Domains. In: Borning, A. (ed.) PPCP 1994. LNCS, vol. 874, pp. 86–94. Springer, Heidelberg (1994)
Google Scholar
Kroening, D., Ouaknine, J., Seshia, S., Strichman, O.: Abstraction-based Satisfiability Solving of Presburger Arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 308–320. Springer, Heidelberg (2004)
Chapter
Google Scholar
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. on Computers 48(5), 506–521 (1999)
Article
MathSciNet
Google Scholar
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC, pp. 530–535 (2001)
Google Scholar
de Moura, L., Rueß, H.: An Experimental Evaluation of Ground Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 162–174. Springer, Heidelberg (2004)
Chapter
Google Scholar
Nelson, G., Oppen, D.C.: Simplification by Cooperating Decision Procedures. ACM Trans. on Programming Languages and Systems 1, 245–257 (1979)
Article
MATH
Google Scholar
Presburger, M.: Uber die Vollstandigkeit eines Gewissen Systems der Arithmetik Ganzer Zahlen, in Welchem die Addition als Einzige Operation Hervortritt. Comptes-rendus du premier congres des mathematiciens des pays slaves 395, 92–101 (1929)
Google Scholar
Pugh, W.: The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis. In: ACM conf. on Supercomputing, pp. 4–13 (1991)
Google Scholar
Rueß, H., Shankar, N.: Solving Linear Arithmetic Constraints. SRI International Tech. Report CSL-SRI-04-01 (January 2004)
Google Scholar
Seshia, S., Bryant, R.: Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. In: LICS, pp. 100–109 (2004)
Google Scholar
Shostak, R.: Deciding Combination of Theories. Journal of the ACM 31, 1–12 (1984)
Article
MATH
MathSciNet
Google Scholar
Shostak, R.: Deciding Linear Inequalities by Computing Loop Residues. Journal of the ACM 28(4), 769–779 (1981)
Article
MATH
MathSciNet
Google Scholar
Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding Separation Formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 209–222. Springer, Heidelberg (2002)
Chapter
Google Scholar
Wagner, D., Foster, J.S., Brewer, E.A., Aiken, A.: A First Step Towards Detection of Buffer Overrun Vulnerabilities. In: Network and Distributed System Security Symposium, Internet Society (2000)
Google Scholar
Wilson, J.M.: Compact Normal Forms in Propositional Logic and Integer Programming Formulations. Computers and Operation Research, 309–314 (1990)
Google Scholar