Publications

Export 52 results:
Sort by: Author Title Type [ Year  (Desc)]
2024
El-Zawawy, M. A., C. Lal, and M. Conti, "A Location-Aware and Healing Attestation Scheme for Air-Supported Internet of Vehicles", IEEE Transactions on Intelligent Transportation Systems, vol. 25, issue 2, pp. 2017 - 2033, 2024.
2023
El-Zawawy, M. A., A. Brighente, and M. Conti, "Authenticating Drone-Assisted Internet of Vehicles Using Elliptic Curve Cryptography and Blockchain", IEEE Transactions on Network and Service Management (Impact Factor:4.758), 2023.
El-Zawawy, M. A., P. Kaliyar, M. Conti, and S. Katsikas, "Honey-list based authentication protocol for industrial IoT swarms", Computer Communications, vol. 2011, pp. 239-253, 2023.
2022
El-Zawawy, M. A., P. Faruki, and M. Conti, "Formal Model for Inter-Component Communication and its Security in Android", Computting (Springer - Q2 - Impact factor 2.420), 2022.
El-Zawawy, M. A., A. Brighente, and M. Conti, "SETCAP: Service-Based Energy-Efficient Temporal Credential Authentication Protocol for Internet of Drones", Computer Networks (Q1 - Impact factor: 5.493), 2022.
2021
El-Zawawy, M. A., E. Losiouk, and M. Conti, "Do not let Next-Intent Vulnerability be your next nightmare: type system-based approach to detect it in Android apps", International Journal of Information Security (Q2 - Impact Factor 1.988), 2021.
El-Zawawy, M. A., E. Losiouk, and M. Conti, "Vulnerabilities in Android WebView Objects: Still Not the End!", Computers & Security (Q1- Impact Factor 4.438), 2021.
2019
El-Zawawy, M. A., "A new technique for intent elicitation in Android applications", Iran Journal of Computer Science, pp. 1-12, 2019. Abstract

Android is the most common operating system for smart phones. An Android application is composed of components. Intents are messaging objects. Components communicate using intents. This communication is between components of the same application or different applications. Many security attacks use intents. This paper introduces a new technique, IntGet, for elicitation of intents from Android applications. IntGet was implemented and tested on 359461 smali files of 40 applications. The experimental results revealed that IntGet can be used for designing efficient malware detection methods. The paper shows comparisons between results obtained by IntGet and those obtained by Androguard.

2017
El-Zawawy, M. A., "Modeling Android Fragments and Activities Life Cycles Coordination", 17th International Conference on Computational Science and Its Applications, Trieste, Italy, July 3-6, 2017. Abstract

One of the famous software packages for running smart devices is Android. It is an operating system with middlewares and applications. Android runs most functioning mobile phone and tablet devices, today. On the top of the stack describing the organization of different parts of Android is the “applications” component. A main part of an Android application is activity useful for interaction with users where each activity can be realized as a single-frame user interface. An important tool for utilizing activities is that of fragment representing slices of the interface of the activity. Activities and fragments have life cycles.

This paper presents an operational semantics for precisely and efficiently modeling the state transitions within life cycles of activities and fragments. The semantics considers the effects of the transitions in both life cycles on each other. Such semantics is necessary for precisely designing important static analyses for Android applications including fragment components.

El-Zawawy, M. A., "Posting Graphs for Finding Non-Terminating Executions in Asynchronous Programs", Proceedings of The 17th International Conference on Computational Science and Its Applications, Trieste, Italy, July 3-6, 2017. Abstract

Asynchronous programming is one of the currently dominant programming techniques. The key idea of asynchronous programming is to use a queue to post computations as tasks (events). This queue is used then by the application to pick events asynchronously for processing. Asynchronous programming was found very convenient for achieving a massive percentage of software systems used today such as Gmail and Facebook which are Web 2.0 JavaScript ones.

This paper presents a novel technique for searching for nonterminating executions in asynchronous programming. The targeted cases of nontermination are those caused by the posting concept. The proposed technique is based on graphical representation for posting behaviours of asynchronous programs. Proofs for termination and correctness of the proposed method is outlined in the paper.

El-Zawawy, M. A., "Separation Logic for State Dependencies in Life Cycles of Android Activities and Fragments", 17th International Conference on Computational Science and Its Applications, Trieste, Italy, July 3-6, 2017. Abstract

Millions of smart phones are run by Android, the most common operating system for mobile devices. Main component of Android is applications providing most functionalities of Android smart devices. These applications include e-mail client, entertainment, educational, news, banking, maps, and contacts applications. Testing and verifying Android applications is an important direction of research.

This paper presents a separation logic for state transitions of activities and fragments (important components of applications) during their life cycles. The logic considers the necessary coordinations between the state transitions in the two life cycles. The logic is a good tool to verify and test applications against various issues including security ones.

Chelloug, S. A., and M. A. El-Zawawy, "Middleware for Internet of Things: Survey and Challenges", Intelligent Automation & Soft Computing, 2017. AbstractWebsite

