Ando Saabas
Publications
-
A. Saabas. Logics for Low-Level Code and Proof-Preserving Program Transformations. PhD thesis.
-
M. Veanes, A. Saabas. On bounded reachability of programs with set comprehensions. In Proc. of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2008 (Doha, Qatar, November 2008), v. 5330 of Lecture Notes in Computer Science, pp. 305-317, Springer Verlag 2008.
-
A. Saabas, T. Uustalu. Program and proof optimizations with type systems. J. of Logic and Algebraic Programming, v. 77, n. 1-2, pp. 131-154, 2008
-
A. Saabas, T. Uustalu. Proof optimization for partial redundancy
elimination. In Proc. of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'08 (San Francisco, January 2008), pp. 91-101, ACM, 2008.
-
M. J. Frade, A. Saabas, T. Uustalu. Foundational certification of
data-flow analyses. In Proc. of the 1st IEEE and IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2007 (Shanghai, June 2007), pp. 107-116. IEEE CS Press, 2007.
-
A. Saabas, T. Uustalu. Type systems for optimizing stack-based code. In M.
Huisman, F. Spoto, eds., Proc. of 2nd Wksh. on Bytecode Semantics,
Verification, Analysis and Transformation, Bytecode 2007 (Braga, March
2007), Electron. Notes in Theor. Comput. Sci., to appear.
- A.
Saabas, T. Uustalu. Compositional
Type Systems
for Stack Based Low-Level Languages,
in B. Jay, J. Gudmundsson, eds., Proc. of 12th Computing, Australasian
Theory Symp., CATS 2006 (Hobart, Jan. 2006), v. 51 of Confs. in Research
and Practice in Inform. Techn., pp. 27-39. Australian Comput. Soc., 2006
- P. Grigorenko, A. Saabas,
E. Tyugu. Visual
Tool for Generative
Programming. Proc. of the ACM SIGSOFT Symposium on the Foundations of
Software Engineering, ACM Press, 2005.
- G. Barthe, T. Rezk, A. Saabas. Proof
Obligations Preserving
Compilation. Proc. of the 3rd Workshop on Formal Aspects in Security
and Trust, 2005, (Newcastle upon Tyne, 2005), v. 3866 of Lecture Notes in
computer Science, pp. 112-126, Springer Verlag 2006
-
A. Saabas, T. Uustalu. A compositional natural semantics and Hoare logic for low-level languages. Theor. Comput. Sci., v. 373, n. 3, pp. 273-302, 2007. // Conf. version in P. D Mosses, I. Ulidowski, eds., Proc. of 2nd Wksh. on Structured Operational Semantics, SOS '05 (Lisbon, July 2005), v. 156, n. 1 of Electron. Notes in Theor. Comput. Sci., pp. 151-168. Elsevier, 2006. Conference version
- P. Grigorenko, A. Saabas, E. Tyugu.
COCOVILA -
Compiler-Compiler for
Visual Languages. Proc. of the 5th Workshop on Language Descriptions,
Tools and Applications, 2005 (Edinburgh, April 2005), v. 141, n. 4 of
Electron. Notes in Theor. Comput. Sci., pp. 137-142. Elsevier, 2005
- A. Saabas, G.Barthe, L. Burdy, T.Rezk. Towards Programming Logics for Low Level Languages. Proc. of the 16th Nordic Workshop on Programming Theory, 2004, p.105-107.
- E. Tyugu, A. Saabas. Problems of Visual Specification Languages. Proc. of the 35th International Conference on IT + SE, Gurzuf, May 2003, p. 155 - 157.