30 citations
Counting papers with at most 25 authors, so collaboration author lists do not stand in for the people here.
- Max Planck Institute for InformaticsDE8 papers
- Centre National de la Recherche ScientifiqueFR7 papers
- Université de LorraineFR7 papers
- Institut national de recherche en sciences et technologies du numériqueFR5 papers
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR5 papers
- Laboratoire d'Informatique de Paris-NordFR4 papers
- Saarland UniversityDE4 papers
- Université de MontpellierFR3 papers
- Université Sorbonne Paris NordFR3 papers
- Laboratoire des Sciences du Numérique de NantesFR2 papers
- National Institute of InformaticsJP2 papers
- Université Paris-SaclayFR2 papers
21 papers
Guaranteeing Timed Opacity using Parametric Timed Model Checking
Étienne André, Didier Lime, Dylan Marinho +1
Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage occurs whenever an attacker successfully ded…
Offline and online energy-efficient monitoring of scattered uncertain logs using a bounding model
Bineet Ghosh, Étienne André
Monitoring the correctness of distributed cyber-physical systems is essential. Detecting possible safety violations can be hard when some samples are uncertain or missing. We monit…
ODEbase: A Repository of ODE Systems for Systems Biology
Christoph Lüders, Thomas Sturm, Ovidiu Radulescu
Recently, symbolic computation and computer algebra systems have been successfully applied in systems biology, especially in chemical reaction network theory. One advantage of symb…
Parametric schedulability analysis of a launcher flight control system under reactivity constraints
Étienne André, Emmanuel Coquard, Laurent Fribourg +2
The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a…
Robust optimal periodic control using guaranteed Euler's method
Jawher Jerray, Laurent Fribourg, Étienne André
In this paper, we consider the application of optimal periodic control sequences to switched dynamical systems. The control sequence is obtained using a finite-horizon optimal meth…
Superposition for Lambda-Free Higher-Order Logic
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes +1
We introduce refutationally complete superposition calculi for intentional and extensional clausal -free higher-order logic, two formalisms that allow partial application and ap…
Reachability and liveness in parametric timed automata
Étienne André, Didier Lime, Olivier H. Roux
We study timed systems in which some timing features are unknown parameters. Parametric timed automata (PTAs) are a classical formalism for such systems but for which most interest…
SCL with Theory Constraints
Martin Bromberger, Alberto Fiori, Christoph Weidenbach
We lift the SCL calculus for first-order logic without equality to the SCL(T) calculus for first-order logic without equality modulo a background theory. In a nutshell, the SCL(T)…
A Linear Algebra Approach for Detecting Binomiality of Steady State Ideals of Reversible Chemical Reaction Networks
Hamid Rahkooy, Ovidiu Radulescu, Thomas Sturm
Motivated by problems from Chemical Reaction Network Theory, we investigate whether steady state ideals of reversible reaction networks are generated by binomials. We take an algeb…
Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks
R. Bradford, J. H. Davenport, M. England +8
We consider a problem from biological network analysis of determining regions in a parameter space over which there are multiple steady states for positive real values of variables…
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
Ran Chen, Cyril Cohen, Jean-Jacques Levy +2
Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from gr…
Explicit Modelling of Physical Measures: From Event-B to Java
J Paul Gibson, Dominique Méry
The increasing development of cyber-physical systems (CPSs) requires modellers to represent and reason about physical values. This paper addresses two major, inter-related, aspects…
Proceedings Joint Workshop on Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD)
Régine Laleau, Dominique Méry, Shin Nakajima +1
This volume contains the joint proceedings of IMPEX 2017, the first workshop on Handling IMPlicit and EXplicit knowledge in formal system development and FM&MDD, the second worksho…
Auxiliary Variables in TLA+
Leslie Lamport, Stephan Merz
Auxiliary variables are often needed for verifying that an implementation is correct with respect to a higher-level specification. They augment the formal description of the implem…
Extending Nunchaku to Dependent Type Theory
Simon Cruanes, Jasmin Christian Blanchette
Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitp…
Encoding TLA+ set theory into many-sorted first-order logic
Stephan Merz, Hernán Vanzetto
We present an encoding of Zermelo-Fraenkel set theory into many-sorted first-order logic, the input language of state-of-the-art SMT solvers. This translation is the main component…
Proceedings Second International Workshop on Formal Integrated Development Environment
Catherine Dubois, Paolo Masci, Dominique Méry
This volume contains the proceedings of F-IDE 2015, the second international workshop on Formal Integrated Development Environment, which was held as an FM 2015 satellite event, on…
Linear Integer Arithmetic Revisited
Martin Bromberger, Thomas Sturm, Christoph Weidenbach
We consider feasibility of linear integer programs in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer programs…
Better Answers to Real Questions
Marek Kosta, Thomas Sturm, Andreas Dolzmann
We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which a…
Subtropical Real Root Finding
Thomas Sturm
We describe a new incomplete but terminating method for real root finding for large multivariate polynomials. We take an abstract view of the polynomial as the set of exponent vect…
Bernays-Schoenfinkel-Ramsey with Simple Bounds is NEXPTIME-complete
Marco Voigt, Christoph Weidenbach
First-order predicate logic extended with linear arithmetic is undecidable, in general. We show that the Bernays-Schönfinkel-Ramsey (BSR) fragment extended with linear arithmetic r…