Publications

( dblp, google scholar)

  • Thèse

    • Modular Specification and Compositional Analysis of Stochastic Systems
      PhD Thesis, Ecole doctorale MATISSE, Université de Rennes 1, IRISA. Octobre 2010 (.pdf, .bib).
  • Journaux

    • A. Nouri, S. Bensalem, M. Bozga, B. Delahaye, C. Jégourel, A. Legay. Statistical Model Checking QoS Properties of Systems with SBIP.
      In Software Tools for Technology Transfer, Vol 17, Num. 2, pp. 171-185, 2015.(.pdf, .bib)

    • B. Delahaye, U. Fahrenberg, K.G. Larsen, A. Legay. Refinement and Difference for Probabilistic Automata.
      In Logical Methods in Computer Science, Vol 10, Num. 3, 2014.(.pdf, .bib)

    • B. Delahaye, K.G. Larsen, A. Legay. Stuttering for Abstract Probabilistic Automata.
      In Journal of Logic and Algebraic Programming, Vol 85, Num. 1, pp. 1-19, 2014.(.pdf, .bib)

    • B. Delahaye, J.-P. Katoen, K.G. Larsen, A. Legay, M.L. Pedersen, F. Sher, A. Wasowski. Abstract Probabilistic Automata.
      In Information and Computation, Vol 232, pp. 66-116, 2013.(.pdf, .bib)

    • B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wasowski. New results for Constraint Markov Chains.
      In Performance EVAluation, Vol 69, Num. 7-8, pp. 379-401, 2012. (.pdf, .bib)

    • B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wasowski. Consistency and Refinement for Interval Markov Chains.
      In Journal of Logic and Algebraic Programming, Vol 81, Num. 3, pp. 209-226, 2012. (.pdf, .bib)

    • A. Basu, S.Bensalem, M.Bozga, B. Delahaye, A. Legay. Statistical abstraction and model-checking of large heterogeneous systems.
      In International Journal on Software Tools for Technology Transfer (STTT), Vol 14, Num. 1, pp. 53-72, 2012. (.pdf, .bib)

    • B. Caillaud, B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wasowski. Constraint Markov Chains
      In Theoretical Computer Science, Vol 412, Num. 34, pp. 4373-4404, 2011. (.pdf, .bib)

    • B. Delahaye, B. Caillaud, A. Legay. Probabilistic Contracts: A Compositional Reasoning Methodology for the Design of Systems with Stochastic and/or non-Deterministic Aspects
      In Formal Methods in System Design, Vol. 38, Num. 1, pp. 1-32, 2011. (.pdf, .bib)
  • Conférences

    • A. Bart, B. Delahaye, D. Lime, E. Monfroy, C. Truchet. Reachability in Parametric Interval Markov Chains using Constraints,
      In QEST, 14th International Conference on Quantitative Evaluation of SysTems, Berlin, Germany, 2017 -- accepted for publication. (.pdf,.bib)

    • M.A. Aouadhi, B. Delahaye, A. Lanoix. Moving from Event-B to Probabilistic Event-B,
      In SAC, 32nd ACM Symposium on Applied Computing -- Software Verification and Testing track, Marrakech, Morocco, 2017 -- accepted for publication. (.pdf,.bib)

    • Y. Emzivat, B. Delahaye, D. Lime, O.H. Roux. Probabilistic Time Petri Nets,
      In PETRI NETS, 37th International Conference on Application and Theory of Petri Nets and Concurrency, Toru{\'{n}}, Poland, 2016. (.pdf,.bib)

    • E. André, B. Delahaye. Consistency in Parametric Interval Probabilistic Timed Automata,
      In TIME, 23rd International Symposium on Temporal Representation and Reasoning, Kongens Lyngby, Denmark, 2016. (.pdf,.bib)

    • B. Delahaye, D. Lime, L. Petrucci. Parameter Synthesis for Parametric Interval Markov Chains,
      In VMCAI, 17th International Conference on Verification, Model Checking and Abstract Interpretation, St Petersburg, Florida, United States, 2016. (.pdf,.bib,long)

    • B. Delahaye, J.L. Fiadeiro, A. Legay, A. Lopes. Heterogeneous Timed Machines,
      In ICTAC, 11th International Colloquium on Theoretical Aspects of Computing, Bucharest, Romania, 2014.(.pdf,.bib)

    • N. Benes, B. Delahaye, U. Fahrenberg, J. Kretínský, A. Legay. Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory.
      In CONCUR, 24th international conference on Concurrency Theory, Buenos Aires, Argentina, 2013. (.pdf,.bib)

    • B. Delahaye, U. Fahrenberg, K.G. Larsen, A. Legay Refinement and Difference for Probabilistic Automata.
      In QEST, 9th International Conference on Quantitative Evaluation of SysTems , Buenos Aires, Argentina, 2013. (.pdf,.bib,long)

    • B. Delahaye, J. L. Fiadeiro, A. Legay, A. Lopes A Timed Component Algebra for Services.
      In FMOODS/FORTE, 8th International Federated Conference on Distributed Computing Techniques , Florence, Italy, 2013. (.pdf,.bib)

    • B. Delahaye, K.G. Larsen, A. Legay Stuttering for Abstract Probabilistic Automata.
      In LFCS, Symposium on Logical Foundations of Computer Science, San Diego, California, USA, 2013 (to appear). (.pdf,.bib,long)

    • S.Bensalem, M.Bozga, B.Delahaye, C.Jégourel, A. Legay, A. NouriStatistical Model Checking QoS Properties of Systems with SBIP.
      In ISoLA, Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th International Symposium, Heraklion, Crete, Greece, 2012(.pdf, .bib)

    • B.Delahaye, U. Fahrenberg, T.A. Henzinger, A. Legay, D. Nickovic Synchronous Interface Theories and Time Triggered Scheduling.
      In FMOODS/FORTE, 7th International Federated Conference on Distributed Computing Techniques, Stockholm, Sweden, 2012. (.pdf, .bib)

    • B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wasowski APAC: A Tool for Reasoning about Abstract Probabilistic Automata.
      In QEST, 8th International Conference on Quantitative Evaluation of SysTems, Aachen, Germany, 2011. (.pdf, .bib)

    • B. Delahaye, J.-P. Katoen, K.G. Larsen, A. Legay, M.L. Pedersen, F. Sher, A. Wasowski New Results on Abstract Probabilistic Automata.
      In ACSD, 11th International Conference on Application of Concurrency to System Design, Newcastle upon Tyne, UK, 2011.(.pdf, long)

    • B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wasowski Decision Problems for Interval Markov Chains.
      In LATA, 5th International Conference on Language and Automata Theory and Applications , Tarragona, Spain, 2011. (.pdf,.bib, long)

    • B. Delahaye, J.-P. Katoen, K.G. Larsen, A. Legay, M.L. Pedersen, F. Sher, A. Wasowski. Abstract Probabilistic Automata
      In VMCAI, 12th International Conference on Verification, Model Checking and Abstract Interpretation, Austin, TX, USA, 2011. (.pdf, .bib, long)

    • B. Caillaud, B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wasowski. Compositional Design Methodology with Constraint Markov Chains
      In QEST, 7th International Conference on Quantitative Evaluation of SysTems, Williamsburg, Virginia, USA, 2010. (.pdf, .bib, long)

    • A. Legay, B. Delahaye, S. Bensalem. Statistical Model Checking: An Overview
      In RV, 1st Conference on Runtime Verification, Malta, 2010. (.pdf, .bib)

    • A. Basu, S. Bensalem, M. Bozga, B. Delahaye, A. Legay, E. Sifakis. Verification of an AFDX Infrastructure using Simulations and Probabilities
      In RV, 1st Conference on Runtime Verification, Malta, 2010. (.pdf, .bib)

    • B. Delahaye, B. Caillaud, A. Legay. Probabilistic Contracts: A Compositional Reasoning Methodology for the Design of Stochastic Systems
      In ACSD, 10th International Conference on Application of Concurrency to System Design, Braga, Portugal, 2010. (.pdf, .bib)

    • A. Basu, S. Bensalem, M. Bozga, B. Caillaud, B. Delahaye, A. Legay. Statistical abstraction and model-checking of large heterogeneous systems
      In FMOODS/FORTE, 5th International Federated Conference on Distributed Computing Techniques, Amsterdam, The Netherlands.
      Volume 6117 of Lecture Notes in Computer Science , pages 32-46, Springer, 2010. (.pdf, .bib)
  • Workshops

    • B. Delahaye. Consistency for Parametric Interval Markov Chains.
      In SynCoP, 2nd Nordic Workshop Synthesis of Complex Parameters, London, UK, 2015.(.pdf,.bib)

    • É. André, B. Delahaye, P. Habermehl, C. Jard, D. Lime, L. Petrucci, O.H. Roux, T. Touili. Beyond Model Checking: Parameters Everywhere.
      In Journées GDR GPL -- Défis 2025, 2014

    • B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wasowski. Stuttering in Abstract Probabilistic Automata
      In NWPT, 23rd Nordic Workshop on Programming Theory, Västerås, Sweden, 2011. (.pdf)

    • B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wasowski. Decision Problems for Interval Markov Chains
      In NWPT, 22nd Nordic Workshop on Programming Theory , Turku, Finland, 2010. (.pdf)

    • B. Delahaye, B. Caillaud, A. Legay. Compositional Reasoning for Assume/Guarantee Contracts Combining Stochastic and Nondeterministic Aspects
      In NWPT, 21st Nordic Workshop on Programming Theory, Lyngby, Denmark, 2009. (.pdf)

    • B. Delahaye. Probabilistic Contract Based Reasoning with Markov Decision Processes
      Extended abstract, MOVEP, 2008. (.pdf)
  • Rapports

    • B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wasowski New Results for Constraint Markov Chains.
      Rapport de Recherche, 2011.(.pdf)

    • B.Caillaud, B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wasowski Constraint Markov Chains.
      Rapport de Recherche, 2011.(.pdf)

    • B. Delahaye, K.G. Larsen, A. Legay, A. Wasowski On Greatest Lower Bound of Modal Transition Systems.
      Rapport de Recherche, 2010.(.pdf)

    • A. Legay, B. Delahaye. Statistical Model Checking: an overview
      In CoRR, abs/1005.1327, 2010.

    • Compositional Design Methodology with Constraint Markov Chains.
      Rapport de Recherche INRIA, 2010.(.pdf,.bib)

    • Statistical abstraction and model-checking of large heterogeneous systems.
      Rapport de Recherche INRIA, 2010. (.pdf,.bib)

    • Compositional Reasoning on (Probabilistic) Contracts.
      Rapport de Recherche INRIA, 2009. (.pdf,.bib)

    • A Model for Probabilistic Reasoning on Assume/Guarantee Contracts.
      Rapport de Recherche INRIA, 2008. (.pdf, .bib)

    • Problème d'optimisation quadratique pour la synthèse de circuits VLSI et de programme flot de données optimaux.
      Rapport du stage de Master à l'IRISA en 2006 (.pdf).

    • Toward Flexible Equational Reasoning for a Purely Imperative Calculus.
      Rapport du stage à l'université d'Heriot-Watt en 2005 (.pdf).
    • Evaluation des performances du DMA dans la technologie SCI et implantation dans Madeleine.
      Rapport du stage au LaBRI en 2004 (.pdf).