571 citations
- Centre National de la Recherche ScientifiqueFR20 papers
- Center for MathematicaL studies and their ApplicationsFR7 papers
- Sorbonne UniversitéFR4 papers
- Institut national de recherche en sciences et technologies du numériqueFR3 papers
- Conditions Extrêmes et Matériaux Haute Température et IrradiationFR2 papers
- Institut de recherche mathématique de RennesFR2 papers
- Institut NéelFR2 papers
- Laboratoire RobervalFR2 papers
- Laboratoire Universitaire de Recherche en Production Automatisée2 papers
- Université de Technologie de CompiègneFR2 papers
- Université Joseph FourierFR2 papers
- Université Paris CitéFR2 papers
4 papers · 1 filter
Decomposition of Decidable First-Order Logics over Integers and Reals
Florent Bouchy, Alain Finkel, Jérôme Leroux
We tackle the issue of representing infinite sets of real- valued vectors. This paper introduces an operator for combining integer and real sets. Using this operator, we decompose…
Deciding security properties for cryptographic protocols. Application to key cycles
Hubert Comon-Lundh, Véronique Cortier, Eugen Zalinescu
There is a large amount of work dedicated to the formal verification of security protocols. In this paper, we revisit and extend the NP-complete decision procedure for a bounded nu…
LTL with the Freeze Quantifier and Register Automata
Stephane Demri, Ranko Lazic
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data…
On the freeze quantifier in Constraint LTL: decidability and complexity
Stéphane Demri, Ranko Lazic, David Nowak
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze q…