Výsledky vyhledávání - "Freek Verbeek"

Akademický článek

Verification of Building Blocks for Asynchronous Circuits

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 114, Iss Proc. ACL2 2013, Pp 70-84 (2013)

Scalable formal verification constitutes an important challenge for the design of asynchronous circuits. Deadlock freedom is a property that is desired but hard to verify. It is an emergent property that has to be verified monolithically. We present

Externí odkaz: https://doaj.org/article/9b4c969ac0a3457bb1fe3d343936924b

Zobrazit plný text záznamu

Akademický článek

Formal verification of a deadlock detection algorithm

Autor: Freek Verbeek, Julien Schmaltz

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 70, Iss Proc. ACL2 2011, Pp 103-112 (2011)

Deadlock detection is a challenging issue in the analysis and design of on-chip networks. We have designed an algorithm to detect deadlocks automatically in on-chip networks with wormhole switching. The algorithm has been specified and proven correct

Externí odkaz: https://doaj.org/article/ff6921d65a1a49ae80b39bfe66a87608

Zobrazit plný text záznamu

A Formal Semantics for P-Code

Autor: Nico Naus, Freek Verbeek, Dale Walker, Binoy Ravindran

Publikováno v: Lecture Notes in Computer Science ISBN: 9783031258022

Decompilation is currently a widely used tool in reverse engineering and exploit detection in binaries. Ghidra, developed by the National Security Agency, is one of the most popular decompilers. It decompiles binaries to high P-Code, from which the f

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::6ba5adb307718ef27c57a86322994d3c
https://doi.org/10.1007/978-3-031-25803-9_7

Zobrazit plný text záznamu

Formally verified lifting of C-compiled x86-64 binaries

Autor: Freek Verbeek, Joshua Bockenek, Zhoulai Fu, Binoy Ravindran

Publikováno v: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::62140a10bdb3cbd7194f1963d9207d6b
https://doi.org/10.1145/3519939.3523702

Zobrazit plný text záznamu

Fully Reliable Dynamic Routing Logic for a Fault-Tolerant NoC Architecture

Autor: Julien Schmaltz, Freek Verbeek, Abdulaziz Alhussien, Bernard van Gastel, Nader Bagherzadeh

Publikováno v: Scopus-Elsevier
Journal of Integrated Circuits and Systems, 8(1), 43-53. Brazilian Microelectronics Society

A fault-tolerant adaptive wormhole routing function for Networks-on-Chips (NoCs) is presented. The novelty of this routing logic is that it is capable of using runtime information on availability of links to dynamically bypass faulty channels. When f

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::12c49a80a37b69be3bf81ed4b487f794
https://doi.org/10.29292/jics.v8i1.371

Zobrazit plný text záznamu

DSV: Disassembly Soundness Validation Without Assuming a Ground Truth

Autor: Xiaoxin An, Freek Verbeek, Binoy Ravindran

Publikováno v: Lecture Notes in Computer Science ISBN: 9783031067723

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::0ce6a1666c82d971abd91846fdf15b7f
https://doi.org/10.1007/978-3-031-06773-0_34

Zobrazit plný text záznamu

Verification of Functional Correctness of Code Diversification Techniques

Autor: Freek Verbeek, Binoy Ravindran, Jae-Won Jang

Publikováno v: Lecture Notes in Computer Science ISBN: 9783030763831
NFM

Code diversification techniques are popular code-reuse attacks defense. The majority of code diversification research focuses on analyzing non-functional properties, such as whether the technique improves security. This paper provides a methodology t

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::c2f229b4bf7cc2f43e7a56a86811618d
https://doi.org/10.1007/978-3-030-76384-8_11

Zobrazit plný text záznamu

Deadlock Verification of Cache Coherence Protocols and Communication Fabrics

Autor: Freek Verbeek, Pooria M. Yaghini, Ashkan Eghbal, Nader Bagherzadeh

Publikováno v: Verbeek, F, Yaghini, P M, Eghbal, A & Bagherzadeh, N 2017, ' Deadlock Verification of Cache Coherence Protocols and Communication Fabrics ', Ieee Transactions on Computers, vol. 66, no. 2, pp. 272-284 . https://doi.org/10.1109/TC.2016.2584060
IEEE Transactions on Computers, 66, 2, pp. 272-284
IEEE Transactions on Computers, 66, 272-284
Ieee Transactions on Computers, 66(2), 272-284. IEEE COMPUTER SOC

Cache coherence plays a major role in manycore systems. The verification of deadlocks is a challenge in particular, because deadlock freedom is an emerging property. Formal methods often decouple verification of the protocol from verification of the

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9012f39e9cb286f52d6952ab05660806
https://hdl.handle.net/2066/168686

Zobrazit plný text záznamu

Establishing a refinement relation between binaries and abstract code

Autor: Joshua A. Bockenek, Binoy Ravindran, Abhijith Bharadwaj, Freek Verbeek, Ian Roessle

Publikováno v: MEMOCODE

This paper presents a method for establishing a refinement relation between a binary and a high-level abstract model. The abstract model is based on standard notions of control flow, such as if-then-else statements, while loops and variable scoping.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::233138c5422b40e7625de4e0a5a3a40f
https://doi.org/10.1145/3359986.3361215

Zobrazit plný text záznamu

Formally verified big step semantics out of x86-64 binaries

Autor: Freek Verbeek, Binoy Ravindran, Ian Roessle

Publikováno v: CPP

This paper presents a methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x86-

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::247ad3b1ac181a3d3f2e704093c8a721
https://doi.org/10.1145/3293880.3294102

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání