Daniel Găină
|
Associate professor
Research interests
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.
Area of study
- Logic
- Formal Methods
- Category Theory
Journal papers
- Daniel Găină, Guillermo Badia and Tomasz Kowalski,
Omitting Types Theorem in hybrid dynamic first-order logic with rigid symbols,
Annals of Pure and Applied Logic, 2023
(pdf)
- Daniel Găină and Tomasz Kowalski,
Lindström’s theorem, both syntax and semantics free,
Journal of Logic and Computation, vol. 32, issue 5,
pp. 942–975, July 2022,
(pdf)
- Daniel Găină, Masaki Nakamura, Kazuhiro Ogata
and Kokichi Futatsugi,
Stability of termination and
sufficient-completeness under pushouts via amalgamation
,
Theoretical Computer Science, vol. 848, pp. 82-105, 2020
(pdf)
- Daniel Găină and Tomasz Kowalski,
Fraïssé-Hintikka Theorem in institutions,
Journal of Logic and Computation, vol. 30, issue 7, pp.
1377-1399, 2020
(pdf)
- Daniel Găină,
Forcing and Calculi for Hybrid Logics,
Journal of the ACM, vol. 67, issue 4, pp. 1-55, 2020
(pdf)
- Daniel Găină,
Birkhoff Style Calculi for Hybrid Logics,
Formal Aspects of Computing, vol. 29, issue 5, pp. 805-832, 2017
(pdf)
- Daniel Găină,
Downward Löwenheim-Skolem Theorem and
interpolation in logics with constructors,
Journal of Logic and Computation, vol. 27, issue 6, pp.1717-1752, 2017
(pdf)
- Daniel Găină,
Foundations of logic programming in hybrid logics with user-defined sharing,
Theoretical Computer Science, vol. 686, pp. 1-24, 2017
(pdf)
- Daniel Găină and Kokichi Futatsugi,
Initial semantics in logics with constructors,
Journal of Logic and Computation, vol. 25, issue 1, pp. 95-116, 2015
(pdf)
- Daniel Găină,
Forcing, Downward Löwenheim-Skolem and Omitting
Types Theorems, institutionally,
Logica Universalis, vol. 8, issue 3-4, pp. 469-498, 2014
(pdf)
- Daniel Găină,
Interpolation in logics with constructors,
Theoretical Computer Science, vol. 474, pp. 46-59, 2013
(pdf)
- Daniel Găină, Kokichi Futatsugi and Kazuhiro Ogata,
Constructor-based Logics,
Journal of Universal Computer Science, vol. 18, issue 16, pp. 2204-2233, 2012
(pdf)
- Kokichi Futatsugi, Daniel Găină and Kazuhiro Ogata,
Principles of proof scores in CafeOBJ,
Theoretical Computer Science, vol. 464, pp. 90-112, 2012
- Daniel Găină and Marius Petria,
Completeness by Forcing,
Journal of Logic and Computation, vol. 20, issue 6, pp. 1165-1186, 2010
(pdf)
- Mihai Codescu and Daniel Găină,
Birkhoff Completeness in Institutions,
Logica Universalis, vol. 2, issue 2, pp. 277-309, 2008
(pdf)
- Daniel Găină and Andrei Popescu,
An Institution-Independent Proof of the Robinson
Consistency Theorem,
Studia Logica, vol. 85, issue 1, pp. 41-73, 2007
- Daniel Găină and Andrei Popescu,
An Institution-independent Generalization of
Tarski's Elementary Chain Theorem,
Journal of Logic and Computation, vol. 16, issue 6, pp. 713-735, 2006
(pdf)
Conference papers
- Daniel Găină,
Birkhoff style proof systems for hybrid-dynamic quantum logic ,
In Proceedings of Advances in Modal Logic (AiML 2024), Prague, The Czech Republic, 19–23 August, 2024
(pdf)
- Go Hashimoto, Daniel Găină and Ionut Tutu
Forcing, Transition Algebras, and Calculi ,
In Proceedings of 51st EATCS International Colloquium on Automata, Languages and Programming (ICALP 2024), Tallinn, Estonia, 8-13 July 2024
(pdf)
- Daniel Găină, Guillermo Badia and Tomasz Kowalski,
Robinson consistency in many-sorted
hybrid first-order logics ,
In Proceedings of Advances in Modal Logic (AiML 2022), Rennes,
22-25 August, 2022
(pdf)
- Daniel Găină and Ionut Tutu,
Birkhoff Completeness for Hybrid-Dynamic First-Order Logic ,
In Proceedings of 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019), London, UK, September 3-5, 2019
(pdf)
- Daniel Găină, Ionut Tutu and Adrian Riesco,
Specification and Verification of Invariant Properties of Transition Systems ,
In Proceedings of 25th Asia-Pacific Software Engineering Conference (APSEC 2018), Nara, Japan, December 4-7, 2018
(pdf)
- 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)
- 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
- 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
- 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