@INPROCEEDINGS{AA-MPB-SR-MR-AKS:VERIFY2002:array, AUTHOR = "Alessandro Armando and Maria Paola Bonacina and Silvio Ranise and Micha{\"e}l Rusinowitch and Aditya Kumar Sehgal", TITLE = "High-performance deduction for verification: a case study in the theory of arrays", BOOKTITLE = "Proceedings of the 2nd International Workshop on Verification (VERIFY)", EDITOR = "Serge Autexier and Heiko Mantel", PUBLISHER = "DIKU, University of Copenhagen, Denmark", SERIES = "Technical Reports", NUMBER = "07/2002", PAGES = "103--112", MONTH = "July", YEAR = 2002}