The Internet of things (IoT) applications span many potential fields. Furthermore, smart homes, smart cities, smart vehicular networks, and healthcare are very attractive and intelligent applications. In most of these applications, the system consists of smart objects that are equipped by sensors and Radio Frequency Identification (RFID) and may rely on other technological computing and paradigm solutions such as M2 M (machine to machine) computing, Wifi, Wimax, LTE, cloud computing, etc. Thus, the IoT vision foresees that we can shift from traditional sensor networks to pervasive systems, which deliver intelligent automation by running services on objects. Actually, a significant attention has been given to designing a middleware that supports many features; heterogeneity, mobility, scalability, multiplicity, and security. This papers reviews the-state-of-the-art techniques for IoT middleware systems and reveals an interesting classification for these systems into service and agent-oriented systems. Therefore two visions have emerged to provide the IoT middleware systems: Via designing the middleware for IoT system as an eco-system of services or as an eco-system of agents. The most common feature of the two approaches is the ability to overcome heterogeneity issues. However, the agent approach provides context awareness and intelligent elements. The review presented in this paper includes a detailed comparison between the IoT middleware approaches. The paper also explores challenges that form directions for future research on IoT middleware systems. Some of the challenges arise, because some crucial features are not provided (or at most partially provided) by the existing middleware systems, while others have not been yet tackled by current research in IoT.

2016
El-Zawawy, M. A., "An Operational Semantics for Android Applications", 16th International Conference on Computational Science and Its Applications, Beijing, China, July 4-7, 2016. Abstract

The most common operating system for smart phones, which are among
the most common forms of computers today, is the Android operating
system. The Android applications are executed on Dalvik Virtual
Machines (DVMs) which are register-based, rather than stack-based
such as Java Virtual Machines (JVMs). The differences between DVMs
and JVMs make tools of programm analysis of JVMs are not directly
applicable to DVMs. Operational semantics is a main tool to study,
verify, and analyze Android applications.

This paper presents an accurate operational semantics
\textit{Android}$\mathcal{S}$ for Android programming. The set of
Dalvik instruction considered in the semantics is designed carefully
to capture main functionalities of Android programming and to enable
the use of semantics to evaluate method of Application analysis. The
semantics also simulates the interaction between users and
applications during application executions. The semantics also
respects constrains of state changes imposed by the life cycle of
Android applications.

El-Zawawy, M. A., "A Type System for Android Applications", 16th International Conference on Computational Science and Its Applications, Beijing, China, July 4-7, 2016. Abstract

The most common form of computers today is the hand held form and
specially smart phones and tablets. The platform for the majority of
smart phones is the Android operating system. Therefore analyzing
and verifying the Android applications become an issue of extreme
importance. However classical techniques of static analysis are not
applicable directly to Android applications. This is so because
typically Android applications are developed using Java code that is
translated into Java bytecode and executed using Dalvik virtual
machine. Also developing new techniques for static analysis of
Android applications is an involved problem due to many facts such
as the concept of gestures used in Android interaction with users.

One of the main tools of analyzing and verifying programs is types
systems~\cite{el2012heap}. This paper presents a new type system,
Android$\mathcal{T}$, which is specific to Android applications. The
proposed type system ensures the absence of errors like "method is
undefined". Also the type system is applicable to check the
soundness of static analyses of Android applications.

2015
2014
El-Zawawy, M. A., "Certified Transformation for Static Single Assignment of SPMD Programs", Proceedings of The 14th International Conference on Computational Science and Its Applications -- DOI: 10.1109/ICCSA.2014.15, Page(s): 12 -- 17, IEEE CONFERENCE PUBLICATIONS, Guimarães, Portugal, June 30 - July 3, 2014. AbstractCertified Transformation for Static Single Assignment of SPMD Programs.pdf

A common program view adapted by most contemporary compilers is Static Single Assignment (SSA) which can be realized as transitional form (TF). In SSA, each variable is modified by exactly one assignment. SSA is based on splitting variables of the original program into many versions. Power constraints of sequential programming led parallel programming to be the main programming style today for performance boosting. The single program, multiple data (SPMD) style of parallelism is a prevalent model of parallel computing. A Proof-Carrying Code package typically consists of the original code, a proof that is checkable by a machine, and the code’s correctness specification.

A new technique for constructing a static single assignment form for SPMD programs is introduced in this paper. The proposed technique is in the form of a system of inference rules. The input of our proposed technique is a SPMD program and the output is a SSA form of the program. Judgment derivations in the proposed system are convenient choices for proof parts of a PCC packages. Therefore the resulting SSA form is certified in terms of proof-carrying code area of research.

El-Zawawy, M. A., "ConNet: A Network Programming Language with Concurrency", Proceedings of The 14th International Conference on Computational Science and Its Applications -- DOI: 10.1109/ICCSA.2014.38, Page(s): 165 -- 170, IEEE CONFERENCE PUBLICATIONS , Guimarães, Portugal, June 30 - July 3, 2014. AbstractConNet: A Network Programming Language with Concurrency.pdf

