Freek Verbeek

Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

2021

X86 instruction semantics and basic block symbolic execution.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Verification of Functional Correctness of Code Diversification Techniques.

[BibT_eX]

[DOI]

Jae-Won Jang

Proceedings of the NASA Formal Methods - 13th International Symposium, 2021

2020

Highly Automated Formal Proofs over Memory Usage of Assembly Code.

[BibT_eX]

[DOI]

Joshua A. Bockenek

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Sound C Code Decompilation for a Subset of x86-64 Binaries.

[BibT_eX]

[DOI]

Pierre Olivier

Marko C. J. D. van Eekelen

Proceedings of the Software Engineering and Formal Methods - 18th International Conference, 2020

2019

A benchmark for C program verification.

[BibT_eX]

[DOI]

CoRR, 2019

Formal Verification of Memory Preservation of x86-64 Binaries.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, Reliability, and Security, 2019

Establishing a refinement relation between binaries and abstract code.

[BibT_eX]

[DOI]

Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, 2019

Formally verified big step semantics out of x86-64 binaries.

[BibT_eX]

[DOI]

Ian Roessle

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

A Compositional Approach for Verifying Protocols Running on On-Chip Networks.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2018

2017

Deadlock Verification of Cache Coherence Protocols and Communication Fabrics.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2017

Estimating worst-case latency of on-chip interconnects with formal simulation.

[BibT_eX]

[DOI]

Nike van Vugt

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016

CoBRA: Low cost compensation of TSV failures in 3D-NoC.

[BibT_eX]

[DOI]

Proceedings of the 2016 IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems, 2016

ADVOCAT: Automated deadlock verification for on-chip cache coherence and interconnects.

[BibT_eX]

[DOI]

Proceedings of the 2016 Design, Automation & Test in Europe Conference & Exhibition, 2016

2015

Formal API Specification of the PikeOS Separation Kernel.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

2014

A Decision Procedure for Deadlock-Free Routing in Wormhole Networks.

[BibT_eX]

[DOI]

IEEE Trans. Parallel Distributed Syst., 2014

Recreational Formal Methods: Designing Vacuum Cleaning Trajectories.

[BibT_eX]

[DOI]

Frits W. Vaandrager

Bull. EATCS, 2014

Formal Specification of a Generic Separation Kernel.

[BibT_eX]

[DOI]

Abderrahmane Feliachi

Burkhart Wolff

Arch. Formal Proofs, 2014

Inference of channel types in micro-architectural models of on-chip communication networks.

[BibT_eX]

[DOI]

Bernard van Gastel

Proceedings of the 22nd International Conference on Very Large Scale Integration, 2014

On Two Models of Noninterference: Rushby and Greve, Wilding, and Vanfleet.

[BibT_eX]

[DOI]

Adrian Garcia Ramirez

Proceedings of the Computer Safety, Reliability, and Security, 2014

2013

Verification of Building Blocks for Asynchronous Circuits

[BibT_eX]

[DOI]

Proceedings of the Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, 2013

Formal Deadlock Verification for Click Circuits.

[BibT_eX]

[DOI]

Sebastiaan J. C. Joosten

Proceedings of the 19th IEEE International Symposium on Asynchronous Circuits and Systems, 2013

2012

Towards the formal verification of cache coherency at the architectural level.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2012

Easy Formal Specification and Validation of Unbounded Networks-on-Chips Architectures.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2012

Proof Pearl: A Formal Proof of Dally and Seitz' Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

A formally verified deadlock-free routing function in a fault-tolerant NoC architecture.

[BibT_eX]

[DOI]

Proceedings of the 25th Symposium on Integrated Circuits and Systems Design, 2012

Automatic generation of deadlock detection algorithms for a family of microarchitecture description languages of communication fabrics.

[BibT_eX]

[DOI]

Proceedings of the 2012 IEEE International High Level Design Validation and Test Workshop, 2012

2011

On Necessary and Sufficient Conditions for Deadlock-Free Routing in Wormhole Networks.

[BibT_eX]

[DOI]

IEEE Trans. Parallel Distributed Syst., 2011

A Comment on "A Necessary and Sufficient Condition for Deadlock-Free Adaptive Routing in Wormhole Networks".

[BibT_eX]

[DOI]

IEEE Trans. Parallel Distributed Syst., 2011

Formal verification of a deadlock detection algorithm

[BibT_eX]

[DOI]

Proceedings of the Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, 2011

A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free.

[BibT_eX]

[DOI]

Proceedings of the 19th International Euromicro Conference on Parallel, 2011

Automatic verification for deadlock in networks-on-chips with adaptive routing and wormhole switching.

[BibT_eX]

[DOI]

Proceedings of the NOCS 2011, 2011

Hunting deadlocks efficiently in microarchitectural models of communication fabrics.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

2010

A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Formal specification of networks-on-chips: deadlock and evacuation.

[BibT_eX]

[DOI]