Daniel Gaina


Assistant Professor, Ph.D., Research center for software verification, Japan Advanced Institute of Science and Technology
My research interests are rooted within algebraic specification, one of the most promising aproach to formal methods assisting the developing of software systems at several stages such as design, specification and formal verification. Algebraic specification and programming languages are rigorously based on logic, which amounts to the existence of a logical system underlying the language such that each language feature and construction can be expressed as a mathematical entity of the underlying logic.
The current goal of my research is to develop mathematical and logical structures supporting the efficient development of correct reconfigurable software systems, i.e. systems with reconfigurable mechanisms managing the dynamic evolution of their configurations in response to external stimuli or internal performance measures. A typical example of reconfigurable system is given by the cloud-based applications that flexibly react to client demands by allocating, for example, new server units to meet higher rates of service requests. The model implemented over the cloud is pay-per-usage, which means that the users will pay only for using the services. Therefore, the cloud service providers have to maintain a certain level of quality of service to keep up the reputation.
Reconfigurable systems are safety- and security-critical systems with strong qualitative requirements, and consequently, formal verification is needed.
Keywords: Logic, Formal Methods, Category Theory

Google Scholar

Journal papers

  1. Daniel Găină,
    Birkhoff Style Calculi for Hybrid Logics,
    Formal Aspects of Computing, accepted
  2. Daniel Găină,
    Downward Löwenheim-Skolem Theorem and interpolation in logics with constructors,
    Journal of Logic and Computation, doi: 10.1093/logcom/exv018, 2015 (pdf)
  3. Daniel Găină and Kokichi Futatsugi,
    Initial semantics in logics with constructors,
    Journal of Logic and Computation, vol. 25, No. 1, pp. 95-116, 2015 (pdf)
  4. Daniel Găină,
    Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, institutionally,
    Logica Universalis, Vol. 8, No. 3, pp. 469-498, 2014 (pdf)
  5. Daniel Găină,
    Interpolation in logics with constructors,
    Theoretical Computer Science, Vol. 474, pp. 46-59, 2013 (pdf)
  6. Daniel Găină, Kokichi Futatsugi and Kazuhiro Ogata,
    Constructor-based Logics,
    Journal of Universal Computer Science, Vol. 18, No. 16, pp. 2204-2233, 2012 (pdf)
  7. Kokichi Futatsugi, Daniel Găină and Kazuhiro Ogata,
    Principles of proof scores in CafeOBJ,
    Theoretical Computer Science, Vol. 464, pp. 90-112, 2012
  8. Daniel Găină and Marius Petria,
    Completeness by Forcing,
    Journal of Logic and Computation, Vol. 20, No. 6, pp. 1165-1186, 2010 (pdf)
  9. Mihai Codescu and Daniel Găină,
    Birkhoff Completeness in Institutions,
    Logica Universalis, Vol. 2, No. 2, pp. 277-309, 2008 (pdf)
  10. Daniel Găină and Andrei Popescu,
    An Institution-Independent Proof of the Robinson Consistency Theorem,
    Studia Logica, Vol. 85, No. 1, pp. 41-73, 2007
  11. Daniel Găină and Andrei Popescu,
    An Institution-independent Generalization of Tarski's Elementary Chain Theorem,
    Journal of Logic and Computation, Vol. 16, No. 6, pp. 713-735, 2006 (pdf)

Conference papers

  1. Masaki Nakamura, Daniel Găină, Kazuhiro Ogata and Kokichi Futatsugi,
    Proving Sufficient Completeness of Constructor-Based Algebraic Specifications ,
    In Proceedings of the International Conference on Advances in Computer Science and Ubiquitous Computing, Cebu, Philippines, December 15-17, 2015
  2. Daniel Găină,
    Foundations of Logic Programming in Hybridised Logics ,
    22nd International Workshop on Algebraic Development Techniques, WADT 2014, Sinaia, Romania, September 4-7, 2014 (pdf)
  3. Daniel Găină, Dorel Lucanu, Kazuhiro Ogata and Kokichi Futatsugi,
    On Automation of OTS/CafeOBJ Method ,
    in Proceedings of SAS 2014, Kanazawa, Japan, April 14-16, 2014 (pdf)
  4. Daniel Găină, Zhang Min, Yuki Chiba and Yasuhito Arimoto,
    Constructor-based Inductive Theorem Prover,
    In Proceedings of 5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013, Warsaw, Poland, September 3-6, 2013
  5. Daniel Găină, Kokichi Futatsugi and Kazuhiro Ogata,
    Constructor-Based Institutions ,
    In Proceedings of the 3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009, Udine, Italy, September 7-10, 2009

Constructor-based Inductive Theorem Prover (CITP)


Daniel Gaina
danieldomain of mail address(at jaist.ac.jp)