Interdependent functionalities such as access authorizing, routing, traffic observing, and load adjusting are offered by today’s networks. Inconveniently, the existing languages for programming software defined networks do not provide parallelism to simulate the natural interdependence between common network functionalities. These languages are also not successful in providing a rudimentary solution to overcome the bad need for concurrency. This results in perplexed network programs.

This paper proposes ConNet, a model for a concurrent network programming langauge. This model is simple, yet powerful enough to express strong networking applications. The model is supported with a new operational semantics that is based on a new concept, the event of states concept. A type system to
guarantee type safety of ConNet programs is proposed in this paper as well. Mathematical formalization for the correctness of the type system is stated in the paper. Results of experiments checking efficiency of the language model are presented and discussed in the paper.

El-Zawawy, M. A., and A. I. AlSalem, "ImpNet: Programming Software-Defied Networks Using Imperative Techniques", WSEAS Transactions on Computers, vol. 13, no. Article# 35, pp. 402–413, June, 2014. AbstractImpNet: Programming Software-Defied Networks Using Imperative Techniques.pdf

Software and hardware components are basic parts of modern networks. However the software component is typical sealed and function-oriented. Therefore it is very difficult to modify these components. This badly affected networking innovations. Moreover, this resulted in network policies having complex interfaces that are
not user-friendly and hence resulted in huge and complicated flow tables on physical switches of networks. This
greatly degrades the network performance in many cases.
Software-Defined Networks (SDNs) is a modern architecture of networks to overcome issues mentioned above.
The idea of SDN is to add to the network a controller device that manages all the other devices on the network
including physical switches of the network. One of the main tasks of the managing process is switch learning;
achieved via programming physical switches of the network by adding or removing rules for packet-processing
to/from switches, more specifically to/from their flow tables.
A high-level imperative network programming language, called ImpNet, is presented in this paper. ImpNet enables writing efficient, yet simple, and powerful programs to run on the controller to control all other network devices including switches. ImpNet is compositional, simply-structured, expressive, and more importantly imperative. The syntax of ImpNet together two types of operational semantics to contracts of ImpNet are presented in the paper. The proposed semantics are of the static and dynamic types. Two modern application programmed using ImpNet are shown in the paper as well. The semantics of the applications are shown in the paper also.

El-Zawawy, M. A., and M. N. Alanazi, "Probabilistic Alias Analysis for Parallel Programming in SSA Forms", The 2014 International Conference on Software Engineering Research and Practice, Las Vegas, USA, July 21-24, 2014. Probabilistic Alias Analysis for Parallel Programming in SSA Forms.pdf
El-Zawawy, M. A., "Frequent Statement and Dereference Elimination for Imperative and Object-Oriented Distributed Programs", The Scientific World Journal, vol. 2014, ID 839121, pp. 13 pages, April, 2014. AbstractFrequent Statement and Dereference Elimination for Imperative and Object-Oriented Distributed Programs.pdf

This paper introduces new approaches for the analysis of frequent statement and dereference elimination for imperative and object oriented distributed programs running on parallel machines equipped with hierarchical memories.The paper uses languages whose address spaces are globally partitioned. Distributed programs allow defining data layout and threads writing to and reading from other thread memories. Three type systems (for imperative distributed programs) are the tools of the proposed techniques. The first type system defines for every program point a set of calculated (ready) statements and memory accesses.The second type system uses an enriched version of types of the first type system and determines which of the ready statements and memory accesses are used later in the program.The third type system uses the information gather so far to eliminate unnecessary statement computations and memory accesses (the analysis of frequent statement and dereference elimination). Extensions to these type systems are also presented to cover object-oriented distributed programs. Two advantages of our work over related work are the following.The hierarchical
style of concurrent parallel computers is similar to the memory model used in this paper. In our approach, each analysis result is assigned a type derivation (serves as a correctness proof).

El-Zawawy, M. A., and M. N. Alanazi, "An Efficient Binary Technique for Trace Simplifications of Concurrent Programs", Proceedings of The IEEE 6th International Conference on Adaptive Science \& Technology (ICAST), Ota, Nigeria, 29-31 Oct, 2014. An Efficient Binary Technique for Trace Simplifications of Concurrent Programs.pdf
El-Zawawy, M. A., and A. I. AlSalem, "ImNet: An Imperative Network Programming Language", Proceedings of The 14th International Conference on Applied Computer Science – Constantin Buzatu (Ed): ACS 2014, Modern Computer Applications in Science and Education, pp. 149-156, 2014. AbstractImNet: An Imperative Network Programming Language.pdf

One of the most recent architectures of networks is Software-Defined Networks (SDNs) using a controller appliance to control the set of switches on the network. The controlling process includes installing or uninstalling packet-processing rules on flow tables of switches.
This paper presents a high-level imperative network programming language, called ImNet, to facilitate writing
efficient, yet simple, programs executed by controller to manage switches. ImNet is simply-structured, expressive, compositional, and imperative. This paper also introduces an operational semantics to ImNet. Detailed examples of programs (with their operational semantics) constructed in ImNet are illustrated in the paper as well.

