Zobrazeno 1 - 10
of 17
pro vyhledávání: '"Etienne Renault"'
Publikováno v:
International Journal on Software Tools for Technology Transfer. 25:77-94
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b038338fe06f40bf7d44c8d348bada6c
https://doi.org/10.1007/s10009-022-00692-w
https://doi.org/10.1007/s10009-022-00692-w
Publikováno v:
Constraints. 28:45-66
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9e669780e4a377d7e0cb9d70f5b9e0d0
https://doi.org/10.1007/s10601-022-09339-8
https://doi.org/10.1007/s10601-022-09339-8
Publikováno v:
2022 29th Asia-Pacific Software Engineering Conference (APSEC).
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1d14f32ae3cb8a1d05128cbb9f5c0048
https://doi.org/10.1109/apsec57359.2022.00038
https://doi.org/10.1109/apsec57359.2022.00038
Autor:
Etienne Renault
Publikováno v:
Innovations in Systems and Software Engineering. 16:143-159
The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model checking, this exploration uses a depth-first search and can be achieved with multiple randomized threads to increas
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7d72b4ec6158a70ff6631f0eb356a84d
https://doi.org/10.1007/s11334-020-00362-7
https://doi.org/10.1007/s11334-020-00362-7
Autor:
Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, Henrich Lauko
Publikováno v:
Computer Aided Verification ISBN: 9783031131875
Spot is a C++17 library for LTL and $$\omega $$ ω -automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to su
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3a1228d6feac1ee58f07fcae262b8634
https://doi.org/10.1007/978-3-031-13188-2_9
https://doi.org/10.1007/978-3-031-13188-2_9
Publikováno v:
Formal Techniques for Distributed Objects, Components, and Systems ISBN: 9783031086786
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b245372466aacce2ec33f4b25c962bdf
https://doi.org/10.1007/978-3-031-08679-3_11
https://doi.org/10.1007/978-3-031-08679-3_11
Publikováno v:
Model Checking Software ISBN: 9783030846282
SPIN
SPIN
We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin [19] and Spot [7]. Go2Pins is an effort to promote the integration of both formal verification and testing inside industrial-size projects. W
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b1d0d3162e0a20557cc26cdb26e50e33
https://doi.org/10.1007/978-3-030-84629-9_8
https://doi.org/10.1007/978-3-030-84629-9_8
Autor:
Etienne Renault, Denis Poitrenaud
Publikováno v:
ICFEM 2019-21st International Conference on Formal Engineering Methods
ICFEM 2019-21st International Conference on Formal Engineering Methods, Nov 2019, Shenzhen, China. pp.370-386, ⟨10.1007/978-3-030-32409-4_23⟩
Formal Methods and Software Engineering ISBN: 9783030324087
ICFEM
ICFEM 2019-21st International Conference on Formal Engineering Methods, Nov 2019, Shenzhen, China. pp.370-386, ⟨10.1007/978-3-030-32409-4_23⟩
Formal Methods and Software Engineering ISBN: 9783030324087
ICFEM
International audience; In explicit state model checking of concurrent systems, multi-core emptiness checks and partial order reductions (POR) are two major techniques to handle large state spaces. The first one tries to take advantage of multi-core
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ebc9af6f13a47833113e71026302933d
https://hal.sorbonne-universite.fr/hal-02408440/document
https://hal.sorbonne-universite.fr/hal-02408440/document
Autor:
Etienne Renault
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030003586
VECoS
VECoS
The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model-checking this exploration uses a Depth-First-Search (DFS) and can be achieved with multiple randomized threads to in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2d5a546bb4243ed0823d9fbab12ab6b3
https://doi.org/10.1007/978-3-030-00359-3_9
https://doi.org/10.1007/978-3-030-00359-3_9
Publikováno v:
International Journal on Software Tools for Technology Transfer
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017, 19 (6), pp.653-673. ⟨10.1007/s10009-016-0422-5⟩
International Journal on Software Tools for Technology Transfer, 2017, 19 (6), pp.653-673. ⟨10.1007/s10009-016-0422-5⟩
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017, 19 (6), pp.653-673. 〈10.1007/s10009-016-0422-5〉
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017, 19 (6), pp.653-673. ⟨10.1007/s10009-016-0422-5⟩
International Journal on Software Tools for Technology Transfer, 2017, 19 (6), pp.653-673. ⟨10.1007/s10009-016-0422-5⟩
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017, 19 (6), pp.653-673. 〈10.1007/s10009-016-0422-5〉
International audience; We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a Strongly Connected Component (SCC) enumeration, support generalized Büchi acceptance, a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9fea83823f89ba514a0df6f46fe3f8b8
https://hal.sorbonne-universite.fr/hal-01310101/document
https://hal.sorbonne-universite.fr/hal-01310101/document