Zobrazeno 1 - 10
of 20
pro vyhledávání: '"Mirco Giacobbe"'
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030452360
TACAS (2)
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030452360
TACAS (2)
Quantization converts neural networks into low-bit fixed-point computations which can be carried out by efficient integer-only hardware, and is standard practice for the deployment of neural networks on real-time embedded devices. However, like their
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b3772c1524657a5b2d58588a007b19ac
http://europepmc.org/articles/PMC7480702
http://europepmc.org/articles/PMC7480702
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783031223365
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::99812a3a45982c1b72e2b788fca53f28
https://doi.org/10.1007/978-3-031-22337-2_3
https://doi.org/10.1007/978-3-031-22337-2_3
Publikováno v:
HSCC
This paper accompanies FOSSIL: a software tool for the synthesis of Lyapunov functions and of barrier certificates (or functions) for dynamical systems modelled as differential equations. Lyapunov functions are formal certificates for stability analy
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ea1ee84e4914b522ed6e646949b4e667
https://doi.org/10.1145/3447928.3456646
https://doi.org/10.1145/3447928.3456646
Autor:
Goran Frehse, Alessandro Abate, Dieky Adzkiya, Anna Becchi, Lei Bu, Alessandro Cimatti, Mirco Giacobbe, Alberto Griggio, Sergio Mover, Muhammad Syifa'ul Mufid, Idriss Riouak, Stefano Tonetta, Enea Zaffanella
This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with piecewise constant dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2cd6752339db7b13f3ee1f38c425350c
https://ora.ox.ac.uk/objects/uuid:ccec6497-edeb-457c-b095-f4248837ad3f
https://ora.ox.ac.uk/objects/uuid:ccec6497-edeb-457c-b095-f4248837ad3f
Autor:
Guy Avni, Mirco Giacobbe, Taylor T. Johnson, Guy Katz, Anna Lukina, Nina Narodytska, Christian Schilling
This LNCS volume constitutes the proceedings of the First International Symposium on AI Verification, SAIV 2024, in Montreal, QC, Canada, during July 2024. The scope of the topics was broadly categorized into two groups. The first group, formal metho
We introduce a novel approach to the automated termination analysis of computer programs: we use neural networks to represent ranking functions. Ranking functions map program states to values that are bounded from below and decrease as a program runs
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::425148fb9c6e144eb41427a5ec0131b8
http://arxiv.org/abs/2102.03824
http://arxiv.org/abs/2102.03824
Publikováno v:
Computer Aided Verification ISBN: 9783030816872
CAV (2)
CAV (2)
We present the first machine learning approach to the termination analysis of probabilistic programs. Ranking supermartingales (RSMs) prove that probabilistic programs halt, in expectation, within a finite number of steps. While previously RSMs were
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7ea8d1bf454e47b7d18eeefb1696d6fd
https://doi.org/10.1007/978-3-030-81688-9_1
https://doi.org/10.1007/978-3-030-81688-9_1
Publikováno v:
Scopus-Elsevier
Deep reinforcement learning (DRL) is applied in safety-critical domains such as robotics and autonomous driving. It achieves superhuman abilities in many tasks, however whether DRL agents can be shown to act safely is an open problem. Atari games are
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2807140a3d163e55a0edba98ea1c746e
We propose algorithms for performing model checking and control synthesis for discrete-time uncertain systems under linear temporal logic (LTL) specifications. We construct temporal logic trees (TLT) from LTL formulae via reachability analysis. In co
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c6e7cec6a87e068b5125a5b13af55891