Search

Your search keyword '"Cirstea, Horatiu"' showing total 134 results
Start Over Author "Cirstea, Horatiu"

Refine your results

more »

more »

more »

more »
134 results on '"Cirstea, Horatiu"'

1. Validating Traces of Distributed Programs Against TLA+ Specifications

Author

Cirstea, Horatiu, Kuppe, Markus A., Loillier, Benjamin, and Merz, Stephan

Subjects
Computer Science - Programming Languages, Computer Science - Software Engineering
Abstract

TLA+ is a formal language for specifying systems, including distributed algorithms, that is supported by powerful verification tools. In this work we present a framework for relating traces of distributed programs to high-level specifications written in TLA+. The problem is reduced to a constrained model checking problem, realized using the TLC model checker. Our framework consists of an API for instrumenting Java programs in order to record traces of executions, of a collection of TLA+ operators that are used for relating those traces to specifications, and of scripts for running the model checker. Crucially, traces only contain updates to specification variables rather than full values, and developers may choose to trace only certain variables. We have applied our approach to several distributed programs, detecting discrepancies between the specifications and the implementations in all cases. We discuss reasons for these discrepancies, best practices for instrumenting programs, and how to interpret the verdict produced by TLC.

Published
2024

2. Validating Traces of Distributed Programs Against TLA+ Specifications

Author

Cirstea, Horatiu, Kuppe, Markus A., Loillier, Benjamin, Merz, Stephan, Goos, Gerhard, Series Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Madeira, Alexandre, editor, and Knapp, Alexander, editor

Published
2025
Full Text
View/download PDF

3. Extending PlusCal for Modeling Distributed Algorithms

Author

Cirstea, Horatiu, Merz, Stephan, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Herber, Paula, editor, and Wijs, Anton, editor

Published
2024
Full Text
View/download PDF

5. Generating Distributed Programs from Event-B Models

Author

Cirstea, Horatiu, Grall, Alexis, and Méry, Dominique

Subjects
Computer Science - Programming Languages, Computer Science - Logic in Computer Science
Abstract

Distributed algorithms offer challenges in checking that they meet their specifications. Verification techniques can be extended to deal with the verification of safety properties of distributed algorithms. In this paper, we present an approach for combining correct-by-construction approaches and transformations of formal models (Event-B) into programs (DistAlgo) to address the design of verified distributed programs. We define a subset LB (Local Event-B) of the Event-B modelling language restricted to events modelling the classical actions of distributed programs as internal or local computations, sending messages and receiving messages. We define then transformations of the various elements of the LB language into DistAlgo programs. The general methodology consists in starting from a statement of the problem to program and then progressively producing an LB model obtained after several refinement steps of the initial LB model. The derivation of the LB model is not described in the current paper and has already been addressed in other works. The transformation of LB models into DistAlgo programs is illustrated through a simple example. The refinement process and the soundness of the transformation allow one to produce correct-by-construction distributed programs., Comment: In Proceedings VPT/HCVS 2020, arXiv:2008.02483

Published
2020
Full Text
View/download PDF

6. Generic Encodings of Constructor Rewriting Systems

Author

Cirstea, Horatiu and Moreau, Pierre-Etienne

Subjects
Computer Science - Logic in Computer Science, Computer Science - Computation and Language, Computer Science - Programming Languages
Abstract

Rewriting is a formalism widely used in computer science and mathematical logic. The classical formalism has been extended, in the context of functional languages, with an order over the rules and, in the context of rewrite based languages, with the negation over patterns. We propose in this paper a concise and clear algorithm computing the difference over patterns which can be used to define generic encodings of constructor term rewriting systems with negation and order into classical term rewriting systems. As a direct consequence, established methods used for term rewriting systems can be applied to analyze properties of the extended systems. The approach can also be seen as a generic compiler which targets any language providing basic pattern matching primitives. The formalism provides also a new method for deciding if a set of patterns subsumes a given pattern and thus, for checking the presence of useless patterns or the completeness of a set of patterns., Comment: Added appendix with proofs and extended examples

Published
2019

7. Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation

Author

Cirstea, Horatiu and Sabel, David

Subjects
Computer Science - Logic in Computer Science, Computer Science - Programming Languages
Abstract

This volume contains the formal proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017), held on 8th September 2017 in Oxford, United Kingdom, and affiliated with the Second International Conference on Formal Structures for Computation and Deduction (FSCD 2017).

Published
2018
Full Text
View/download PDF

8. Faithful (meta-)encodings of programmable strategies into term rewriting systems

Author

Cirstea, Horatiu, Lenglet, Serguei, and Moreau, Pierre-Etienne

