### Page Not Found

Page not found. Your pixels are in another canvas.

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Page not found. Your pixels are in another canvas.

News

This is a page not in th emain menu

** Published:**

Basic syntax highlighting for K (the K Framework) in the Kakoune text editor.

** Published:**

Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. This post highlights our achievements in formally proving key correctness properties of finality in Gasper using the Coq proof assistant.

** Published:**

Ever wondered how K and Coq compare and contrast as language verification frameworks? I posted a series of articles comparing K and Coq as language verification frameworks through a working example.

** Published:**

I posted an article celebrating the successful completion of the first milestone in an ongoing collaboration between Runtime Verification and Ethereum Foundation, to build a formal framework for modeling and verifying the Beacon Chain. We have completed the executable formal model of Beacon Chain in the K Framework.

** Published:**

We have two papers presented today at the 1st Workshop on Formal Methods for Blockchains, hosted by the 3rd Formal Methods World Congress on October 11, 2019 in Porto, Portugal:

** Published:**

I posted an article celebrating the successful completion of the first part of an ongoing collaboration between Runtime Verification and Algorand, to model Algorand’s consensus protocol and verify its safety theorem using the Coq proof assistant].

Statistical model checking of distance fraud attacks on the Hancke-Kuhn family of protocols

A formal resource-bounded-intruders model for a wide range of denial of service attacks

Statistical model checking of RANDAO’s resilience against pre-computed reveal sstrategies

Modeling of the Algorand Consensus Protocol in the Coq proof assistant and verifying its safety guarantees

An executable K model of Ethereum 2.0 Beacon Chain Phase 0 specification

Modeling Gasper and verifying its properties using the Coq proof assistant

*Principles and Practice of Declarative Programming, ACM, pp 131–142*, 2007

Musab A. Alturki and José Meseguer

*Automated Specification and Verification of Web Systems, ENTCS 200, pp 25–41*, 2008

Musab A. Alturki and José Meseguer

*International Symposium on Information, Computer, and Communications Security, ACM, pp 262-275*, 2009

Rakesh Bobba, Himanshu Khurana, Musab A. Alturki and Farhana Ashraf

*Security and Rewriting Techniques, ENTCS 234, pp 3-18*, 2009

Musab A. Alturki, José Meseguer and Carl A. Gunter

*Fundamental Approaches to Software Engineering, Springer, LNCS 5503, pp 262-277*, 2009

Musab A. Alturki, Dinakar Dhurjati, Dachuan Yu, Ajay Chander and Hiroshi Inamura

*European Symposium on Research in Computer Security, Springer, LNCS 5789, pp 390-405*, 2009

Ravinder Shankesi, Musab A. Alturki, Ralf Sasse, Carl A. Gunter and José Meseguer

*Rewriting Techniques for Real-Time Systems, EPTCS 36, pp 26-45*, 2010

Musab A. Alturki and José Meseguer

*Algebra and Coalgebra in Computer Science, Springer, LNCS 6859, pp 386-392*, 2011

Musab A. Alturki and José Meseguer

*Fundamental Approaches to Software Engineering, Springer, LNCS 7212, pp 78-93*, 2012

Jonas Eckhardt, Tobias Mühlbauer, Musab A. Alturki, José Meseguer and Martin Wirsing

*Artificial Neural Networks and Machine Learning, Springer, LNCS 8681, pp 241-248*, 2014

Issam H. Laradji, Lahouari Ghouti, Faisal Saleh and Musab A. Alturki

*Formal Methods, Springer, LNCS 9109, pp 40-56*, 2015

Musab A. Alturki and Omar Alzuhaibi

*Journal of Logical and Algebraic Methods in Programming, Volume 84(4), pp 505–533*, 2015

Musab A. Alturki and José Meseguer

*Software Engineering Advances, pp 463-469*, 2015

Taher A. Ghaleb, Khalid Aljasser and Musab A. Alturki

*Information Reuse and Integration, IEEE, pp 283-290*, 2017

Musab A. Alturki

*Cyber-Physical Systems Security and Privacy, ACM, pp 60-71*, 2018

Musab A. Alturki, Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov and Carolyn Talcott

*Journal of Software: Evolution and Process, Wiley, Volume 30(11), pp e1965*, 2018

Taher A. Ghaleb, Musab A. Alturki and Khalid Aljasser

*Foundations of Security, Protocols, and Equational Reasoning, Springer, LNCS 11565, pp 192-213*, 2019

Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, Andre Scedrov and Carolyn Talcott

*Computer Security Foundations Symposium, IEEE, pp 382-396*, 2019

Abraão Aires Urquiza, Musab A. Alturki, Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov and Carolyn Talcott

*Formal Methods for Blockchains, (to appear)*, 2019

Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña and Grigore Roşu

** Published:**

Undergraduate Course, *King Fahd University of Petroleum and Minerals*

Fall 2002, Spring 2003

Undergraduate Course, *King Fahd University of Petroleum and Minerals*

2011 – 2013

Undergraduate Course, *King Fahd University of Petroleum and Minerals*

Fall 2011

Undergraduate Course, *King Fahd University of Petroleum and Minerals*

Spring 2012

(Under)graduate Course, *King Fahd University of Petroleum and Minerals*

Fall 2012, Fall 2013

Graduate course, *King Fahd University of Petroleum and Minerals*

Fall 2014, Fall 2015, Fall 2016