El-Zawawy, M. A., "Proof-Carrying Model for Parsing Techniques", 14th International Conference On Computational Science and Its Applications - {ICCSA} 2014 - , Guimarães, Portugal, June 30 - July 3, 2014, Proceedings, Part {V}, vol. 8583: Lecture Notes in Computer Science, Springer, pp. 1–14, 2014. AbstractProof-Carrying Model for Parsing Techniques.pdf

This paper presents new approaches to common parsing algorithms. The new approach utilizes the concept of inference rule. Therefore the new approach is simple, yet powerful enough to overcome the performance of traditional techniques. The new approach is basically composed of systems of inference rules.
Mathematical proofs of the equivalence between proposed systems and classical algorithms are outlined in the paper. The proposed technique provides a correctness verification (a derivation of inference rules) for each parsing process. These verifications are required in modern applications such as mobile computing. Results of experimental proving the efficiency of the proposed systems and their produced verifications are shown in the paper.

El-Zawawy, M. A., "Testing Automation of Context-Oriented Programs Using Separation Logic", Applied Computational Intelligence and Soft Computing, vol. 2014 , issue 2014, Article ID 930186, pp. 8 pages, 2014. AbstractTesting Automation of Context-Oriented Programs Using Separation Logic.pdf

A new approach for programming that enables switching among contexts of commands during program execution is context-oriented programming (COP). This technique is more structured and modular than object-oriented and aspect-oriented programming and hence more flexible. For context-oriented programming, as implemented in COP languages such as ContextJ* and ContextL, this paper introduces accurate operational semantics. The language model of this paper uses Java concepts and is equipped with layer techniques for activation/deactivation of layer contexts. This paper also presents a logical system for COP programs. This logic is necessary for the automation of testing, developing, and validating of partial correctness specifications for COP programs and is an extension of separation logic. A mathematical soundness proof for the logical system against the proposed operational semantics is presented in the paper.

2013
El-Zawawy, M. A., and E. A. Aleisa, "A new model for Context-Oriented Programs", Life Science Journal, vol. 10, no. 2, pp. 2515-2523, June, 2013. AbstractA new model for Context-Oriented Programs.pdf

Context-oriented programming (COP) is a new technique for programming that allows changing the context in which commands execute as a program executes. Compared to object-oriented programming (aspect-oriented programming), COP is more flexible (modular and structured). This paper presents a precise syntax-directed operational semantics for context-oriented programming with layers, as realized by COP languages like ContextJ* and ContextL. Our language model is built on Java enriched with layer concepts and activation and deactivation of layer scopes. The paper also presents a static type system that guarantees that typed programs do not get stuck. Using the means of the proposed semantics, the mathematical correctness of the type system is presented in the paper.

El-Zawawy, M. A., "Distributed Data and Programs Slicing", Life Science Journal, vol. 10, no. 4, pp. 1361-1369, December, 2013. AbstractDistributed Data and Programs Slicing.pdf

This paper presents a new technique for data slicing of distributed programs running on a hierarchy of machines. Data slicing can be realized as a program transformation that partitions heaps of machines in a hierarchy into independent regions. Inside each region of each machine, pointers preserve the original pointer structures in the original heap hierarchy. Each heap component of the base type (e.g., the integer type) goes only to a region of one of the heaps. The proposed technique has the shape of a system of inference rules. In addition, this paper presents a simply structure type system to decide type soundness of distributed programs. Using this type system, a mathematical proof that the proposed slicing technique preserves typing properties is outlined in this paper as well.

El-Zawawy, M. A., "Detection of Probabilistic Dangling References in Multi-core Programs Using Proof-Supported Tools", 13th International Conference On Computational Science and Its Applications - ICCSA 2013 - Ho Chi Minh City, Vietnam, June 24-27, 2013, Proceedings, Part VICCSA (5), vol. 7975: Lecture Notes in Computer Science, Springer, pp. 516-530, 2013. AbstractDetection of Probabilistic Dangling References in Multi-core Programs Using Proof-Supported Tools.pdf

This paper presents a new technique for detection of probabilistic dangling references in multi-core programs. The technique has the form of a simply structured type system and provides a suitable framework for proof-carrying code applications like mobile code applications that have limited resources. The type derivation of each individual analysis serves as a proof for the correctness of the analysis. The type system is designed to analyze parallel programs with structured concurrent constructs: fork-join constructs, conditionally spawned cores, and parallel loops.
For a given program S, a probabilistic threshold pms, and a probabilistic reference analysis for S, if S is well-typed in our proposed type system then all computational paths with probabilities greater than or equal to pms will contain no dangling pointers at run time. The soundness of the presented type system is proved in this paper with respect to a probabilistic operational semantics to our model language.

El-Zawawy, M. A., "Frequent Statement and De-reference Elimination for Distributed Programs", 13th International Conference On Computational Science and Its Applications - ICCSA 2013 - Ho Chi Minh City, Vietnam, June 24-27, 2013, Proceedings, Part III, ICCSA (3), vol. 7973: Lecture Notes in Computer Science, Springer, pp. 82-97, 2013. AbstractFrequent Statement and De-reference Elimination for Distributed Programs.pdf