Subjects
Computer Science - Programming Languages, F.4
Abstract

Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and rewriting strategies are used to con- trol their application. The operational semantics of these strategies are generally accepted and approaches for analyzing the termination of specific strategies have been studied. We propose in this paper a generic encoding of classic control and traversal strategies used in rewrite based languages such as Maude, Stratego and Tom into a plain term rewriting system. The encoding is proven sound and complete and, as a direct consequence, estab- lished termination methods used for term rewriting systems can be applied to analyze the termination of strategy controlled term rewriting systems. We show that the encoding of strategies into term rewriting systems can be easily adapted to handle many-sorted signa- tures and we use a meta-level representation of terms to reduce the size of the encodings. The corresponding implementation in Tom generates term rewriting systems compatible with the syntax of termination tools such as AProVE and TTT2, tools which turned out to be very effective in (dis)proving the termination of the generated term rewriting systems. The approach can also be seen as a generic strategy compiler which can be integrated into languages providing pattern matching primitives; experiments in Tom show that applying our encoding leads to performances comparable to the native Tom strategies.

Published
2017
Full Text
View/download PDF

9. Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation

Author

Cirstea, Horatiu and Escobar, Santiago

Subjects
Computer Science - Programming Languages, Computer Science - Logic in Computer Science
Abstract

This volume contains the formal proceedings of the Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), held on 23rd June 2016 in Porto, Portugal, as a satellite event of the First International Conference on Formal Structures for Computation and Deduction (FSCD 2016). The workshop brought together researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area., Comment: Dedicated to the memory of Kristoffer H. Rose

Published
2017
Full Text
View/download PDF

10. Pattern Eliminating Transformations

Author

Cirstea, Horatiu, Lermusiaux, Pierre, Moreau, Pierre-Etienne, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Fernández, Maribel, editor

Published
2021
Full Text
View/download PDF

12. Extensional and Intensional Strategies

Author

Bourdier, Tony, Cirstea, Horatiu, Dougherty, Daniel, and Kirchner, Hélène

Subjects
Computer Science - Computer Science and Game Theory, Computer Science - Logic in Computer Science, Computer Science - Programming Languages, F.3.3, I.2.8
Abstract

This paper is a contribution to the theoretical foundations of strategies. We first present a general definition of abstract strategies which is extensional in the sense that a strategy is defined explicitly as a set of derivations of an abstract reduction system. We then move to a more intensional definition supporting the abstract view but more operational in the sense that it describes a means for determining such a set. We characterize the class of extensional strategies that can be defined intensionally. We also give some hints towards a logical characterization of intensional strategies and propose a few challenging perspectives.

Published
2010
Full Text
View/download PDF

14. Rewriting Calculus: Foundations and Applications

Author

Cirstea, Horatiu

Subjects
Computer Science - Symbolic Computation, Computer Science - Logic in Computer Science, Computer Science - Programming Languages, I.1, D.1, D.3, F.4.0, F.4.1
Abstract

This thesis is devoted to the study of a calculus that describes the application of conditional rewriting rules and the obtained results at the same level of representation. We introduce the rewriting calculus, also called the rho-calculus, which generalizes the first order term rewriting and lambda-calculus, and makes possible the representation of the non-determinism. In our approach the abstraction operator as well as the application operator are objects of calculus. The result of a reduction in the rewriting calculus is either an empty set representing the application failure, or a singleton representing a deterministic result, or a set having several elements representing a not-deterministic choice of results. In this thesis we concentrate on the properties of the rewriting calculus where a syntactic matching is used in order to bind the variables to their current values. We define evaluation strategies ensuring the confluence of the calculus and we show that these strategies become trivial for restrictions of the general rewriting calculus to simpler calculi like the lambda-calculus. The rewriting calculus is not terminating in the untyped case but the strong normalization is obtained for the simply typed calculus. In the rewriting calculus extended with an operator allowing to test the application failure we define terms representing innermost and outermost normalizations with respect to a set of rewriting rules. By using these terms, we obtain a natural and concise description of the conditional rewriting. Finally, starting from the representation of the conditional rewriting rules, we show how the rewriting calculus can be used to give a semantics to ELAN, a language based on the application of rewriting rules controlled by strategies., Comment: PhD Thesis in French

Published
2000

16. Formal Specification and Validation of Security Policies

Author

Bourdier, Tony, Cirstea, Horatiu, Jaume, Mathieu, Kirchner, Hélène, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Garcia-Alfaro, Joaquin, editor, and Lafourcade, Pascal, editor

Published
2012
Full Text
View/download PDF

17. TomML: A Rule Language for Structured Data

Author

Cirstea, Horatiu, Moreau, Pierre-Etienne, Reilles, Antoine, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Governatori, Guido, editor, Hall, John, editor, and Paschke, Adrian, editor

Published
2009
Full Text
View/download PDF

