150 citations · 623 across the 65 of their papers we have counts for
8 papers · 1 filter
Dynamic Verification of SystemC with Statistical Model Checking
Van Chan Ngo, Axel Legay, Jean Quilbeuf
Many embedded and real-time systems have a inherent probabilistic behaviour (sensors data, unreliable hardware,...). In that context, it is crucial to evaluate system properties su…
Lightweight Monte Carlo Verification of Markov Decision Processes with Rewards
Axel Legay, Sean Sedwards, Louis-Marie Traonouez
Markov decision processes are useful models of concurrency optimisation problems, but are often intractable for exhaustive verification methods. Recent work has introduced lightwei…
Homotopy Bisimilarity for Higher-Dimensional Automata
Uli Fahrenberg, Axel Legay
We introduce a new category of higher-dimensional automata in which the morphisms are functional homotopy simulations, i.e. functional simulations up to concurrency of independent…
Smart Sampling for Lightweight Verification of Markov Decision Processes
Pedro D'Argenio, Axel Legay, Sean Sedwards +1
Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondetermi…
Compositionality for Quantitative Specifications
Uli Fahrenberg, Jan Křetínský, Axel Legay +1
We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive…
State Machine Flattening: Mapping Study and Assessment
Xavier Devroey, Gilles Perrouin, Maxime Cordy +3
State machine formalisms equipped with hierarchy and parallelism allow to compactly model complex system behaviours. Such models can then be transformed into executable code or inp…