This paper introduces a new approach for the analysis of frequent statement and de-reference elimination for distributed programs run on parallel machines equipped with hierarchical memories. The address space of the language studied in the paper is globally partitioned. This language allows programmers to define data layout and threads which can write to and read from other thread memories.
Simply structured type systems are the tools of the techniques presented in this paper which presents three type systems. The first type system defines for program points of a given distributed program sets of calculated (ready) statements and memory accesses. The second type system uses an enriched version of types of the first type system and determines which of the specified statements and memory accesses are used later in the program. The third type system uses the information gather so far to eliminate unnecessary statement computations and memory accesses (the analysis of frequent statement and de-reference elimination).
Two advantages of our work over related work are the following. The hierarchical style of concurrent parallel computers is similar to the memory model used in this paper. In our approach, each analysis result is assigned a type derivation (serves as a correctness proof).

2012
El-Zawawy, M. A., "Recognition of Logically Related Regions Based Heap Abstraction", Journal of the Egyptian Mathematical Society, vol. 20, no. 2, pp. 64-71, September, 2012. AbstractRecognition of Logically Related Regions Based Heap Abstraction.pdf

This paper presents a novel set of algorithms for heap abstraction, identifying logically related regions of the heap. The targeted regions include objects that are part of the same component structure (recursive data structure). The result of the technique outlined in this paper has the form of a compact normal form (an abstract model) that boosts the efficiency of the static analysis via speeding its convergence. The result of heap abstraction, together with some properties of data structures, can be used to enable program optimizations like static deallocation, pool allocation, region-based garbage collection, and object co-location. More precisely, this paper proposes algorithms for abstracting heap components with the layout of a singly linked list, a binary tree, a cycle, and a directed acyclic graph. The termination and correctness of these algorithms are studied in the paper. Towards presenting the algorithms the paper also presents concrete and abstract models for heap representations.

El-Zawawy, M. A., and N. M. Daoud, "Dynamic Verification for File Safety of Multithreaded Programs", IJCSNS International Journal of Computer Science and Network Security, vol. 12, no. 5, pp. 14-20, May, 2012. AbstractDynamic Verification for File Safety of Multithreaded Programs.pdf

In this paper, we present a new semantics to check file safety of multithreaded programs. A file-safe program is one that reaches a final configuration under the proposed semantics. We extend the While language with file operations and multi-threading commands, and call the new language whilef. This paper shows that the file safety is an un-decidable property for whilef. The file safety becomes a decidable property in a special case shown in this paper. The case happens when users provide pointer information. If the file is safe we call it a strongly safe file program. We modify the syntax and the semantic of the language and called it SafeWhilef.

El-Zawawy, M. A., and N. M. Daoud, "New Error-recovery Techniques for Faulty-Calls of Functions", Computer and Information Science, vol. 5, no. 3, pp. 67-75, May, 2012. AbstractNew Error-recovery Techniques for Faulty-Calls of Functions.pdf

In this paper, we introduce type systems to detect faulty calls of functions in a program. The intended meaning of the faulty call is calling a function with a miss-match to the number of its arguments. We use error-detecting semantics that when detects the faulty calls, doesn't proceed to the next state. Type systems are used in the process of analysis and in repairing. The paper presents two type systems: the safety type system which checks the safety of a given program and the repairing type system which corrects errors. The repairing process is made by replacing the faulty call of function with a correct one. In the repairing process simple interactive input/output statements are used. The interaction (input/output) helps to get the lost parameters by interacting with the user; informing him about the number of lost parameters. The user can then input these parameters.

El-Zawawy, M. A., and H. A. Nayel, "Type Systems Based Data Race Detector", IJCSNS International Journal of Computer Science and Network Security, vol. 5, no. 4, pp. 53-60, July, 2012. AbstractType Systems Based Data Race Detector.pdf

Multi-threading is a methodology that has been extremely used. Modern software depends essentially on multi-threading. Operating systems, famous examples, are based on multi-threading; a user can write his document, play an audio file, and downloading a file from internet at the same time. Each of these tasks called a thread. A common problem occurs when implementing multi-threaded programs is a data-race. Data race occurs when two threads try to access a shared variable at the same time without a proper synchronization. A detector is software that determines if the program contains a data-race problem or not. In this paper, we develop a detector that has the form of a type system. We present a type system which discovers the data-race problems. We also prove the soundness of our type system.

El-Zawawy, M. A., "Dead code elimination based pointer analysis for multithreaded programs", Journal of the Egyptian Mathematical Society, vol. 20, no. 1, pp. 28-37, January, 2012. AbstractDead code elimination based pointer analysis for multithreaded programs.pdf