18. Confluence of Pattern-Based Calculi

Author

Cirstea, Horatiu, Faure, Germain, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Baader, Franz, editor

Published
2007
Full Text
View/download PDF

19. Rewriting Calculus with Fixpoints: Untyped and First-Order Systems

Author

Cirstea, Horatiu, Liquori, Luigi, Wack, Benjamin, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Berardi, Stefano, editor, Coppo, Mario, editor, and Damiani, Ferruccio, editor

Published
2004
Full Text
View/download PDF

20. The Rho Cube

Author

Cirstea, Horatiu, Kirchner, Claude, Liquori, Luigi, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Honsell, Furio, editor, and Miculan, Marino, editor

Published
2001
Full Text
View/download PDF

22. Matching Power

Author

Cirstea, Horatiu, Kirchner, Claude, Liquori, Luigi, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, and Middeldorp, Aart, editor

Published
2001
Full Text
View/download PDF

26. An Extension of PlusCal for Modeling Distributed Algorithms

Author

Alkayed, Heba, Cirstea, Horatiu, Merz, Stephan, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Merz, Stephan, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; The PlusCal language combines the expressive power of TLA+ with the “look and feel” of imperative pseudo-code in order to allow users to express algorithms at a high level of abstraction. PlusCal algorithms are translated to TLA+ specifications and can be formally verified using the TLA+ Toolbox. We propose a small extension of PlusCal, tentatively called Distributed PlusCal, intended for simplifying the presentation of distributed algorithms in PlusCal.Distributed systems consist of nodes that communicate by message passing. It is convenient to model a node as running several threads that share local memory. For example, one thread may execute the main algorithm, while a separate thread listens for incoming messages. Although PlusCal offers processes, they have a single thread of execution. Different threads of the same node must therefore be modeled as individual processes, and variables representing the local memory of a node must be declared as global variables, obscuring the structure of the code. Our first extension allows a PlusCal process to have several code blocks that execute in parallel. Besides, Distributed PlusCal explicitly identifies variables representing communication channels and introduces associated send and receive operations. In contrast to using ordinary variables and writing macros or operator definitions for channel operations, making channels part of the language gives us some more flexibility in the TLA+ translation.

Published
2020

36. Matching Power

Author

Cirstea, Horatiu, primary, Kirchner, Claude, additional, and Liquori, Luigi, additional

Published
2001
Full Text
View/download PDF

43. A Java Framework for Test Data Generation

Author

Cirstea, Horatiu, Moreau, Pierre-Etienne, Balland, Emilie, Cirstea, Horatiu, Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), Programming Language Technology For Communication Services (Phoenix), Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] (EA4136), UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)-Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] (EA4136), and UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]

Subjects
[INFO]Computer Science [cs], [INFO] Computer Science [cs]
Published
2015

46. Towards an automatic tool for multi-scale model derivation

Author

Belkhir, Walid, Ratier, Nicolas, Nguyen, Duy Duc, Yang, Bin, Lenczner, Michel, Zamkotsian, Frédéric, Cirstea, Horatiu, Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC), Laboratoire d'Astrophysique de Marseille (LAM), Aix Marseille Université (AMU)-Institut national des sciences de l'Univers (INSU - CNRS)-Centre National d'Études Spatiales [Toulouse] (CNES)-Centre National de la Recherche Scientifique (CNRS), Formal islands: foundations and applications (PAREO), Inria Nancy - Grand Est, Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), and Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS]
Abstract

This paper reports recent advances in the development of a symbolic asymptotic mod-eling software package, called MEMSALab, which will be used for automatic generation of asymptotic models for arrays of micro and nanosystems. More precisely, a model is a partial differential equation and an asymptotic method approximate it by another partial differential equation which can be numerically simulated in a reasonable time. The challenge consists in taking into account a wide range of different physical features and geometries e.g. thin structures, periodic structures, multiple nested scales etc. The main purpose of this software is to construct models incrementally so that model features can be included step by step. This idea, conceptualized under the name "by-extension-combination", is presented in detail for the first time.

Published
2015

47. A faithful encoding of programmable strategies into term rewriting systems

Author

Cirstea, Horatiu, Lenglet, Serguei, Moreau, Pierre-Etienne, Formal islands: foundations and applications (PAREO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Lenglet, Sergueï

Subjects
000 Computer science, knowledge, general works, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-IR]Computer Science [cs]/Information Retrieval [cs.IR], Computer Science, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing
Abstract

