2013
Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks
Publication
Publication
Presented at the
Conference on Current Trends in Theory and Practice of Computer Science, Špindlerův Mlýn
We present a completeness proof of the inductive assertion method for object-oriented programs extended with auxiliary variables. The class of programs considered are assumed to compute over structures which include the standard interpretation of Presburger arithmetic. Further, the assertion language is first-order, i.e., quantification only ranges over basic types like that of the natural numbers, Boolean and Object.
| Additional Metadata | |
|---|---|
| , , , , , | |
| , | |
| Springer | |
| P. van Emde Boas (Peter) , F.C.A. Groen , G.F. Italiano , J.R. Nawrocki , H. Sack | |
| Lecture Notes in Computer Science | |
| Highly Adaptable and Trustworthy Software using Forma Methods | |
| Conference on Current Trends in Theory and Practice of Computer Science | |
| Organisation | Computer Security |
|
de Gouw, S., de Boer, F., Ahrendt, W., & Bubel, R. (2013). Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks. In P. van Emde Boas, F. C. A. Groen, G. F. Italiano, J. R. Nawrocki, & H. Sack (Eds.), SOFSEM 2013: Theory and Practice of Computer Science, 39th International Conference on Current Trends in Theory and Practice of Computer Science (pp. 207–219). Springer. |
|