This paper presents a new approach for optimizing multitheaded programs with pointer constructs. The approach has applications in the area of certified code (proof-carrying code) where a justification or a proof for the correctness of each optimization is required. The optimization meant here is that of dead code elimination. Towards optimizing multithreaded programs the paper presents a new operational semantics for parallel constructs like join-fork constructs, parallel loops, and conditionally spawned threads. The paper also presents a novel type system for flow-sensitive pointer analysis of multithreaded programs. This type system is extended to obtain a new type system for live-variables analysis of multithreaded programs. The live-variables type system is extended to build the third novel type system, proposed in this paper, which carries the optimization of dead code elimination. The justification mentioned above takes the form of type derivation in our approach.

El-Zawawy, M. A., "Abstraction Analysis and Certified Flow and Context Sensitive Points-to Relation for Distributed Programs", 12th International Conference Computational Science and Its Applications, ICCSA 2012, Salvador de Bahia, Brazil, June 18-21, 2012, Proceedings, Part IV, ICCSA (4), Lecture Notes in Computer Science, vol. 7336: Springer, pp. 83-99, 2012. AbstractAbstraction Analysis and Certified Flow and Context Sensitive Points-to Relation for Distributed Programs.pdf

This paper presents a new technique for pointer analysis of distributed programs executed on parallel machines with hierarchical memories. One motivation for this research is the languages whose global address space is partitioned. Examples of these languages are Fortress, X10, Titanium, Co-Array Fortran, UPC, and Chapel. These languages allow programmers to adjust threads and data layout and to write to and read from memories of other threads. The techniques presented in this paper have the form of type systems which are simply structured. The proposed technique is shown on a language which is the while langauge enriched with basic commands for pointer manipulations and also enriched with commands vital for distributed execution of programs. An abstraction analysis that for a given statement calculates the set of function abstractions that the statement may evaluate-to is introduced in this paper. The abstraction analysis is needed in the proposed pointer analysis. The mathematical soundness of all techniques presented in this paper are discussed. The soundness is proved against a new operational semantics presented in this paper. Our work has two advantages over related work. In our technique, each analysis result is associated with a correctness proof in the form of type derivation. The hierarchical memory model used in this paper is in line with the hierarchical character of concurrent parallel computers.

El-Zawawy, M. A., "Heap Slicing Using Type Systems", 12th International Conference Computational Science and Its Applications, ICCSA 2012, Salvador de Bahia, Brazil, June 18-21, 2012, Proceedings, Part III, ICCSA (3), Lecture Notes in Computer Science, vol. 7335: Springer, pp. 592-606, 2012. AbstractHeap Slicing Using Type Systems.pdf

Using type systems, this paper treats heap slicing which is a technique transforming a program into a new one that produces the same result while working on a heap sliced into independent regions. Heap slicing is a common approach to handle the problem of modifying the heap layout without changing the program semantics. Heap slicing has applications in the areas of performance optimization and security. Towards solving the problem of heap slicing, this paper introduces three type systems. The first type system does a pointer analysis and annotates program points with pointer information. This type system is an augmentation of a previously developed type system by the author. The second type system does a region analysis and refines the result of the first type system by augmenting the pointer information with region information. The region information approximately specifies at each program point for each memory cell the region where the cell exists. The third type system uses the information gathered by the region type system to do the principal transformation of heap slicing. The paper also presents two operational semantics; one for single-region heap scenario and the other for multi-regions heap scenario. These semantics are used to prove the soundness of the type systems.

2011
El-Zawawy, M. A., and H. A. Nayel, "Partial Redundancy Elimination for Multi-threaded Programs", IJCSNS International Journal of Computer Science and Network Security, vol. 11, no. 10, pp. 127-133, October, 2011. AbstractPartial Redundancy Elimination for Multi-threaded Programs.pdf

Multi-threaded programs have many applications which are widely used such as operating systems. Analyzing multi-threaded programs differs from sequential ones; the main feature is that many threads execute at the same time. The effect of all other running threads must be taken in account. Partial redundancy elimination is among the most powerful compiler optimizations: it performs loop-invariant code motion and common subexpression elimination. We present a type system with optimization component which performs partial redundancy elimination for multi-threaded programs.

El-Zawawy, M. A., "Program Optimization Based Pointer Analysis and Live Stack-Heap Analysis", International Journal of Computer Science Issues, vol. 8, no. 2, pp. 98-107, March, 2011. AbstractProgram Optimization Based Pointer Analysis and Live Stack-Heap Analysis.pdf

In this paper, we present type systems for flow-sensitive pointer analysis, live stack-heap (variables) analysis, and program optimization. The type system for live stack-heap analysis is an enrichment of that for pointer analysis; the enrichment has the form of a second component being added to types of the latter system. Results of pointer analysis are proved useful via their use in the type system for live stack-heap analysis. The type system for program optimization is also an augmentation of that for live stack-heap analysis, but the augmentation takes the form of a transformation component being added to inference rules of the latter system. The form of program optimization being achieved is that of dead-code elimination. A form of program correction may result indirectly from eliminating faulty code (causing the program to abort) that is dead. Therefore program optimization can result in program correction. Our type systems have the advantage of being compositional and relatively-simply structured. The novelty of our work comes from the fact that our type system for program optimization associates the optimized version of a program with a justification (in the form of a type derivation) for the optimization. This justification is pretty much appreciated in many research areas like certified code (proof-carrying code) which is the motivation of this work.

