Výsledky vyhledávání - "Nicolas Amat"

SMPT: A Testbed for Reachability Methods in Generalized Petri Nets

Publikováno v: Proceedings of the 25th International Symposium on Formal Methods, LNCS 14000
25th International Symposium on Formal Methods (FM 2023)
25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.445-453, ⟨10.1007/978-3-031-27481-7_25⟩
Formal Methods ISBN: 9783031274800

SMPT (for Satisfiability Modulo Petri Net) is a model checker for reachability problems in Petri nets. It started as a portfolio of methods to experiment with symbolic model checking, and was designed to be easily extended. Some distinctive features

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8b0b15729fb98a38deaacb46d1e755fa
http://arxiv.org/abs/2302.14741

Zobrazit plný text záznamu

Leveraging polyhedral reductions for solving Petri net reachability problems

Autor: Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan

Publikováno v: International Journal on Software Tools for Technology Transfer
International Journal on Software Tools for Technology Transfer, 2023, 25, pp.95-114. ⟨10.1007/s10009-022-00694-8⟩

We propose a new method that takes advantage of structural reductions to accelerate the verification of reachability properties on Petri nets. Our approach relies on a state space abstraction, called polyhedral abstraction, which involves a combinati

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f90c1b88fe1b0d6073f791c9f949596f
https://hal.laas.fr/hal-03973463/document

Zobrazit plný text záznamu

Automated Polyhedral Abstraction Proving

Autor: Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan

Publikováno v: Application and Theory of Petri Nets and Concurrency ISBN: 9783031336195
Application and Theory of Petri Nets and Concurrency. PETRI NETS 2023
44th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2023)
44th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2023), Jun 2023, Lisbon, Portugal. pp.324-345, ⟨10.1007/978-3-031-33620-1_18⟩

International audience; We propose an automated procedure to prove polyhedral abstractions for Petri nets. Polyhedral abstraction is a new type of state-space equivalence based on the use of linear integer constraints. Our approach relies on an encod

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7cabce154f332efecde76c8bafa58d4d
https://doi.org/10.1007/978-3-031-33620-1_18

Zobrazit plný text záznamu

Property Directed Reachability for Generalized Petri Nets

Autor: Silvano Dal Zilio, Nicolas Amat, Thomas Hujsa

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022
Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022, Apr 2022, Munich, Germany. ⟨10.1007/978-3-030-99524-9_28⟩
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995232

We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on th

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b499303cd9d345711aabb81d7fd4a753
http://arxiv.org/abs/2208.03043

Zobrazit plný text záznamu

Accelerating the Computation of Dead and Concurrent Places using Reductions

Autor: Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan

Publikováno v: 27th International SPIN Symposium on Model Checking of Software
27th International SPIN Symposium on Model Checking of Software, Jul 2021, Aarhus, Denmark. ⟨10.1007/978-3-030-84629-9_3⟩
Model Checking Software ISBN: 9783030846282
SPIN

International audience; We propose a new method for accelerating the computation of a concurrency relation, that is all pairs of places in a Petri net that can be marked together. Our approach relies on a state space abstraction, that involves a mix

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d9d23dfaef0fc8597e24161a91cc9398
https://hal.laas.fr/hal-03268388

Zobrazit plný text záznamu

On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets

Autor: Bernard Berthomieu, Nicolas Amat, Silvano Dal Zilio

Publikováno v: 42rd International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2021)
42rd International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2021), Jun 2021, Paris (virtual), France. ⟨10.1007/978-3-030-76983-3_9⟩
Application and Theory of Petri Nets and Concurrency ISBN: 9783030769826
Petri Nets

International audience; We define a method for taking advantage of net reductions in combination with a SMT-based model checker. We prove the correctness of this method using a new notion of equivalence between nets that we call polyhedral abstractio

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0181a17244ec5ccc0528f83f190143a9
https://hal.laas.fr/hal-03202111/file/paper.pdf

Zobrazit plný text záznamu

A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking

Autor: Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio

Publikováno v: Fundamenta Informaticae
Fundamenta Informaticae, 2022, 187 (2-4), pp.103-138. ⟨10.3233/FI-222134⟩

International audience; We define a new method for taking advantage of net reductions in combination with a SMT-based model checker. Our approach consists in transforming a reachability problem about some Petri net, into the verification of an update

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bfd9d9608b24b53d500715bc9b4fdf93
http://arxiv.org/abs/2104.09850

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání