Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Purchase individual online access for 1 year to this journal.
Price: EUR 410.00Impact Factor 2024: 0.4
Fundamenta Informaticae is an international journal publishing original research results in all areas of theoretical computer science. Papers are encouraged contributing:
- solutions by mathematical methods of problems emerging in computer science
- solutions of mathematical problems inspired by computer science.
Topics of interest include (but are not restricted to): theory of computing, complexity theory, algorithms and data structures, computational aspects of combinatorics and graph theory, programming language theory, theoretical aspects of programming languages, computer-aided verification, computer science logic, database theory, logic programming, automated deduction, formal languages and automata theory, concurrency and distributed computing, cryptography and security, theoretical issues in artificial intelligence, machine learning, pattern recognition, algorithmic game theory, bioinformatics and computational biology, quantum computing, probabilistic methods, & algebraic and categorical methods.
Authors: Hermenegildo, Manuel | López-García, Pedro | Pettorossi, Alberto | Proietti, Maurizio
Article Type: Other
DOI: 10.3233/FI-2020-1987
Citation: Fundamenta Informaticae, vol. 177, no. 3-4, pp. i-iii, 2020
Authors: Albert, Elvira | Bezirgiannis, Nikolaos | de Boer, Frank | Martin-Martin, Enrique
Article Type: Research Article
Abstract: We present a formal translation of a resource-aware extension of the Abstract Behavioral Specification (ABS) language to the functional language Haskell. ABS is an actor-based language tailored to the modeling of distributed systems. It combines asynchronous method calls with a suspend and resume mode of execution of the method invocations. To cater for the resulting cooperative scheduling of the method invocations of an actor, the translation exploits for the compilation of ABS methods Haskell functions with continuations. The main result of this article is a correctness proof of the translation by means of a simulation relation between a formal …semantics of the source language and a high-level operational semantics of the target language, i.e., a subset of Haskell. We further prove that the resource consumption of an ABS program extended with a cost model is preserved over this translation, as we establish an equivalence of the cost of executing the ABS program and its corresponding Haskell-translation. Concretely, the resources consumed by the original ABS program and those consumed by the Haskell program are the same, considering a cost model. Consequently, the resource bounds automatically inferred for ABS programs extended with a cost model, using resource analysis tools, are sound resource bounds also for the translated Haskell programs. Our experimental evaluation confirms the resource preservation over a set of benchmarks featuring different asymptotic costs. Show more
Keywords: actor model, futures, cooperative multitasking, coroutine, continuation, functional programming, operational semantics
DOI: 10.3233/FI-2020-1988
Citation: Fundamenta Informaticae, vol. 177, no. 3-4, pp. 203-234, 2020
Authors: Alpuente, María | Pardo, Daniel | Villanueva, Alicia
Article Type: Research Article
Abstract: In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KERNEL C, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KERNEL C in the 𝕂 semantic framework, we enrich the symbolic execution facilities recently provided by 𝕂 with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. …We implemented our technique in the automated tool KIND SPEC 2.1, which generates logical axioms that express pre- and post-condition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by 𝕂, some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our setting with little effort. Show more
Keywords: contract inference, symbolic execution, abstract subsumption, deductive verification
DOI: 10.3233/FI-2020-1989
Citation: Fundamenta Informaticae, vol. 177, no. 3-4, pp. 235-273, 2020
Authors: Bichler, Manuel | Morak, Michael | Woltran, Stefan
Article Type: Research Article
Abstract: State-of-the-art answer set programming (ASP) solvers rely on a program called a grounder to convert non-ground programs containing variables into variable-free, propositional programs. The size of this grounding depends heavily on the size of the non-ground rules, and thus, reducing the size of such rules is a promising approach to improve solving performance. To this end, in this paper we announce lpopt, a tool that decomposes large logic programming rules into smaller rules that are easier to handle for current solvers. The tool is specifically tailored to handle the standard syntax of the ASP language (ASP-Core) and makes it easier …for users to write efficient and intuitive ASP programs, which would otherwise often require significant handtuning by expert ASP engineers. It is based on an idea proposed by Morak and Woltran (2012) that we extend significantly in order to handle the full ASP syntax, including complex constructs like aggregates, weak constraints, and arithmetic expressions. We present the algorithm, the theoretical foundations on how to treat these constructs, as well as an experimental evaluation showing the viability of our approach. Show more
Keywords: Logic Programming, Answer Set Programming, Rule Decomposition, Tree Decomposition, Preprocessing
DOI: 10.3233/FI-2020-1990
Citation: Fundamenta Informaticae, vol. 177, no. 3-4, pp. 275-296, 2020
Authors: Alpuente, María | Cuenca-Ortega, Angel | Escobar, Santiago | Meseguer, José
Article Type: Research Article
Abstract: The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equational axioms. This paper generalizes the symbolic homeomorphic embedding relation to order–sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of different, increasingly efficient formulations of the homeomorphic embedding relation modulo axioms that we implement in Maude. Our experimental results show that the most efficient …version indeed pays off in practice. Show more
Keywords: homeomorphic embedding, rewriting logic, Maude
DOI: 10.3233/FI-2020-1991
Citation: Fundamenta Informaticae, vol. 177, no. 3-4, pp. 297-329, 2020
Authors: Falaschi, Moreno | Gabbrielli, Maurizio | Olarte, Carlos | Palamidessi, Catuscia
Article Type: Research Article
Abstract: Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. In this paper we define a dynamic slicer for CCP (and other language variants) and we show it to be a useful companion tool for the existing debugging techniques. We start with a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and …the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We show that this technique can be tailored to several variants of CCP, such as the timed language ntcc , linear CCP (an extension of CCPbased on linear logic where constraints can be consumed) and some extensions of CCP dealing with epistemic and spatial information. We also develop a prototypical implementation freely available for making experiments. Show more
Keywords: Concurrent Constraint Programming, Program slicing, Debugging
DOI: 10.3233/FI-2020-1992
Citation: Fundamenta Informaticae, vol. 177, no. 3-4, pp. 331-357, 2020
Authors: Mesnard, Fred | Payet, Étienne | Vidal, Germán
Article Type: Research Article
Abstract: Concolic testing is a well-known validation technique for imperative and object oriented programs. In a previous paper, we have introduced an adaptation of this technique to logic programming. At the heart of our framework lies a specific procedure that we call “selective unification”. It is used to generate appropriate run-time goals by considering all possible ways an atom can unify with the heads of some program clauses. In this paper, we show that the existing algorithm for selective unification is not complete in the presence of non-linear atoms. We then prove soundness and completeness for a restricted version of the …problem where some atoms are required to be linear. We also consider concolic testing in the context of constraint logic programming and extend the notion of selective unification accordingly. Show more
Keywords: Logic programming, Constraint logic programming, Concolic testing, Unification
DOI: 10.3233/FI-2020-1993
Citation: Fundamenta Informaticae, vol. 177, no. 3-4, pp. 359-383, 2020
Authors: Tarau, Paul
Article Type: Research Article
Abstract: Contrary to several other families of lambda terms, no closed formula or generating function is known and none of the sophisticated techniques devised in analytic combinatorics can currently help with counting or generating the set of simply-typed closed lambda terms of a given size. Moreover, their asymptotic scarcity among the set of closed lambda terms makes counting them via brute force generation and type inference quickly intractable, with previous published work showing counts for them only up to size 10. By taking advantage of the synergy between logic variables, unification with occurs check and efficient backtracking in …today’s Prolog systems, we climb 4 orders of magnitude above previously known counts by deriving progressively faster sequential Prolog programs that generate and/or count the set of closed simply-typed lambda terms of sizes up to 14. Similar counts for closed simply-typed normal forms are also derived up to size 14. Finally, we devise several parallel execution algorithms, based on generating code to be uniformly distributed among the available cores, that push the counts for simply typed terms up to size 15 and simply typed normal forms up to size 16. As a remarkable feature, our parallel algorithms are linearly scalable with the number of available cores. Show more
Keywords: logic programming transformations, type inference, simply-typed lambda terms and normal forms, sequential and parallel combinatorial generation algorithms, Prolog multi-threading
DOI: 10.3233/FI-2020-1994
Citation: Fundamenta Informaticae, vol. 177, no. 3-4, pp. 385-415, 2020
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
[email protected]
For editorial issues, like the status of your submitted paper or proposals, write to [email protected]
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
[email protected]
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office [email protected]
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
[email protected]
For editorial issues, like the status of your submitted paper or proposals, write to [email protected]
如果您在出版方面需要帮助或有任何建, 件至: [email protected]