Zobrazeno 1 - 10
of 19
pro vyhledávání: '"Tamir Heyman"'
Publikováno v:
International Journal of Foundations of Computer Science. 18:45-61
Recent advances in scheduling and networking have paved the way for efficient exploitation of large-scale distributed computing platforms such as computational grids and huge clusters. Such infrastructures hold great promise for the highly resource-d
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f71d04919de995a4fb3d04ac74348e04
https://doi.org/10.1142/s0129054107004565
https://doi.org/10.1142/s0129054107004565
Publikováno v:
Formal Methods in System Design. 29:157-175
This work presents a novel distributed symbolic algorithm for reachability analysis that can effectively exploit, as needed, a large number of machines working in parallel. The novelty of the algorithm is in its dynamic allocation and reallocation of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b7002cfbcc52f60ce3642422e933cb96
https://doi.org/10.1007/s10703-006-0011-4
https://doi.org/10.1007/s10703-006-0011-4
Publikováno v:
Formal Methods in System Design. 26:197-219
In this paper we propose a distributed symbolic algorithm for model checking of propositional ?-calculus formulas. ?-calculus is a powerful formalism and ?-calculus model checking can solve many problems, including, for example, verification of (fair
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::64a04a58a5c3e67f2f75e9c640001a5b
https://doi.org/10.1007/s10703-005-1493-1
https://doi.org/10.1007/s10703-005-1493-1
Publikováno v:
International Journal on Software Tools for Technology Transfer. 4:496-504
This paper presents a scalable method for parallel symbolic on-the-fly model checking in a distributed memory environment. Our method combines a scheme for on-the-fly model checking for safety properties with a scheme for scalable reachability analys
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f4b2b450e4c159a7f7fa5a7d38c58203
https://doi.org/10.1007/s10009-002-0093-2
https://doi.org/10.1007/s10009-002-0093-2
Publikováno v:
Formal Methods in System Design. 23:39-65
High-performance hardware designs often intersperse combinational logic freely between level-sensitive latch layers (wherein each layer is transparent during only one clock phase), rather than utilizing master-slave latch pairs with no combinational
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::30612fd6e4be8aa981019fd3957036ed
https://doi.org/10.1023/a:1024485130001
https://doi.org/10.1023/a:1024485130001
Publikováno v:
Formal Methods in System Design. 21:317-338
This paper presents a scalable method for parallelizing symbolic reachability analysis on a distributed-memory environment of workstations. We have developed an adaptive partitioning algorithm that significantly reduces space requirements. The memory
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8e38541c92ae6d2d1eb70b84a2037798
https://doi.org/10.1023/a:1020373206491
https://doi.org/10.1023/a:1020373206491
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319092836
SAT
SAT
This paper presents an application of formal methods to the verification of hardware power management modules. The property being verified is called Dominant Controllability and is a property of a netlist node and a subset of the inputs. The property
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::82c34bea2188cfd7425daf1d64c6cf60
https://doi.org/10.1007/978-3-319-09284-3_18
https://doi.org/10.1007/978-3-319-09284-3_18
Autor:
Yael Abarbanel-Vinov, Neta Aizenbud-Reshef, Irit Shitsevalov, Cindy Eisner, Iris Reuveni, Tali Yatzkar-Haham, Yaron Wolfsthal, Ilan Beer, Daniel Geist, Tamir Heyman, Eran Rippel
Publikováno v:
Formal Methods in System Design. 19:35-44
We examine IBM's exploitation of formal verification using RuleBase—a formal verification tool developed by the IBM Haifa Research Laboratory. The goal of the paper is methodological. We identify an integrated methodology for the deployment of form
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::22163b2a577ba0e8eb2e52412bf3819e
https://doi.org/10.1023/a:1011219209077
https://doi.org/10.1023/a:1011219209077
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783540291053
CHARME
CHARME
This paper presents a novel BDD-based distributed algorithm for reachability analysis which is completely asynchronous. Previous BDD-based distributed schemes are synchronous: they consist of interleaved rounds of computation and communication, in wh
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a42dfa233f575de7abe60546dab39134
https://doi.org/10.1007/11560548_12
https://doi.org/10.1007/11560548_12
Publikováno v:
Automated Technology for Verification and Analysis ISBN: 9783540292098
ATVA
ATVA
Recent advances in scheduling and networking have cleared the way for efficient exploitation of large-scale distributed computing platforms, such as computational grids and huge clusters. Such infrastructures hold great promise for the highly resourc
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7a922eb6b3792f21089d88f9f226a328
https://doi.org/10.1007/11562948_4
https://doi.org/10.1007/11562948_4