Using an SGML Workbench for Digital Libraries (2009)
Jacques Ducloy, Crin Cnrs, Inria Lorraine
Traditionally, the entire information community was organized around a kernel of industrial companies where publishers played a very strategic role. This position was strengthened by two physical...
Pierre Alliez INRIA Sophia-Antipolis (2009)
Anisotropic Polygonal Remeshing, David Cohen-steiner, Olivier Devillers, Bruno Lévy, Inria Lorraine
Figure 1: From an input triangulated geometry, the curvature tensor field is estimated, then smoothed, and its umbilics are deduced (colored dots). Lines of curvatures (following the principal...
ABSTRACT Cluster-Based Interactive Volume Rendering with Simian (2008)
Christiaan Gribble, Xavier Cavin, Inria Lorraine
Commodity-based computer clusters offer a cost-effective alternative to traditional large-scale, tightly coupled computers as a means to provide high-performance computational and visualization...
Abstract Consider polynomials over GF(2). We define almost irreducible and almost primitive polynomials, explain why they are useful, and give some examples and conjectures relating to them. 2...
parXXL: A Fine Grained Development Environment on Coarse Grained Architectures (2008)
Jens Gustedt, Stéphane Vialle, Amelia De Vivo, Inria Lorraine
Abstract. We present a new integrated environment for cellular computing and other fine grained applications. It is based upon previous developments concerning cellular computing environments (the...
Forwarding control of scale model autonomous helicopter: (2008)
Inria Lorraine, Projet Conge, Isgmp Bat A, Robert E. Mahony
Abstract — A simple model of the dynamics of a scale model autonomous helicopter is considered. A stabilising control law is designed which guarantees the control inputs remain bounded by...
Toward the Integration of Numerical Computations into the OMSCS Framework (2008)
Jacques Calmet, Vincent Lefèvre, Inria Lorraine
Abstract. Computer algebra systems and automated theorem provers, which have complementary abilities, can be integrated to form an Open Mechanized Symbolic Computation System (OMSCS). This framework...
Almost Irreducible and Almost Primitive Trinomials \Lambda (2008)
Abstract Consider polynomials over GF(2). We define almost irreducible and almost primitive polynomials, explain why they are useful, and give some examples and conjectures relating to them. 2...
Universal Sets of n Points for 1-bend Drawings of Planar Graphs with n Vertices ⋆ (2008)
Hazel Everett, Sylvain Lazard, Stephen Wismath, Inria Lorraine
Abstract. This paper shows that any planar graph with n vertices can be point-set embedded with at most one bend per edge on a universal set of n points in the plane. An implication of this result is...
Stress-testing Control Structures for Dynamic Dispatch in Java (2008)
Olivier Zendra, Inria Lorraine, Loria Mcgill
Permission is granted for noncommercial reproduction of the work for educational or research purposes.
Eun-young Kang, Stephan Merz, Inria Lorraine
The date of receipt and acceptance will be inserted by the editor Abstract This article discusses a new format of predicate diagrams for the verification of real-time systems. We consider systems...
Thomas Bolander, Patrick Blackburn, Inria Lorraine, Rue Du, Jardin Botanique
Abstract. This article extends and improves work on tableau-based decision methods for hybrid logic by Bolander and Braüner [4]. Their paper gives tableau-based decision procedures for basic hybrid...
Isabelle Guérin Lassous, Jens Gustedt, Inria Lorraine
We present and analyze two portable algorithms for the List Ranking Problem in the Coarse Grained Multicomputer model (CGM). We report on implementations of these algorithms and experiments that were...
Language and Computation (2008)
Ville V. Nurmi, Dmitry Sustretov (eds, Amalia Todirascu, Raffaella Bernardi, Malvina Nissim, Judit Gervain, ...
School in Logic, Language and Information ever since it was held for the first time in 1996. The Student Session is a unique interdisciplinary forum for student researchers from around the world to...
Assefaw Hadish Gebremedhin, Jens Gustedt, Inria Lorraine, Isabelle Guérin Lassous, Jan Arne Telle
We present a new parallel computation model that enables the design of resource-optimal and scalable parallel algorithms and simplifies their analysis. The model rests on the following novel ideas:...
A Survey of Methods for Recovering Quadrics in Triangle Meshes SYLVAIN PETITJEAN (2008)
In a variety of practical situations such as reverse engineering of boundary representation from depth maps of scanned objects, range data analysis, model-based recognition and algebraic surface...
Yannick Toussaint, Inria Lorraine
We present the ILIAD project and its current results. ILIAD aims at combining statistic and linguistic approaches in order to analyse information in large documentary databases. The resulting...
Carlos Areces, Inria Lorraine, Balder Ten Cate
Hybrid languages are modal languages that have special symbols for naming individual states in models. Their history can be traced back to work of Arthur Prior in the fifties. The subject has...
Random Generation of Unlabelled Combinatorial Structures (2007)
Paul Zimmermann, Inria Lorraine
[summary by Eithne Murray] A systematic method for generating unlabelled combinatorial structures uniformly at random is presented. It applies to structures that are decomposable, i.e., formally...
Random Generation of Unlabelled Combinatorial Structures (2007)
Paul Zimmermann, Inria Lorraine
[summary by Eithne Murray] A systematic method for generating unlabelled combinatorial structures uniformly at random is presented. It applies to structures that are decomposable, i.e., formally...
Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution (2007)
Inria Lorraine, Kristoffer H. Rose
We present the oe a w-calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how oe a w can be used as a foundation of implementations of...
Uniform Random Generation for the Powerset Construction (2007)
Paul Zimmermann, Inria Lorraine
An algorithm for the uniform random generation of the powerset construction is presented, completing the calculus developed in [1] and [2], and its implementation in the Gaia system [7]. Given a...
Second Order Derivatives, Newton Method, Application to Shape Optimization (2007)
Arian Novruzi, Jean-rodolphe Roche, Cnrs Umr, Inria Lorraine, Projet Numath
.-- We describe a Newton method applied to the evaluation of a critical point of a total energy associated to a shape optimization problem. The key point of these methods is the Hessian of the shape...
Automated Verification by Induction and Associative-Commutative Operators (2007)
Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch, Inria Lorraine
Theories with associative and commutative (AC) operators, such as arithmetic, process algebras, boolean algebras, sets, : : : are ubiquitous in software and hardware verification. These AC operators...
Yannick Toussaint, Inria Lorraine
We present the ILIAD project and its current results. ILIAD aims at combining statistic and linguistic approaches in order to analyse information in large documentary databases. The resulting...
Yannick Toussaint, Inria Lorraine
We present the ILIAD project and its current results. ILIAD aims at combining statistic and linguistic approaches in order to analyse information in large documentary databases. The resulting...
Hybrid Logics are usually presented as an extension of modal logics where we can explicitly refer to the elements in the model. In this paper we will start by introducing hybrid logics from that...
Proof reconstruction for first-order logic and set-theoretical constructions (2006)
Clément Hurlin, Inria Sophia-antipolis, Amine Chaieb, Tjark Weber, Pascal Fontaine, ...
Proof reconstruction is a technique that combines an interactive theorem prover and an automatic one in a sound way, so that users benefit from the expressiveness of the first tool and the automation...
PRO: A Model for the Design and Analysis of Efficient and Scalable Parallel Algorithms (2005)
Mohamed Essaïdi, Isabelle Guérin Lassous, Jan Arne Telle, Assefaw Hadish Gebremedhin, Jens Gustedt, Inria Lorraine
We present a new parallel computation model called the Parallel Resource-Optimal computation model. PRO is a framework being proposed to enable the design of efficient and scalable parallel...
Truly on-the-fly LTL model checking (2005)
Moritz Hammer, Stephan Merz, Inria Lorraine
Abstract. We propose a novel algorithm for automata-based LTL model checking that interleaves the construction of the generalized Büchi automaton for the negation of the formula and the emptiness...
ABF++: fast and robust angle based flattening (2005)
Alla Sheffer, Bruno Lévy, Inria Lorraine, Maxim Mogilnitsky, Er Bogomyakov
Article Type Communicated by Submitted Revised (2005)
Olivier Devillers, Hazel Everett, Sylvain Lazard, Maria Pentcheva, Inria Lorraine, ...
We give a drawing of Kn in three dimensions in which vertices are placed at integer grid points and edges are drawn crossing-free with at most one bend per edge in a volume bounded by O(n 2.5).
A Local System for Intuitionistic Logic: Preliminary Results (2005)
This paper presents a system for intuitionistic logic in which all the rules are local, in the sense that, in applying the rules of the system, one needs only a fixed amount of information about the...
Master-Element Vector Irradiance for Large Tessellated Models, in "Graphite conf. proc (2005)
Grégory Lecot, Bruno Lévy, Laurent Alonso, Inria Lorraine, Inria Lorraine, Jean-claude Paul
Figure 1: Left: Master-Element global illumination applied to ”‘David” ’ (500K∆). Center: Isis model lighted with an area light (375K∆). Right: A scene with five data sets (1.5M∆). The...
ABF++: fast and robust angle based flattening (2005)
Alla Sheffer, Bruno Lévy, Inria Lorraine, Maxim Mogilnitsky, Alexander Bogomyakov
Conformal parameterization of mesh models has numerous applications in geometry processing. Conformality is desirable for remeshing, surface reconstruction, and many other mesh processing...
Mixing finite success and finite failure in an automated prover (2005)
Alwen Tiu, Gopalan Nadathur, Dale Miller, Inria Lorraine
Abstract. The operational semantics and typing of modern programming and specification languages are often defined using relations and proof systems. In simple settings, logic programming can be used...
Master-Element Vector Irradiance for Large Tessellated Models, in "Graphite conf. proc (2005)
Grégory Lecot, Bruno Lévy, Laurent Alonso, Inria Lorraine, Inria Lorraine, Jean-claude Paul
Figure 1: Left: Master-Element global illumination applied to ”‘David” ’ (500K∆). Center: Isis model lighted with an area light (375K∆). Right: A scene with five data sets (1.5M∆). The...
Article Type Communicated by Submitted Revised (2005)
Olivier Devillers, Hazel Everett, Sylvain Lazard, Maria Pentcheva, Inria Lorraine, ...
We give a drawing of Kn in three dimensions in which vertices are placed at integer grid points and edges are drawn crossing-free with at most one bend per edge in a volume bounded by O(n 2.5).
A Non-commutative Extension of Multiplicative Exponential Linear Logic (2004)
Alessio Guglielmi, Fakultät Informatik, Lutz Straßburger, Dresden Loria, ...
We extend multiplicative exponential linear logic (MELL) by a noncommutative, self-dual logical operator. The extended system, called NEL, is defined in the formalism of the calculus of structures,...
Refining Mobile UML State Machines (2004)
Stephan Merz, Martin Wirsing, Inria Lorraine
Abstract. We study the semantics and refinement of mobile objects, considering an extension of core UML state machines by primitives that designate the location of objects and their moves within a...
Refining Mobile UML State Machines (2004)
Stephan Merz, Martin Wirsing, Inria Lorraine
Abstract. We study the semantics and refinement of mobile objects, considering an extension of core UML state machines by primitives that designate the location of objects and their moves within a...
A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems (2003)
Stephan Merz, Martin Wirsing, Inria Lorraine
Abstract. We define a variant of Lamport’s Temporal Logic of Actions, extended by spatial modalities, that is intended for the specification of mobile systems with distributed state. We discuss...
Unions of non-disjoint theories and combinations of satisfiability procedures (2003)
Cesare Tinelli, Christophe Ringeissen, Inria Lorraine
In this paper we outline a theoretical framework for the combination of decision procedures for constraint satisfiability. We describe a general combination method which, given a procedure that...
Cluster-Based Interactive Volume (2003)
Rendering With Simian, Christiaan Gribble, Christiaan Gribble, Xavier Cavin, Xavier Cavin, Inria Lorraine, ...
Commodity-based computer clusters offer a cost-effective alternative to traditional largescale, tightly coupled computers as a means to provide high-performance computational and visualization...
A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems (2003)
Stephan Merz, Martin Wirsing, Inria Lorraine
Abstract. We define a variant of Lamport’s Temporal Logic of Actions, extended by spatial modalities, that is intended for the specification of mobile systems with distributed state. We discuss...
Stephan Merz, Inria Lorraine, S. Merz
TLA is a language intended for the high-level specification of reactive, distributed, and in particular asynchronous systems. Combining the linear-time temporal logic TLA and classical set-theory, it...
Factorization of a 512-bit RSA modulus (2000)
Stefania Cavallar, Bruce Dodson, Arjen K. Lenstra, Walter Lioen, Peter L, Brian Murphy, ...
This is a slightly abridged version of the paper which was originally submitted to
Factorization of a 512-bit RSA modulus (2000)
Stefania Cavallar, Arjenk. Lenstra, Peter L. Montgomery, Brian Murphy, Herman Te Riele, Karen Aardal, ...
Cs: a MuPAD package for counting and randomly generating combinatorial structures (1998)
Alain Denise, Isabelle Dutour, Paul Zimmermann, Inria Lorraine Loria, Inria Lorraine
We present a new computer algebra package which permits to count and to generate combinatorial structures of various types, provided that these structures can be described by a speci cation, as de...
Cs: a MuPAD package for counting and randomly generating combinatorial structures (1998)
Alain Denise, Isabelle Dutour, Paul Zimmermann, Inria Lorraine, Inria Lorraine
We present a new computer algebra package which permits to count and to generate combinatorial structures of various types, provided that these structures can be described by a specification, as...
Analysis of Engineering Drawings: State of the Art and Challenges (1997)
In this paper, we analyze the state of the art in interpretation of engineering drawings, both from a methodological point of view and from the perspective of the applications. We try to emphasize...
Automated Theorem Proving by Test Set Induction (1997)
Test set induction is a goal-directed proof technique which combines the full power of explicit induction and proof by consistency. It works by computing an appropriate explicit induction scheme...
Progress Report on Parallelism in MuPAD (1997)
Christian Heckler, Torsten Metzner, Paul Zimmermann, Inria Lorraine
MuPAD [8] is a general purpose computer algebra system with two programming concepts for parallel processing: micro-parallelism for shared-memory machines and macroparallelism for distributed...
Modeling sharing and recursion for weak reduction strategies using explicit substitution (1996)
Pierre Lescanne, Inria Lorraine, Kristoffer H. Rose, Kristoffer H. Rose
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent publications in the BRICS Report Series. Copies...
Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution (1996)
Pierre Lescanne, Kristoffer H. Rose, Inria Lorraine
We present the ...-calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how ... can be used as a foundation of implementations of functional...
Combining Unification and Built-In Constraints (Extended Abstract) (1996)
Farid Ajili, Claude Kirchner, Inria Lorraine
) Farid Ajili Claude Kirchner (Extended Abstract) INRIA Lorraine & CRIN 615 rue du jardin botanique BP 101 54602 Villers-l`es-Nancy Cedex, France email: fFarid.Ajili,Claude.Kirchnerg@loria.fr In...
Rough And Modal Algebras (1996)
Laurent Vigneron, Inria Lorraine, Anita Wasilewska
We have used here a theorem prover DATAC (D#duction Automatique dans des Th#ories Associatives et Commutatives) to discover, study and compare properties of rough and corresponding modal algebras....
Polynomial Factorization Challenges (1996)
Paul Zimmermann, Inria Lorraine, Laurent Bernardin, Michael Monagan
Joachim von zur Gathen has proposed a challenge for factoring univariate polynomials over finite fields to evaluate the practicability of current factorization algorithms ("A Factorization...
Structural and Syntactic Methods in Line Drawing Analysis: To which Extent do they Work? (1996)
this paper to structural and syntactic methods does of course in no ways mean that we despise or reject the statistical approach to pattern recognition. Actually, the complementarity of these two...
Using Induction and Rewriting to Verify and Complete Parameterized Specifications (1996)
In software engineering there is a growing demand for formal methods for the specification and validation of software systems. The formal development of a system might give rise to many proof...
Pierre Lescanne, Kristoffer H. Rose, Pierre Lescanne, Inria Lorraine, ...
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent...
Uniform random generation for the powerset construction (1995)
Paul Zimmermann, Inria Lorraine
[summary by Eithne Murray] An algorithm for the uniform random generation of the powerset construction is presented. Given a combinatorial class I, together with a counting procedure and an unranking...
Proofs, concurrent objects and computations in a FILL framework (1995)
D. Galmiche, E. Boudinet, Inria Lorraine
There are several major approaches to model concurrent computations using logic. In this context, one aim can be to achieve different forms of programming as logic, object-oriented or concurrent ones...
Adel Bouhoula, Michaël Rusinowitch, Inria Lorraine
The SPIKE system is an automatic theorem prover in theories presented by conditional equations. SPIKE was written in Caml Light, a functional language of the ML family. The program is provided with a...
On the Reduction of Chocs Bisimulation to π-calculus Bisimulation (1995)
Calculus Bisimulation, Roberto M. Amadio, Inria Lorraine
Chocs and ß-calculus are two extensions of CCS where, respectively, processes and channels are transmissible values. In previous work we have proposed a formalization of the notion of bisimulation...
December Spike, Adel Bouhoula, Inria Lorraine
The SPIKE system is an automatic theorem prover in theories presented by conditional equations. SPIKE was written in Caml Light c fl , a functional language of the ML c fl family. The program is...
The Complexity and Enumerative Geometry of Aspect Graphs of Smooth Surfaces (1994)
Sylvain Petitjean, Inria Lorraine
Aspect graphs have been the object of very active research by the computer vision community in recent years, but most of it has concentrated on the design of algorithms to compute the representation....
Automating the Construction of Stationary Multiple-Point Classes (1994)
Sylvain Petitjean, Inria Lorraine
In this paper, we describe an algorithm to compute arbitrary stationary multiple-point formulas. We report its full implementation in Maple and show some examples matching formulas found by hand...
Improving the Efficiency of AC Matching and Unification (1993)
Inria Lorraine, Steven M. Eker, Steven M. Eker, Steven M. Eker
This report consists of three independent parts that each study important steps in the matching and unification process for AC theories. In the first part we consider the problem of AC matching where...
A Procedure for Automatic Proof Nets Construction (1992)
Didier Galmiche, Guy Perrier, Crin Cnrs, Inria Lorraine
. In this paper, we consider the multiplicative fragment of linear logic (MLL) from an automated deduction point of view. Before to use this new logic to make logic programming or to program with...
Solving Systems of Linear Diophantine Equations: An Algebraic Approach (1991)
Eric Domenjoud, Inria Lorraine
We describe through an algebraic and geometrical study, a new method for solving systems of linear diophantine equations. This approach yields an algorithm which is intrinsically parallel. In...