Zobrazeno 1 - 10
of 12
pro vyhledávání: '"Adrien Champion"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 105, Iss Proc. FTSCS 2012, Pp 22-38 (2012)
This paper addresses the issue of lemma generation in a k-induction-based formal analysis of transition systems, in the linear real/integer arithmetic fragment. A backward analysis, powered by quantifier elimination, is used to output preimages of th
Externí odkaz:
https://doaj.org/article/7504b9a5266f46adb662a8f034469f56
Publikováno v:
Journal of Automated Reasoning. 64:1393-1418
We propose a method for automatically finding refinement types of higher-order function programs. Our method is an extension of the Ice framework of Garg et al. for finding invariants. In addition to the usual positive and negative samples in machine
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b1eff2463a5decc280d177d51689318a
https://doi.org/10.1007/s10817-020-09571-y
https://doi.org/10.1007/s10817-020-09571-y
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783319899596
TACAS (1)
TACAS (1)
We propose a method for automatically finding refinement types of higher-order function programs. Our method is an extension of the Ice framework of Garg et al. for finding invariants. In addition to the usual positive and negative samples in machine
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6e93bb9578067f32d4c5f9c2fd1b3fb9
https://doi.org/10.1007/978-3-319-89960-2_20
https://doi.org/10.1007/978-3-319-89960-2_20
Publikováno v:
Programming Languages and Systems ISBN: 9783030027674
APLAS
APLAS
The ICE framework is a machine-learning-based technique originally introduced for inductive invariant inference over transition systems, and building on the supervised learning paradigm. Recently, we adapted the approach to non-linear Horn clause sol
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6bcf184f1e665c2a8e957e6deece7520
https://doi.org/10.1007/978-3-030-02768-1_8
https://doi.org/10.1007/978-3-030-02768-1_8
Publikováno v:
Science of Computer Programming. 103:71-87
This paper addresses the issue of potential invariant generation in the formal analysis of transition systems with k-induction, in the linear real/integer arithmetic fragment. First, quantifier elimination is used to find parameters for generic templ
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7212a438a14277435b0f5578a116a91f
https://doi.org/10.1016/j.scico.2014.10.004
https://doi.org/10.1016/j.scico.2014.10.004
Autor:
Romain Jobredeaux, Michael Dierkes, Rémi Delmas, Adrien Champion, Pierre Roux, Pierre-Loïc Garoche
Publikováno v:
SAE International Journal of Aerospace. 6:150-160
Critical control systems are often built as a combination of a control core with safety mechanisms allowing to recover from failures. For example a PID controller used with triplicated inputs and voting. Typically these systems would be designed at t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::34762e6e56e11d7798e35b9ae13c44d0
https://doi.org/10.4271/2013-01-2109
https://doi.org/10.4271/2013-01-2109
Autor:
Rémi Delmas, Adrien Champion
Publikováno v:
Journal Européen des Systèmes Automatisés. 47:45-59
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a9225dec54d9a8255b4f758a669acdd8
https://doi.org/10.3166/jesa.47.45-59
https://doi.org/10.3166/jesa.47.45-59
Publikováno v:
Computer Aided Verification ISBN: 9783319415390
CAV (2)
CAV (2)
Kind 2 is an open-source, multi-engine, SMT-based model checker for safety properties of finite- and infinite-state synchronous reactive systems. It takes as input models written in an extension of the Lustre language that allows the specification of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::605088c2ffa69f9ae9d5e29d520db205
https://doi.org/10.1007/978-3-319-41540-6_29
https://doi.org/10.1007/978-3-319-41540-6_29
Publikováno v:
Software Engineering and Formal Methods ISBN: 9783319415901
SEFM
SEFM
Contract-based software development has long been a leading methodology for the construction of component-based reactive systems, embedded systems in particular. Contracts are an effective way to establish boundaries between components and can be use
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::23be759dce331772ac191c151bd92cac
https://doi.org/10.1007/978-3-319-41591-8_24
https://doi.org/10.1007/978-3-319-41591-8_24
Publikováno v:
SAE International Journal of Aerospace. 4:850-858
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::da7ea02c0ff81621539f456bf2c5c9a1
https://doi.org/10.4271/2011-01-2558
https://doi.org/10.4271/2011-01-2558