International audience; Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and declarative rewriting strategies are used to control their application. The operational semantics of these strategies are generally accepted and approaches for analyzing the termination of specific strategies have been studied. We propose in this paper a generic encoding of classic control and traversal strategies used in rewrite based languages such as Maude, Stratego and Tom into a plain term rewriting system. The encoding is proven sound and complete and, as a direct consequence, established termination methods used for term rewriting systems can be applied to analyze the termination of strategy controlled term rewriting systems. The corresponding implementation in Tom generates term rewriting systems compatible with the syntax of termination tools such as AProVE and TTT2, tools which turned out to be very effective in (dis)proving the termination of the generated term rewriting systems. The approach can also be seen as a generic strategy compiler which can be integrated into languages providing pattern matching primitives; this has been experimented for Tom and performances comparable to the native Tom strategies have been observed. 1998 ACM Subject Classification F.4 Mathematical Logic and Formal Languages

Published
2015
Full Text
View/download PDF

48. Bringing Strategic Rewriting into the Mainstream

Author

Balland, Emilie, Cirstea, Horatiu, Moreau, Pierre-Etienne, Programming Language Technology For Communication Services (Phoenix), Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] (EA4136), UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Formal islands: foundations and applications (PAREO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)-Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] (EA4136), UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2], Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Moreau, Pierre-Etienne

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], pattern matching, strategies, term rewriting, object-oriented programming, tree traversal, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Abstract

Developing programming paradigms and languages that ease the program-mers' job of writing quality reusable code have been central ever since the beginning of programming. Tom, the language presented here, has been developed in an attempt to make a step forward in this direction. It promotes term rewriting techniques piggybacked on top of a general-purpose programming language like Java, C, and Python. This results in concise pieces of code which are close to the targeted application domain and which can be reasoned about using effective theoretical and practical tools. This approach has been validated on a variety of concrete applications ranging from academic tools like theorem provers, to large and complex applications, including the Tom compiler itself and several industrial products. This paper presents an overview of the current version of the language and explains the design rationale, browses the application domains and gives some hints on the tool building.

Published
2015

49. Le calcul de réécriture

Author

Cirstea, Horatiu, Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Université Nancy II, Furio Honsell, and Cirstea, Horatiu

Subjects
langages déclaratifs, [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], stratégies, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], lambda calcul, réécriture
Abstract

Le manuscrit présente une partie des travaux de recherche que j'ai effectués au cours des dix dernières années. Je me suis focalisé en particulier sur la présentation du calcul de réécriture comme un formalisme théorique permettant de donner la sémantique dynamique et statique de toute une famille de langages basés sur le filtrage, les règles et les stratégies de réécriture. Je présente le calcul de réécriture général ainsi que plusieurs instances et extensions, en mettant l'accent sur l'expressivité et sur les propriétés de ces calculs. Je montre en particulier que l'intégration uniforme des mécanismes de bases de la réécriture et du lambda-calcul permet une définition précise du processus de réécriture sous des stratégies ainsi que des encodages, typés ou non, de différents formalismes similaires. Je présente dans ce manuscrit des systèmes de types développés dans l'optique d'un formalisme théorique pour le typage dans des langages de programmation à base de règles et je ne discute que brièvement les systèmes de types dépendants étudiés dans une perspective logique. Le filtrage et l'application de substitutions obtenues comme résultat sont des opérations réalisées au niveau méta du calcul de réécriture mais une version explicite permet leur manipulation modulaire et efficace au niveau objet du calcul. Cette version explicite du calcul est étendue avec des structure de graphe permettant de représenter explicitement le partage et les cycles. Je propose également un formalisme général permettant d'exprimer différents calculs à motif et une méthodologie qui met en évidence les points clés permettant d'obtenir la confluence de ces calculs.

Published
2010

50. A faithful encoding of programmable strategies into term rewriting systems

Author

Horatiu Cirstea and Serguei Lenglet and Pierre-Etienne Moreau, Cirstea, Horatiu, Lenglet, Serguei, Moreau, Pierre-Etienne, Horatiu Cirstea and Serguei Lenglet and Pierre-Etienne Moreau, Cirstea, Horatiu, Lenglet, Serguei, and Moreau, Pierre-Etienne

Abstract

Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and declarative rewriting strategies are used to control their application. The operational semantics of these strategies are generally accepted and approaches for analyzing the termination of specific strategies have been studied. We propose in this paper a generic encoding of classic control and traversal strategies used in rewrite based languages such as Maude, Stratego and Tom into a plain term rewriting system. The encoding is proven sound and complete and, as a direct consequence, established termination methods used for term rewriting systems can be applied to analyze the termination of strategy controlled term rewriting systems. The corresponding implementation in Tom generates term rewriting systems compatible with the syntax of termination tools such as AAProVE and TTT2, tools which turned out to be very effective in (dis)proving the termination of the generated term rewriting systems. The approach can also be seen as a generic strategy compiler which can be integrated into languages providing pattern matching primitives; this has been experimented for Tom and performances comparable to the native Tom strategies have been observed.

Published
2015
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results