I am mostly interested in abstract interpretation theory and approximation methods in any area of computer science, from semantics to static program analysis, software and hardware verification, model-checking and abstract model-checking, program transformation and optimization, software watermarking and code obfuscation, complexity and computability, logic and constraint-based programming, security and safety critical systems. Recently I am more and more interested in applying these mathods in security analysis, code obfuscation and in computational biology. In all these fields I am interested in studying systematic methods for approximating undecidable or highly complex problems my means of formal methods such as abstract interpretation. I believe that abstract interpretation represents a unifying theory for understanding most phenomena connected with computation. In pure math I am interested in lattice theory and closure systems.
This is a brief summary of my research in the last few years:
- Abstract interpretation theory and applications: This is my main current research interest. Abstract interpretation is a general theory for approximating discrete dynamic systems [see Cousot]. A central role in this theory is played by the notion of abstract domain. We defined a number of formal and constructive systematic methods for domain design in abstract interpretation. These can be classified [FGR96,GR98b, GR97a] in terms of domain refinements [GR97b, GS97, GR95, GR98c ], domain simplificators [GR97b], and domain compressors [GR98a, CFGPR97]. Of particular importance are the systematic operations to make an abstract interpretation complete [GRS00], providing powerful formal methods to constructively design optimal domains for abstract interpretation. The results are universal, independent from specific programming languages, and can be applied to any abstract interpretation. Some of these operations have been applied in many areas of computer science. In particular in static program analysis [GR97a, GR97b, GS97, GR95, GR98c] GRS03], program manipulation (such as program slicing) [GM02], comparative semantics of programming languages [GR99, GM00, G02], abstract model-checking [GQ01, GR06], and language-based security [GM04]. We are currently interested in applying these theories in computational complexity of approximate algorithms, computational biology, analysis and verification of hybrid systems, and in program testing of large-scale software systems. As far as the theory is concerned, we are working in the definition of a unifying theory for abstract domain design. This theory is based on standard principles of domain-theory. The idea is to develop a mathematical foundation of abstract domain transformers which is adequate to specify both first and higher-order domain operations for domain refinement, simplification, and compression. Preliminary results are in [GM03].
- Language-based security: We are currently interested in weakening non-interference in static program analysis for language-based security. The manifesto of our research in this field appeared in POPL'04 [GM04]. The idea is weakening non-interference by abstract interpretation and considering abstract domain trensformers to model attackers. We are currently interested in extending this research towards concurrent and timed programming languages. Preliminary results are available in [GM05a] and [GM05b]. Abstract Non Interference is also a unifying paradigm for modeling both declassification and attack models, as proved in [GM05].
- Lattice theory: Standard abstract interpretation theory is based on the isomorphism between the lattice of all abstractions on a given domain and the lattice of all its closure operators. The study of abstract interpretation theory have therefore lead us to have results in the theory of closure operators on complete lattices [GPR96,GR98,GR98b]. We are now interested in complete congruence lattices, currently a hot topic in lattice theory. In [GR98b] we proved an embedding of the lattice of complete congruences on a continuous lattice into the lattice of all its closure operators. This allows us to extend most properties of the lattice of closure operators to the lattice of complete congruences on continuous lattices. This result is a consequence of our research in abstract interpretation completeness [GR97b,GRS00].
- Semantics: We studied semantics for modeling control features of Prolog programs [BCGL93, BCGM95] and the hierarchy of semantics for pure logic programs based on abstract interpretation [G96]. Systematic methods for domain construction have been applied for designing semantics of arbitrary transition systems [GR96,GR95,GM00, GM02].
- Static program analysis: We studied deductive [GG94, BGL93], abductive [G98] and compositional [CDG93] methods for static analysis of logic programs. Specific domains have been studied for the analysis of types [BG92], deterministic computations [GR92], query optimization [CCG94], and numeric constraint optimization [BGL93]. Abstract interpretation has been applied also to specify static analyzers for constraint logic programs [GDL95] and concurrent constraint programs [ZGL97].
- Software watermarking and code obfuscation: We introduced a semantic-based model for specifying code obfuscation algorithms. The idea is to view code obfuscation, and therefore software watermarking, as an abstraction of the concrete semantics of a program [DG05]. Robust algorithms for code obfuscation can then be derived systematically, e.g. in control code obfuscation by opaque predicate insertion, by abstract interpretation from semantic transformers [DG05b, DMDG06].
You can find some selected papers here. If you want to have a
deeper look on some sort of manifesto of my research, check
here my dream (...or
nightmare) or check my invited lecture at MFPS'02 [G02].
... (from the Cartoonbank)