http://research-fadi.aub.edu.lb/dkwk/ 2020-07-15T14:03:13+00:00 http://research-fadi.aub.edu.lb/dkwk/ http://research-fadi.aub.edu.lb/dkwk/lib/images/favicon.ico text/html 2015-02-21T13:51:11+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=biptoabc&rev=1424526671&do=diff Behavior-Interaction-Priority (BIP) is a layered embedded system design and verification framework that provides separation of functionality, synchronization, and priority concerns to simplify system design and to establish correctness by construction. BIP framework comes with a runtime engine and a suite of verification tools that use D-Finder and NuSMV as model checkers. text/html 2012-12-28T15:41:42+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=eece797&rev=1356709302&do=diff EECE 797 Seminar, Fall 2012 Thursday Dec 20, 2012 Title: How to Outsource Computations to Untrusted Helpers Dr. Ghassan Karame, Research Scientist NEC, Germany Abstract: The secure outsourcing of computations proves to be useful in a number of application-scenarios. Techniques for securely outsourcing computations can, for instance, be used in mobile and cloud computing settings to verify the integrity of remote computations. The outsourcing of computations also finds applicability in cons… text/html 2009-10-12T14:59:25+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=fyp0910&rev=1255359565&do=diff Suggestions for Final Year Projects for the academic year 2009-2010 Media Search Do you own a digital camera? How many times did you look for half an hour at your own collection of digital photos and videos to find one photo or few seconds of video. This project aims at automating the search for personal images on your local hard disk. Google, Microsoft among other companies are working on solving this problem at large for an infinity of images on the web. We will solve a smaller proble… text/html 2010-09-28T11:06:57+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=fyp1011&rev=1285672017&do=diff The following are suggestions for final year projects that I am willing to supervise for the year 2010/2011. I am allowed to supervise only three projects. If you are interested please pass by my office to discuss the projects as well as your interests. text/html 2019-09-16T15:15:26+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=fypideas&rev=1568646926&do=diff CME Offshore Project 1: Arabic keywords extractor This project requires knowledge of the following subjects: * Software Engineer: * - Ordered List Item * - Python Stack * - Python NLP toolkits, like Spacy, Gensim, NLTK. * - Machine Learning and Deep Learning NLP. text/html 2017-02-16T16:08:07+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=guicop&rev=1487261287&do=diff GUICop: Approach and Toolset for Specification-based GUI Testing Authors Dalal Hammoud, Fadi A. Zaraket, and Wes Masri American University of Beirut Electrical and Computer Engineering Department Beirut, Lebanon 1107 2020 e-mail: {dsh07, fz11, wm13}@aub.edu.lb text/html 2020-07-13T12:31:22+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=ldfcbip&rev=1594643482&do=diff FORTE 2013: P.C Attie, S. Bensalem, M. Bozga, M. Jaber, J. Sifakis, and F. Zaraket We present a sound but incomplete criterion for checking deadlock-freedom of large systems expressed in BIP: a component-based framework for the construction of complex distributed systems. Since deciding deadlock-freedom for finite-state concurrent systems is PSPACE-complete, our criterion gives up completeness in return for tractability of evaluation. Our criterion can be evaluated by model-checking subsystems … text/html 2013-06-03T15:57:37+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=ltlsyn&rev=1370275057&do=diff Mohamad Noureddine, Fadi A. Zaraket, American University of Beirut Ali S. Elzein, IBM Systems and Technology, elzein@us.ibm.com Abstract Synthesis techniques take realizable Linear Temporal Logic specifications and produce correct circuits that implement the specifications. The generated circuits can be used directly in logic designs, and can also be used as miters that check the correctness of a design. Typically, those techniques generate a non-deterministic finite state automata an… text/html 2014-06-13T13:41:18+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=mosaic&rev=1402666878&do=diff From 01/01/2014 to 31/12/2015 Cooperation with Mediterranean Partners to build Opportunities around ICT and Societal and Industrial Challenges of Horizon 2020. The MOSAIC project aims to foster R&D cooperation between Europe and Mediterranean Partner Countries under European and third country programmes. MOSAIC focuses on Information and Communication Technologies (ICT) and how ICT can support common EU-MED societal challenges among which are Health and Wellbeing, Food and Agriculture, Clean … text/html 2015-11-20T14:22:58+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=pbcov&rev=1448029378&do=diff ABSTRACT Coverage metrics answer the question of whether we adequately checked a given software program. For example, statement coverage metrics measure how many and how often lines of code were executed. Path coverage metrics measure the frequency of execution of interleaving branches of code. Data flow coverage metrics compute computational and predicate use of data paths. In recent years, researchers introduced effective static analysis techniques for checking the correctness of software pr… text/html 2015-04-30T10:47:51+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=pmax&rev=1430390871&do=diff Fadi A. Zaraket, Majd Olleik, Ali Yassine --- American University of Beirut Abstract This paper presents a conceptual framework and a mathematical formulation for software resource allocation and project selection at the level of software skills. First, we introduce a skill-based framework that considers universities, software companies, and potential projects of a country. Based on this framework, we formulate a linear integer program PMAX which determines the selection of projects and the a… text/html 2018-06-14T09:42:42+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=progress&rev=1528969362&do=diff The following is a list of mature projects that we are working on. Some of them are already available in a technical report form under Arxiv. Specification Construction Using Behaviours, Equivalences, and SMT Solvers. Paul C. Attie, Fadi A. Zaraket text/html 2018-06-14T09:42:10+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=publications&rev=1528969330&do=diff Under review * Ali Alawieh, Zahraa Sabra, Amani Jaber, Hussein Hayek, Fadi Zaraket, and Ghassan Hamadeh, “MENA-AMTC: Middle East and North Africa Annotated Medical Text Corpora”, BMC Bioinformatics * Mustafa Jarrar,Fadi zaraket, Rami Asia, HamZeh Amayreh, “Diacritic-Based Matching of Arabic Words”, ACM Transactions on TALLIP * Other mature work in progress text/html 2014-09-06T16:13:32+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=speccheck&rev=1410020012&do=diff Spec Construct Paul Attie, Fadi Zaraket, Mohamad Noureddine, and Farah Al-Hariri abstract The problem of writing a functional specification which re- flects the intentions of the developer has long been recognized as fun- damental. We propose a method to construct (synthesize) a functional specification for a terminating program which takes a single input and produces a single output. The specification consists of a precondition and a postcondition, expressed as first-order logic wff’s, inc… text/html 2018-01-25T09:23:45+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=start&rev=1516872225&do=diff At PCA-Lab we build theories and supporting tools to enhance program correctness automation. The theories define (1) program data elements such as types, operations and relations, (2) program control elements such as conditionals, loops and functions, and (3) program correctness elements such as test cases, oracles, coverage criteria, assertions, pre-conditions, post-conditions and invariants. The aim is to establish that the program data and control elements satisfy the program correctness el… text/html 2015-06-10T15:38:40+00:00 http://research-fadi.aub.edu.lb/dkwk/doku.php?id=ucov&rev=1433950720&do=diff Authors Rawad Abou Assi, Wes Masri, and Fadi A. Zaraket, American University of Beirut Abstract The goal of regression testing is to ensure that the behavior of existing code, believed correct by previous testing, is not altered by new program changes. We argue that the primary focus of regression testing should be on code associated with: