Convex Hull of Arithmetic Automata

1. Becker, B., Dax, C., Eisinger, J., Klaedtke, F.: Lira: Handling constraints of linear arithmetics over the integers and the reals. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 307–310. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

2. Boigelot, B., Herbreteau, F.: The power of hybrid acceleration. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 438–451. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

3. Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log. 6(3), 614–633 (2005)

   Article  MathSciNet  Google Scholar 

4. Bardin, S., Leroux, J., Point, G.: Fast extended release. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 63–66. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

5. Boigelot, B., Rassart, S., Wolper, P.: On the expressiveness of real and integer arithmetic automata (extended abstract). In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 152–163. Springer, Heidelberg (1998)

   Chapter  Google Scholar 

6. Finkel, A., Leroux, J.: The convex hull of a regular set of integer vectors is polyhedral and effectively computable. Information Processing Letter 96(1), 30–35 (2005)

   Article  MathSciNet  Google Scholar 

7. Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976)

   Article  MATH  MathSciNet  Google Scholar 

8. Latour, L.: From automata to formulas: Convex integer polyhedra. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), Turku, Finland, July 14-17, 2004, pp. 120–129. IEEE Computer Society, Los Alamitos (2004)

   Chapter  Google Scholar 

9. Leroux, J.: The affine hull of a binary automaton is computable in polynomial time. In: Verification of Infinite State Systems, 5th International Workshop, INFINITY 2003, Marseille, France, September 2, 2003, vol. 98, pp. 89–104. Elsevier, Amsterdam (2003)

   Google Scholar 

10. Leroux, J.: A polynomial time presburger criterion and synthesis for number decision diagrams. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, June 26-29, 2005, pp. 147–156. IEEE Computer Society, Los Alamitos (2005)

    Chapter  Google Scholar 

11. Leroux, J., Point, G.: TaPAS: The Talence Presburger Arithmetic Suite (submited, 2008)

    Google Scholar 

12. Leroux, J., Sutre, G.: Accelerated data-flow analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, Springer, Heidelberg (2007)

    Chapter  Google Scholar 

13. Leroux, J., Sutre, G.: Acceleration in convex data-flow analysis. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 520–531. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

14. Lugiez, D.: From automata to semilinear sets: A logical solution for sets L(C, P). In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds.) CIAA 2004. D. Lugiez, vol. 3317, pp. 321–322. Springer, Heidelberg (2005)

    Google Scholar 

15. Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, New York (1987)

    Google Scholar 

Download references