![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Kaïs Klai
Person information
- affiliation: University of Paris 13, France
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
- [c69]Nour Elhouda Souid, Kais Klai, Chiheb Ameur Abid, Samir Ben Ahmed:
Enforcing the Opacity of Modular Discrete Event Systems Using Supervisory Control. CoDIT 2023: 1990-1995 - [c68]Kais Klai
, Mohamed Taha Bennani
, Jaime Arias
, Jörg Desel, Hanen Ochi
:
Symbolic Observation Graph-Based Generation of Test Paths. TAP 2023: 127-146 - [c67]Ikram Garfatta, Nour Elhouda Souid, Kaïs Klai:
Towards Formal Verification of Node RED-Based IoT Applications. VECoS 2023: 90-104 - 2022
- [c66]Nour Elhouda Souid, Kais Klai, Chiheb Ameur Abid, Samir Ben Ahmed:
Hyper Symbolic Observation Graph to Enforce Opacity of Discrete Event Systems using Supervisory Control. CoDIT 2022: 1397-1402 - [c65]Nour Elhouda Souid, Kais Klai, Chiheb Ameur Abid, Samir Ben Ahmed:
At Design-Time Approach for Supervisory Control of Opacity. CoopIS 2022: 37-54 - [c64]Hanen Ochi, Kais Klai:
Checking Composition-Aware Service Substitutability. ISPA/BDCloud/SocialCom/SustainCom 2022: 845-853 - [c63]Nour Elhouda Souid, Kais Klai, Chiheb Ameur Abid, Samir Ben Ahmed:
Optimal Supervisory Control of Opacity for Modular Systems. ISPA/BDCloud/SocialCom/SustainCom 2022: 854-861 - [c62]Ikram Garfatta, Kaïs Klai, Mohamed Graïet, Walid Gaaloul:
Model checking of vulnerabilities in smart contracts: a solidity-to-CPN approach. SAC 2022: 316-325 - 2021
- [c61]Rania Ben Halima, Kais Klai, Mohamed Sellami, Zakaria Maamar
:
Formal Modeling and Verification of Property-based Resource Consumption Cycles. SCC 2021: 370-375 - [c60]Ikram Garfatta, Kais Klai, Walid Gaaloul, Mohamed Graiet:
A Survey on Formal Verification for Solidity Smart Contracts. ACSW 2021: 3:1-3:10 - [c59]Nour Elhouda Souid, Kais Klai:
A Novel Approach for Supervisor Synthesis to Enforce Opacity of Discrete Event Systems. ICICS (2) 2021: 210-227 - [c58]Ikram Garfatta, Kaïs Klai, Mohamed Graïet, Walid Gaaloul:
Model Checking of Solidity Smart Contracts Adopted for Business Processes. ICSOC 2021: 116-132 - [c57]Kais Klai, Chiheb Ameur Abid, Jaime Arias
, Sami Evangelista:
Hybrid Parallel Model Checking of Hybrid LTL on Hybrid State Space Representation. VECoS 2021: 27-42 - [c56]Ikram Garfatta, Kaïs Klai, Mohamed Graïet, Walid Gaaloul:
A Solidity-to-CPN Approach Towards Formal Verification of Smart Contracts. WETICE 2021: 69-74 - 2020
- [c55]Ikram Garfatta, Kaïs Klai, Mahamed Graïet, Walid Gaaloul:
Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach. ICSOC Workshops 2020: 47-53 - [c54]Chiheb Ameur Abid, Kaïs Klai, Jaime Arias
, Hiba Ouni:
SOG-Based Multi-Core LTL Model Checking. ISPA/BDCloud/SocialCom/SustainCom 2020: 9-17
2010 – 2019
- 2019
- [c53]Hiba Ouni, Kais Klai, Chiheb Ameur Abid, Belhassen Zouari:
Towards Parallel Verification of Concurrent Systems using the Symbolic Observation Graph. ACSD 2019: 23-32 - [c52]Amina Bourouis, Kais Klai, Nejib Ben Hadj-Alouane
:
Measuring Opacity for Non-Probabilistic DES: a SOG-Based Approach. ICECCS 2019: 242-247 - [c51]Hiba Ouni, Kais Klai, Belhassen Zouari:
Parallel construction of the Symbolic Observation Graph. HPCS 2019: 1011-1013 - [c50]Rakesh Jain, Kais Klai, Samir Tata:
Formal Modeling and Verification of Scalable Process-Aware Distributed IoT Applications. ISPA/BDCloud/SocialCom/SustainCom 2019: 263-270 - 2018
- [j10]Abderraouf Boussif, Mohamed Ghazel
, Kais Klai:
Fault diagnosis of discrete-event systems based on the symbolic observation graph. Int. J. Crit. Comput. Based Syst. 8(2): 141-168 (2018) - [c49]Hiba Ouni, Kais Klai, Chiheb Ameur Abid, Belhassen Zouari:
Reducing Time and/or Memory Consumption of the SOG Construction in a Parallel Context. ISPA/IUCC/BDCloud/SocialCom/SustainCom 2018: 147-154 - [c48]Ikram Garfatta, Kais Klai, Mohamed Graiet, Walid Gaaloul
:
Formal Modelling and Verification of Cloud Resource Allocation in Business Processes. OTM Conferences (1) 2018: 552-567 - [c47]Souha Boubaker, Kais Klai, Hedi Kortas, Walid Gaaloul
:
A Formal Model for Business Process Configuration Verification Supporting OR-Join Semantics. OTM Conferences (1) 2018: 623-642 - [c46]Ikram Garfatta, Kais Klai, Mohamed Graiet, Walid Gaaloul
:
[WiP] Formal Modelling of IT Resource Allocation in Business Processes. SOCA 2018: 227-232 - 2017
- [j9]Amina Bourouis
, Kais Klai, Nejib Ben Hadj-Alouane
, Yamen El Touati
:
On the Verification of Opacity in Web Services and Their Composition. IEEE Trans. Serv. Comput. 10(1): 66-79 (2017) - [c45]Amina Burouis
, Nejib Ben Hadj-Alouane
, Kais Klai:
Computing Quantified Opacity for SOG-Abstracted Web Services. SCC 2017: 362-369 - [c44]Souha Boubaker, Kais Klai, Katia Schmitz, Mohamed Graiet, Walid Gaaloul
:
Deadlock-Freeness Verification of Business Process Configuration Using SOG. ICSOC 2017: 96-112 - [c43]Amina Bourouis
, Kais Klai, Nejib Ben Hadj-Alouane
:
Measuring opacity in web services. iiWAS 2017: 530-534 - [c42]Hiba Ouni, Kais Klai, Chiheb Ameur Abid, Belhassen Zouari:
Parallel Symbolic Observation Graph. ISPA/IUCC 2017: 770-777 - [c41]Souheib Baarir, Kais Klai:
First international workshop on verification of business and software processes. ICSSP 2017: 143-144 - [c40]Samir Tata, Kais Klai, Rakesh Jain:
Formal Model and Method to Decompose Process-Aware IoT Applications. OTM Conferences (1) 2017: 663-680 - [c39]Hiba Ouni, Kais Klai, Chiheb Ameur Abid, Belhassen Zouari:
A Parallel Construction of the Symbolic Observation Graph: the Basis for Efficient Model Checking of Concurrent Systems. SCSS 2017: 107-119 - [c38]Mohamed Graiet, Kais Klai:
Track Report for Formal Verification of Service Based Systems: FVSBS 2017. WETICE 2017: 238 - 2016
- [c37]Kais Klai, Hanen Ochi:
A Formal Approach for Service Composition in a Cloud Resources Sharing Context. CCGrid 2016: 458-461 - [c36]Kais Klai, Hanen Ochi:
Model Checking of Composite Cloud Services. ICWS 2016: 356-363 - [c35]Rania Ben Halima, Slim Kallel, Kais Klai, Walid Gaaloul
, Mohamed Jmaiel:
Formal Verification of Time-Aware Cloud Resource Allocation in Business Process. OTM Conferences 2016: 400-417 - [c34]Mohamed Graiet, Kais Klai:
Track Report for Formal Verification of Service Based Systems: FVSBS 2016. WETICE 2016: 191 - 2015
- [j8]Amina Bourouis
, Kais Klai, Yamen El Touati
, Nejib Ben Hadj-Alouane
:
Checking Opacity of Vulnerable Critical Systems On-The-Fly. Int. J. Inf. Technol. Web Eng. 10(1): 1-30 (2015) - [j7]Kais Klai:
Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets. Trans. Petri Nets Other Model. Concurr. 10: 34-54 (2015) - [c33]Camille Coti, Sami Evangelista, Kais Klai:
Queue-less, Uncentralized Resource Discovery: Formal Specification and Verification. PNSE @ Petri Nets 2015: 315-316 - [c32]Kais Klai, Hanen Ochi:
LTL Model Cheking of Service-Based Business Processes in the Cloud. COMPSAC Workshops 2015: 398-403 - [c31]Amina Bourouis
, Kais Klai, Yamen El Touati
, Nejib Ben Hadj-Alouane
:
Opacity Preserving Abstraction for Web Services and Their Composition Using SOGs. ICWS 2015: 313-320 - [c30]Kais Klai, Hanen Ochi:
A Bottom-Up Approach to Check the Correctness of Interorganisational Workflows. TASE 2015: 7-14 - [c29]Abderraouf Boussif, Mohamed Ghazel, Kais Klai:
Combining Enumerative and Symbolic - Techniques for Diagnosis of Discrete-Event Systems. VECoS 2015: 23-34 - [c28]Mohamed Graiet, Kais Klai:
FVSBS 2015 Track Report: Formal Verification of Service Based Systems. WETICE 2015: 182 - [i2]Camille Coti, Sami Evangelista, Kais Klai:
Time Petri Net Models for a New Queuless and Uncentralized Resource Discovery System. CoRR abs/1502.03431 (2015) - 2014
- [c27]Kais Klai:
On-The-Fly Model Checking of Times Properties on Time Petri Nets. PNSE @ Petri Nets 2014: 35-53 - [c26]Sami Yangui, Kais Klai, Samir Tata:
Deployment of Service-Based Processes in the Cloud Using Petri Net Decomposition. OTM Conferences 2014: 57-74 - [c25]Mohamed Graiet, Zied Jaoua, Kais Klai:
Track Report of Formal Verification of Service Based Systems (FVSBS 2014). WETICE 2014: 312 - [c24]Kais Klai, Nawel Hamdi, Nejib Ben Hadj-Alouane
:
An On-the-Fly Approach for the Verification of Opacity in Critical Systems. WETICE 2014: 345-350 - 2013
- [c23]Kais Klai, Samir Tata:
Formal Modeling of Elastic Service-Based Business Processes. IEEE SCC 2013: 424-431 - [c22]Mourad Amziani, Kais Klai, Tarek Melliti, Samir Tata:
Time-Based Evaluation of Service-Based Business Process Elasticity in the Cloud. CloudCom (1) 2013: 573-580 - [c21]Kais Klai, Hanen Ochi:
Checking Compatibility of Web Services Behaviorally. FSEN 2013: 267-282 - [c20]Kais Klai, Hanen Ochi, Samir Tata:
Formal Abstraction and Compatibility Checking of Web Services. ICWS 2013: 163-170 - [c19]Kais Klai, Naim Aber, Laure Petrucci
:
Verification of Reachability Properties for Time Petri Nets. RP 2013: 159-170 - [c18]Kais Klai, Naim Aber, Laure Petrucci
:
A New Approach to Abstract Reachability State Space of Time Petri Nets. TIME 2013: 117-124 - 2012
- [j6]Kais Klai, Samir Tata, Hanen Ochi:
Generic and Specific Compatibility Criteria for Web Service Composition: Formal Abstraction and Modular Verification Approach1. Int. J. Web Serv. Res. 9(4): 45-68 (2012) - [j5]Étienne André, Christine Choppy, Kais Klai:
Formalizing non-concurrent UML state machines using colored petri nets. ACM SIGSOFT Softw. Eng. Notes 37(4): 1-8 (2012) - [j4]Christine Choppy, Anna Dedova, Sami Evangelista, Kais Klai, Laure Petrucci
, Samir Youcef:
Modelling and Formal Verification of the NEO Protocol. Trans. Petri Nets Other Model. Concurr. 6: 197-225 (2012) - [c17]Kais Klai, Jörg Desel:
Checking Soundness of Business Processes Compositionally Using Symbolic Observation Graphs. FMOODS/FORTE 2012: 67-83 - [c16]Leila Abidi, Christophe Cérin, Kais Klai:
Design, Verification and Prototyping the Next Generation of Desktop Grid Middleware. GPC 2012: 74-88 - [c15]Kais Klai, Hanen Ochi:
Checking Compatibility of Web Services Using SOGs. ICWS 2012: 670-671 - [c14]Étienne André
, Kais Klai, Hanen Ochi, Laure Petrucci
:
A Counterexample-Based Incremental and Modular Verification Approach. Monterey Workshop 2012: 283-302 - 2011
- [j3]Kais Klai, Samir Tata, Jörg Desel:
Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. Data Knowl. Eng. 70(5): 467-482 (2011) - [j2]Christine Choppy, Kais Klai, Hacene Zidani:
Formal verification of UML state diagrams: a petri net based approach. ACM SIGSOFT Softw. Eng. Notes 36(1): 1-8 (2011) - [c13]Alexandre Duret-Lutz
, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg
:
Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking. ATVA 2011: 336-350 - [c12]Kais Klai, Walid Gaaloul
:
Petri Net Modeling and Verification of Transactional Workflows. WETICE 2011: 176-184 - [i1]Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg:
Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking. CoRR abs/1106.5700 (2011) - 2010
- [c11]Christine Choppy, Anna Dedova, Sami Evangelista, Silien Hong, Kais Klai, Laure Petrucci
:
The NEO Protocol for Large-Scale Distributed Database Systems: Modelling and Initial Verification. Petri Nets 2010: 145-164
2000 – 2009
- 2009
- [c10]Kais Klai, Samir Tata, Jörg Desel:
Symbolic Abstraction and Deadlock-Freeness Verification of Inter-enterprise Processes. BPM 2009: 294-309 - 2008
- [j1]Samir Tata, Kais Klai, Nomane Ould Ahmed M'Bareck:
CoopFlow: A Bottom-Up Approach to Workflow Cooperation for Short-Term Virtual Enterprises. IEEE Trans. Serv. Comput. 1(4): 214-228 (2008) - [c9]Kais Klai, Laure Petrucci
:
Modular construction of the symbolic observation graph. ACSD 2008: 88-97 - [c8]Kais Klai, Denis Poitrenaud:
MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs. Petri Nets 2008: 288-306 - 2007
- [c7]Kais Klai, Laure Petrucci, Michel A. Reniers:
An Incremental and Modular Technique for Checking LTL\X Properties of Petri Nets. FORTE 2007: 280-295 - 2006
- [c6]Kais Klai, Nomane Ould Ahmed M'Bareck, Samir Tata:
Behavioral Technique for Workflow Abstraction and Matching. Business Process Management 2006: 477-483 - [c5]Kais Klai, Samir Tata, Issam Chebbi:
An Observation-based Algorithm for Workflow Matching. MSVVEIS 2006: 193-197 - 2005
- [c4]Kamel Barkaoui, Jean-Michel Couvreur, Kais Klai:
On the Equivalence Between Liveness and Deadlock-Freeness in Petri Nets. ICATPN 2005: 90-107 - [c3]Kais Klai, Serge Haddad, Jean-Michel Ilié
:
Modular Verification of Petri Nets Properties: A Structure-Based Approach. FORTE 2005: 189-203 - [c2]Kais Klai, Samir Tata:
Abstraction-basedWorkflow Cooperation Using Petri Net Theory. WETICE 2005: 113-120 - 2004
- [c1]Serge Haddad, Jean-Michel Ilié
, Kais Klai:
Design and Evaluation of a Symbolic and Abstraction-Based Model Checker. ATVA 2004: 196-210
Coauthor Index
aka: Mohamed Graïet
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 23:18 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint