|
 REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
ACKERMAN, W Solvable Cases of the Dectswn Problem. North-Holland Pub Co, Amsterdam, 1954, pp 102-103
|
| |
2
|
BLEDSOE, W.W The Sup-lnf method in Presburger anthmetic Memo ATP-18, Math Dept, U of Texas at Austin, Austin, Tex, Dec 1974.
|
| |
3
|
BLEDSOE, W W A new method for prowng certain Presburger formulas Advance Papers 4th Int Joint Conf on Amf Intell., Tiblhsl, Georgia, U S S.R, Sept. 1975, pp 15-21.
|
| |
4
|
COOPER, D C Programs for mechamcal program verification. In Mach Intell. 6, B. Meltzer and D Mlchte, Eds, Amencan Elsevier, New York, 1971, pp 43-59
|
| |
5
|
COOPER, D C Theorem proving m arithmetic without multnphcatlon In Mach Intell 7, B Meltzer and D Michle, Eds, American Elsevier, New York, 1972, pp 91-99
|
| |
6
|
DOWNEY, P Undecldabdlty of Presburger arithmetic with a single monadic predicate letter Tech Rep 18- 72, Center for Research in Computing Technology, Harvard U, Cambridge, Mass, 1972
|
| |
7
|
ELSPAS, B, BOYER, R E, SHOSTAK, R, AND SPITZEN, J A verification system for JOVIAL/J3 programs SRI Tech Rep 3756-1, Stanford Research Institute, Menlo Park, Cahf, Jan 1976
|
| |
8
|
GOMORY, R E An algonthrn for integer solutions to linear programs Princeton-IBM Math Res Rep, Nov 1958, also in Recent Advances in Mathemaucal Programming, R.L Graves and P Wolfe, Eds, McGraw-Hill, New York, 1963, pp. 269-302.
|
| |
9
|
KREISEL, G, AND KREVINE, J L Elements of Mathemattcal Logtc North-Holland Pub Co, Amsterdam, 1967, pp 54--57
|
| |
10
|
LEE, R D An apphcatton of mathemaucal logic to the integer hnear programming problem Notre Dame J. Formal Logtc XIII, 2 (Aprd 1972), 279-282
|
| |
11
|
MCCARTHY, J. Towards a mathematmal science of computation Proc IFIP Congress 62, North-Holland Pub Co, Amsterdam, 1962, pp 21-28.
|
 |
12
|
|
| |
13
|
OPPEN, D A 2z: upper bound on the complexity of Presburger arithmetic Ph D. Th, U of Toronto, Toronto, Ont, Canada, 1975, J. Comptr Syst Sct (to appear)
|
| |
14
|
PRESBURGER, M Uber die Vollstandigkeit emes gewlssen Systems der Anthmetlk ganzer Zahlen m Welchem die Addition als elnzige Operation hervortntt Sprawozdame z I Kongresu Matematykow Krajow Slowcansklch Warszawa, 1929, Warsaw, Poland, pp. 92-101
|
| |
15
|
SHOSTAK, R An algorithm for reasonmg about equality Proc Seventh Int Joint Conf on Amf Intell, Cambndge, Mass, Aug 1977
|
| |
16
|
|
| |
17
|
|
CITED BY 21
|
|
|
|
|
|
|
|
Robert B. Jones , David L. Dill , Jerry R. Burch, Efficient validity checking for processor verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.2-6, November 05-09, 1995, San Jose, California, United States
|
|
|
|
|
|
|
|
|
Allen Goldberg , T. C. Wang , David Zimmerman, Applications of feasible path analysis to program testing, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.80-94, August 17-19, 1994, Seattle, Washington, United States
|
|
|
|
|
|
Tai-Hung Liu , Khurram Sajid , Adnam Aziz , Vigyan Singhal, Optimizing designs containing black boxes, Proceedings of the 34th annual conference on Design automation, p.113-116, June 09-13, 1997, Anaheim, California, United States
|
|
|
David Y. W. Park , Jens U. Skakkebæk , Mats P. E. Heimdahl , Barbara J. Czerny , David L. Dill, Checking properties of safety critical specifications using efficient decision procedures, Proceedings of the second workshop on Formal methods in software practice, p.34-43, March 04-05, 1998, Clearwater Beach, Florida, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
G.1