211 citations
- Université Grenoble AlpesFR49 papers
- Centre National de la Recherche ScientifiqueFR44 papers
- Institut polytechnique de GrenobleFR12 papers
- Université Joseph FourierFR7 papers
- FortissDE4 papers
- Institut des langues et cultures d'Europe, Amérique, Afrique, Asie et AustralieFR4 papers
- Institut national de recherche en sciences et technologies du numériqueFR4 papers
- Aalto UniversityFI3 papers
- Commissariat à l'Énergie Atomique et aux Énergies AlternativesFR3 papers
- École Polytechnique Fédérale de LausanneCH3 papers
- Laboratoire d'Informatique de GrenobleFR3 papers
- LIP6FR3 papers
7 papers · 1 filter
Fast and exact analysis for LRU caches
Claire Maïza, Valentin Touzeau, David Monniaux +1
For applications in worst-case execution time analysis and in security, it is desirable to statically classify memory accesses into those that result in cache hits, and those that…
First Order Alternation
Radu Iosif, Xiao Xu
We introduce first order alternating automata, a generalization of boolean alternating automata, in which transition rules are described by multisorted first order formulae, with s…
On the Monitoring of Decentralized Specifications Semantics, Properties, Analysis, and Simulation
Antoine El-Hokayem, Yliès Falcone
We define two complementary approaches to monitor decentralized systems. The first relies on those with a centralized specification, i.e, when the specification is written for the…
System Design in the Era of IoT --- Meeting the Autonomy Challenge
Joseph Sifakis
The advent of IoT is a great opportunity to reinvigorate Computing by focusing on autonomous system design. This certainly raises technology questions but, more importantly, it req…
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
Mnacho Echenim, Radu Iosif, Nicolas Peltier
This paper investigates the satisfiability problem for Separation Logic, with unrestricted nesting of separating conjunctions and implications, for prenex formulae with quantifier…
Certified Roundoff Error Bounds using Bernstein Expansions and Sparse Krivine-Stengle Representations
Victor Magron, Alexandre Rocca, Thao Dang
Floating point error is a drawback of embedded systems implementation that is difficult to avoid. Computing rigorous upper bounds of roundoff errors is absolutely necessary for the…