Zobrazeno 1 - 10
of 42
pro vyhledávání: '"Antti E. J. Hyvärinen"'
Publikováno v:
Formal Methods in System Design.
This article provides an innovative approach for verification by model checking of programs that undergo continuous changes. To tackle the problem of repeating the entire model checking for each new version of the program, our approach verifies progr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a1de8562b26c24c6f65344e1f80b6d39
https://doi.org/10.1007/s10703-023-00423-0
https://doi.org/10.1007/s10703-023-00423-0
Publikováno v:
International Journal on Software Tools for Technology Transfer. 24:111-125
The use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::80b36dbd025462fb4c23dece3b30ee85
https://doi.org/10.1007/s10009-021-00641-z
https://doi.org/10.1007/s10009-021-00641-z
Publikováno v:
Computer Aided Verification ISBN: 9783031131844
Formally verifying smart contracts is important due to their immutable nature, usual open source licenses, and high financial incentives for exploits. Since 2019 the Ethereum Foundation’s Solidity compiler ships with a model checker. The checker, c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ec6ecde104f54f4283e9d9209ca1b573
https://doi.org/10.1007/978-3-031-13185-1_16
https://doi.org/10.1007/978-3-031-13185-1_16
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995232
While model checking safety of infinite-state systems by inferring state invariants has steadily improved recently, most verification tools still rely on a technique based on bounded model checking to detect safety violations. In particular, the curr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3e1e136112bcbeb25ab91601edd4549b
https://doi.org/10.1007/978-3-030-99524-9_29
https://doi.org/10.1007/978-3-030-99524-9_29
Publikováno v:
DAC
Ensuring hardware and software correctness increasingly relies on the use of symbolic logic solvers, in particular for satisfiability modulo theories (SMT). However, building efficient and correct SMT solvers is difficult: even state-of-the-art solve
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4d8a377ea12deea596aa36d14e97afb4
https://doi.org/10.1109/dac18074.2021.9586272
https://doi.org/10.1109/dac18074.2021.9586272
Autor:
Antti E. J. Hyvärinen, Jan Kofroň, Leonardo Alt, Grigory Fedyukovich, Natasha Sharygina, Pavel Jančík
Publikováno v:
Formal Methods in System Design. 55:33-71
Craig interpolation has been successfully employed in symbolic program verification as a means of abstraction for sets of program states. In this article, we present the partial variable assignment interpolation system, an extension of the labeled in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c6460c321dae95bb3711dd2f430fba31
https://doi.org/10.1007/s10703-019-00342-z
https://doi.org/10.1007/s10703-019-00342-z
Autor:
Antti E. J. Hyvärinen, Natasha Sharygina, Patrick Eugster, Rodrigo Otoni, Leonardo Alt, Matteo Marescotti
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030614669
ISoLA (3)
ISoLA (3)
Smart contracts challenge the existing, highly efficient techniques applied in symbolic model checking of software by their unique traits not present in standard programming models. Still, the majority of reported smart contract verification projects
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c9159d3dba2caca293ff46c3465f9797
https://doi.org/10.1007/978-3-030-61467-6_12
https://doi.org/10.1007/978-3-030-61467-6_12
Publikováno v:
Static Analysis ISBN: 9783030654733
SAS
SAS
Linear arithmetic over reals (LRA) underlies a wide range of SMT-based modeling approaches, and, strengthened with Craig interpolation using Farkas’ lemma, is a central tool for efficient over-approximation. Recent advances in LRA interpolation hav
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::75db49984fbd62c9674667ed27bbebed
https://doi.org/10.1007/978-3-030-65474-0_16
https://doi.org/10.1007/978-3-030-65474-0_16
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030393212
VMCAI
VMCAI
Recently presented, IC3-inspired symbolic model checking algorithms strengthen the procedure for showing inductiveness of lemmas expressing reachability of states. These approaches show an impressive performance gain in comparison to previous state-o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9389e52a2f8648ee090c519dc6ac49d5
https://doi.org/10.1007/978-3-030-39322-9_13
https://doi.org/10.1007/978-3-030-39322-9_13
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030174613
TACAS (1)
TACAS (1)
Modern verification commonly models software with Boolean logic and a system of linear inequalities over reals and over-approximates the reachable states of the model with Craig interpolation to obtain, for example, candidates for inductive invariant
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b3951f90a5f75436ef435c2cb13c90ac
https://doi.org/10.1007/978-3-030-17462-0_1
https://doi.org/10.1007/978-3-030-17462-0_1