Zobrazeno 1 - 10
of 14
pro vyhledávání: '"BENDÍK., JAROSLAV"'
The need to solve non-linear arithmetic constraints presents a major obstacle to the automatic verification of smart contracts. In this case study we focus on the two overapproximation techniques used by the industry verification tool Certora Prover:
Externí odkaz:
http://arxiv.org/abs/2402.10174
Publikováno v:
Logical Methods in Computer Science, Volume 18, Issue 3 (July 29, 2022) lmcs:8375
Timed automata (TA) have been widely adopted as a suitable formalism to model time-critical systems. Furthermore, contemporary model-checking tools allow the designer to check whether a TA complies with a system specification. However, the exact timi
Externí odkaz:
http://arxiv.org/abs/2108.08018
Version Control Systems (VCS) are frequently used to support development of large-scale software projects. A typical VCS repository of a large project can contain various intertwined branches consisting of a large number of commits. If some kind of u
Externí odkaz:
http://arxiv.org/abs/1708.06623
In various areas of computer science, we deal with a set of constraints to be satisfied. If the constraints cannot be satisfied simultaneously, it is desirable to identify the core problems among them. Such cores are called minimal unsatisfiable subs
Externí odkaz:
http://arxiv.org/abs/1708.00400
Autor:
Bendík, Jaroslav, Meel, Kuldeep S.
Publikováno v:
Formal Methods in System Design; Oct2024, Vol. 63 Issue 1-3, p5-39, 35p
In various areas of computer science, the problem of dealing with a set of constraints arises. If the set of constraints is unsatisfiable, one may ask for a minimal description of the reason for this unsatisifi- ability. Minimal unsatisifable subsets
Externí odkaz:
http://arxiv.org/abs/1606.03289
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Timed automata (TA) have been widely adopted as a suitable formalism to model time-critical systems. Furthermore, contemporary model-checking tools allow the designer to check whether a TA complies with a system specification. However, the exact timi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::93b48989180ab463274a863d99b82e79
https://lmcs.episciences.org/8375
https://lmcs.episciences.org/8375
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems
Timed automata (TA) have shown to be a suitable formalism for modeling real-time systems. Moreover, modern model-checking tools allow a designer to check whether a TA complies with the system specification. However, the exact timing constraints of th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=pmc_________::72193d26155d27b46e3c21efe5bd82b6
http://europepmc.org/articles/PMC7979188
http://europepmc.org/articles/PMC7979188
Autor:
Bendík, Jaroslav, Meel, Kuldeep S.
Publikováno v:
Computer Aided Verification
Given an unsatisfiable formula F in CNF, i.e. a set of clauses, the problem of Minimal Unsatisfiable Subset (MUS) seeks to identify a minimal subset of clauses \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfon
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=pmc_________::5caafcee88be4f6f40b58794b52c0b23
http://europepmc.org/articles/PMC7363222
http://europepmc.org/articles/PMC7363222