El-Zawawy, M. A., "Probabilistic Pointer Analysis for Multithreaded Programs", ScienceAsia, vol. 37, no. 4, pp. 344-354, December, 2011. AbstractProbabilistic Pointer Analysis for Multithreaded Programs.pdf

The use of pointers and data-structures based on pointers results in circular memory references that are interpreted by a vital compiler analysis, namely pointer analysis. For a pair of memory references at a program point, a typical pointer analysis specifies if the points-to relation between them may exist, definitely does not exist, or definitely exists. The "may be" case, which describes the points-to relation for most of the pairs, cannot be dealt with by most compiler optimizations. This is so to guarantee the soundness of these optimizations. However, the "may be" case can be capitalized by the modern class of speculative optimizations if the probability that two memory references alias can be measured. Focusing on multithreading, a prevailing technique of programming, this paper presents a new flow-sensitive technique for probabilistic pointer analysis of multithreaded programs. The proposed technique has the form of a type system and calculates the probability of every points-to relation at each program point. The key to our approach is to calculate the points-to information via a post-type derivation. The use of type systems has the advantage of associating each analysis results with a justification (proof) for the correctness of the results. This justification has the form of a type derivation and is very much required in applications like certified code.

El-Zawawy, M. A., "Flow Sensitive-Insensitive Pointer Analysis Based Memory Safety for Multithreaded Programs", 11th International Conference Computational Science and Its Applications, ICCSA 2011, Cantabria, Santander, Spainl, June 20-23, 2011, Proceedings, Part VI, ICCSA (5), Lecture Notes in Computer Science, vol. 6786: Springer, pp. 355-369, 2011. AbstractFlow Sensitive-Insensitive Pointer Analysis Based Memory Safety for Multithreaded Programs.pdf

The competency of pointer analysis is crucial for many compiler optimizations, transformations, and checks like memory safety. The potential interaction between threads in multithreaded programs complicates their pointer analysis and memory-safety check. The trade-off between accuracy and scalability remains a main issue when studying these analyses. In this work, we present novel approaches for the pointer analysis and memory safety of multithreaded programs as simply structured type systems. In order to balance accuracy and scalability, the type system proposed for pointer analysis of multithreaded programs is flow-sensitive and it invokes another flow-insensitive type system for parallel constructs. Therefore the proposed pointer analysis is described as flow sensitive-insensitive. The third type system presented in this paper takes care of memory safety of multithreaded programs and is an extension of the type system of pointer analysis. Programs having types in memory-safety type system, are guaranteed to be memory safe. Type derivations serve as proofs for correctness of the result of every pointer analysis and memory-safety check. Such proofs are required in the area of proof-carrying code.

2007
El-Zawawy, M. A., Semantic spaces in Priestley form, , PhD thesis, Birmingham, University of Birmingham, UK, January, 2007. AbstractSemantic spaces in Priestley form.pdf

The connection between topology and computer science is based on two fundamental in- sights: the rst, which can be traced back to the beginning of recursion theory, and even intuitionism, is that computable functions are necessarily continuous when input and out- put domains are equipped with their natural topologies. The second, due to M. B. Smyth in 1981, is that the observable properties of computational domains are contained in the collection of open sets. The rst insight underlies Dana Scott's categories of semantics domains, which are certain topological spaces with continuous functions. The second in- sight was made fruitful for computer science by Samson Abramsky, who showed in his “Domain Theory in Logical Form” that instead of working with Scott's domains one can equivalently work with lattices of observable properties. Thus he established a precise link between denotational semantics and program logic. Mathematically, the framework for Abramsky's approach is that of Stone duality, which in general terms studies the relationship between topological spaces and their lattices of opens sets. While for his purposes, Abramsky could rely on existing duality results estab- lished by Stone in 1937, it soon became clear that in order to capture continuous domains, the duality had to be extended. Continuous domains are of interest to semantics because of the need to model the probabilistic behaviour and computation over real numbers. The extension of the Stone duality was achieved by Jung and Sunderhauf ¨ in 1996; the main out- come of this investigation is the realisation that the observable properties of a continuous space form a strong proximity lattice. The present thesis examines strong proximity lattices with the tools of Priestley duality, which was introduced in 1970 as an alternative to Stone's duality for distributive lattices. The advantage of Priestley duality is that it yields compact Hausdorff spaces and thus stays within classical topological ideas. The thesis shows that Priestley duality can indeed be extended to cover strong prox- imity lattices, and identies the additional structure on Priestley spaces that corresponds to the proximity relation. At least three different types of morphism have been dened between strong proximity lattices, and the thesis shows that each of them can be used in Priestley duality. The resulting maps between Priestley spaces are characterised and given a computational interpretation. This being an alternative to the Jung–Sunderhauf ¨ duality, it is examined how the two dualities are related on the side of topological spaces. Finally, strong proximity lattices can be seen as algebras of the logic MLS, introduced by Jung, Kegelmann, and Moshier. The thesis examines how the central notions of MLS are transformed by Priestley duality.

