Ando Saabas


    This page serves as an archive for some of my past ventures.


    • Sphider is a web spider and search engine written in PHP. It has attracted quite a few users and code contributers and is downloaded around 100 times a day.

    • Java Bytecode Editor is a tool for viewing and editing Java bytecode. It extends the jclasslib bytecode viewer.

    • CoCoViLa (Compiler Compiler for Visual Languages) is tool for developing domain specific, executable visual languages. It started as my Master's project, but has been the basis for several PhD theses since. It has been maintained and extended by Pavel Grigorenko and others at the Institute of Cybernetics.


    • 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.