2006
El-Zawawy, M. A., and A. Jung, "Priestley duality for strong proximity lattices", Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXII), eds S. Brookes and M. Mislove, , Genova, Italy, Electronic Notes in Theoretical Computer Science, vol. 158, pp. 199-217, 2006. AbstractPriestley duality for strong proximity lattices.pdf

In 1937 Marshall Stone extended his celebrated representation theorem for Boolean algebras to distributive lattices. In modern terminology, the representing topological spaces are zero-dimensional stably compact, but typically not Hausdorff. In 1970, Hilary Priestley realised that Stone's topology could be enriched to yield order-disconnected compact ordered spaces.

In the present paper, we generalise Priestley duality to a representation theorem for strong proximity lattices. For these a “Stone-type” duality was given in 1995 in joint work between Philipp Sünderhauf and the second author, which established a close link between these algebraic structures and the class of all stably compact spaces. The feature which distinguishes the present work from this duality is that the proximity relation of strong proximity lattices is “preserved” in the dual, where it manifests itself as a form of “apartness.” This suggests a link with constructive mathematics which in this paper we can only hint at. Apartness seems particularly attractive in view of potential applications of the theory in areas of semantics where continuous phenomena play a role; there, it is the distinctness between different states which is observable, not equality.

The idea of separating states is also taken up in our discussion of possible morphisms for which the representation theorem extends to an equivalence of categories.

2005
El-Zawawy, M. A., and A. Jung, Priestley representations for strong proximity lattices and stably compact spaces, , Birmingham , Technical Report CSR-05-3, University of Birmingham, School of Computer Science, April , 2005. Priestley representations for strong proximity lattices and stably compact spaces.pdf
2002
El-Sharkawi, M. E., and M. A. El-Zawawy, "Algorithm for spatial clustering with obstacles", In Proc. 2002 ICICIS Int. Conference on Intelligent Computing and Information Systems (ICICIS’02), Cairo, Egypt, June, 2002. AbstractAlgorithm for spatial clustering with obstacles.pdf

In this paper, we propose an efficient clustering technique to solve the problem of clustering in the presence of obstacles. The proposed algorithm divides the spatial area into rectangular cells. Each cell is associated with statistical information that enables us to label the cell as dense or non-dense. We also label each cell as obstructed (i.e. intersects any obstacle) or non-obstructed. Then the algorithm finds the regions (clusters) of connected, dense, non-obstructed cells. Finally, the algorithm finds a center for each such region and returns those centers as centers of the relatively dense regions (clusters) in the spatial area.

El-Zawawy, M. A., Efficient techniques for mining spatial databases, , M.Sc. thesis, Cairo, Egypt, Department of Mathematics, Faculty of Science, Cairo University, 2002. AbstractEfficient techniques for mining spatial databases.pdf

Clustering is one of the major tasks in data mining. In the last few years, Clustering of spatial data has received a lot of research attention. Spatial databases are components of many advanced information systems like geographic information systems VLSI design systems. In this thesis, we introduce several efficient algorithms for clustering spatial data. First, we present a grid-based clustering algorithm that has several advantages and comparable performance to the well known efficient clustering algorithm. The algorithm has several advantages. The algorithm does not require many input parameters. It requires only three parameters, the number of the points in the data space, the number of the cells in the grid and a percentage. The number of the cells in the grid reflects the accuracy that should be achieved by the algorithm. The algorithm is capable of discovering clusters of arbitrary shapes. The computational complexity of the algorithm is comparable to the complexity of the most efficient clustering algorithm. The algorithm has been implemented and tested against different ranges of database sizes. The performance results show that the running time of the algorithm is superior to the most well known algorithms (CLARANS [23]). The results show also that the performance of the algorithm do not degrade as the number of the data points increases.

2001
El-Zawawy, M. A., and M. E. El-Sharkawi, "Clustering with obstacles in spatial databases", In Proc. 2001 IEEE Int. Symposium of Signal Processing and Information Technology (ISSPIT’01), pages 420-425, Cairo, Egypt, December, 2001. AbstractClustering with obstacles in spatial databases.pdf

Clustering large spatial databases is an important problem, which tries to find the densely populated regions in a spatial area to be used in data mining, knowledge discovery, or efficient information retrieval. However most algorithms have ignored the fact that physical obstacles such as rivers, lakes, and highways exist in the real world and could thus affect the result of the clustering. In this paper, we propose CPO, an efficient clustering technique to solve the problem of clustering in the presence of obstacles. The proposed algorithm divides the spatial area into rectangular cells. Each cell is associated with statistical information used to label the cell as dense or non-dense. It also labels each cell as obstructed (i.e. intersects any obstacle) or nonobstructed. For each obstructed cell, the algorithm finds a number of non-obstructed sub-cells. Then it finds the dense regions of non-obstructed cells or sub-cells by a breadthfirst search as the required clusters with a center to each region.