Tayssir TOUILI

• I am a CNRS researcher in LIAFA.

• Office: Building Sophie Germain, 4th floor, office 4026. Access map.

• Mailing Address: LABORATOIRE LIAFA - UNIVERSITE Paris Diderot - Paris7 - Case 7014 -75205 Paris Cedex 13 - FRANCE

• Phone: (+33)(0)1 57 27 92 45 (If you are outside France, don't dial 0)

• Fax: (+33)(0)1 57 27 94 09 (If you are outside France, don't dial 0)

• E-Mail: touili@liafa.univ-paris-diderot.fr

  PLEASE NOTE: NEW EMAIL ADDRESS

NEW: AN "INVITED RESEARCHER" POSITION IS AVAILABLE. TO APPLY, SEND AN EMAIL TO touili@liafa.jussieu.fr

Conferences:

• Co-chair of CAV 2010


• Co-chair of VECOS 2011


• Workshop co-chair of FM 2012

I am on the PC of:

• POPL 2014
• FSEN 2013
• AVoCS 2012
• SPIN 2012
• VECOS 2012
• LATA 2012
• CAV 2011
• GandALF 2011
• VECOS 2011 (co-chair)
• CAV 2010 (co-chair)
• TACAS 2010
• POPL 2010
• VECOS 2010
• CAV 2009
• INFINITY 2009
• VECOS 2009
• MEMICS 2008
• VMCAI 2008
• VECOS 2008
• VMCAI 2007
• ICTAC 2006

Software:

• NEW: PuMoC: A CTL Model-Checker For Sequential Programs

• ♠ SPADE: Verification of Multithreaded Dynamic and Recursive Programs

• PRESS: A model checker for multithreaded programs modeled by Process Rewrite Systems

• MAGIC: A model checker for concurrent C-programs

Publications:

• Tayssir Touili. Special issue on Computer Aided Verification (CAV'10). Formal Methods in System Design. Volume 40, Number 2 (2012).



• Tayssir Touili, Byron Cook and Paul Jackson. Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings Springer 2010. (Preface and Table of Contents)

• Tayssir Touili. Computing transitive closures of hedge transformations. IJCCBS 3(1/2): 132-150 (2012)



• Ahmed Bouajjani, Tayssir Touili. Widening techniques for regular tree model checking. STTT 14(2): 145-165 (2012)



• Nicholas Kidd, Peter Lammich, Tayssir Touili and Thomas W. Reps. A decision procedure for detecting atomicity violations for communicating processes with locks. Int. Journal on Software Tools for Technology Transfer. (PDF)



• Tayssir Touili and Mohamed Faouzi Atig. Verifying parallel programs with dynamic communication structures. Theoretical Computer Science. Volume 411, Issues 38-39, Pages 3460-3468, 28 August 2010. (PDF)



• Mihaela Sighireanu and Tayssir Touili. Bounded Communication Reachability Analysis of Process Rewrite Systems with Ordered Parallelism. Electronic Notes in Theoretical Computer Science, Volume 239, Pages 43-56. 2009. (gziped PostScript)



• Narjes Ben Rajeb, Brahim Nasraoui, Riadh Robbana and Tayssir Touili. Verifying Multithreaded Recursive Programs with Integer Variables. Electronic Notes in Theoretical Computer Science, Volume 239, Pages 143-154. 2009. (gziped PostScript)



• Ahmed Bouajjani, Jan Strejcek, and Tayssir Touili. On Symbolic Verification of Weakly Extended PAD. Electronic Notes in Theoretical Computer Science, Volume 175, Issue 3, 28 June 2007, Pages 47-64. (gziped PostScript)



• Ahmed Bouajjani, Anca Muscholl, and Tayssir Touili. Permutation Rewriting and Algorithmic Verification. Information and Computation. Volume 205, Issue 2 , February 2007, Pages 199-224 (abstract , gziped PostScript)



• Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. Electronic Notes in Theoretical Computer Science, Volume 138, Issue 3, Pages 153-178, 2005. (gziped PostScript)



• Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. A generic approach to the static analysis of concurrent programs with procedures. International Journal of Foundations of Computer Science, volume 14, number 4, august 2003. (abstract , gziped PostScript)

• Fu Song and Tayssir Touili. Model-Checking Software Library API Usage Rules. In Proc. 10th International Conference on integrated Formal Methods (iFM 2013).



• Fu Song and Tayssir Touili. LTL Model-Checking for Malware Detection. In Proc. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013).



• Fu Song and Tayssir Touili. PuMoC: A CTL Model-Checker For Sequential Programs. In Proc. 27th IEEE/ACM International Conference On Automated Software Engineering (ASE 2012).



• Fu Song and Tayssir Touili. Efficient Malware Detection using Model-Checking. In Proc. 18th International Symposium on Formal Methods (FM 2012).



• Fu Song and Tayssir Touili. Pushdown Model-Checking for Malware Detection. In Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012). (PDF) . This paper won the EASST best paper award at ETAPS 2012.



• Fu Song and Tayssir Touili. Efficient CTL Model-Checking for Pushdown Systems. In Proc. Intern. Conf. on Concurrency Theory (CONCUR 2011). (PDF)



• Tayssir Touili. Constrained Reachability of Process Rewrite Systems. In Proc. 6th International Colloquium on Theoretical Aspects of Computing (ICTAC'09). 2009. (gziped PostScript)



• Mohamed Faouzi Atig and Tayssir Touili. Verifying Parallel Programs with Dynamic Communication Structures. In Proc. 14th International Conference on Implementation and Application of Automata (CIAA'09). 2009. (gziped PostScript)



• Nicholas Kidd, Peter Lammich, Tayssir Touili and Thomas W. Reps. A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks. In Proc. 16th International SPIN Workshop on Model Checking of Software (SPIN'09). 2009. (gziped PostScript)



• Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili. Analyzing Asynchronous Programs with Preemption. In Proc. 28th Foundations of Software Technology and Theoretical Computer Science conference (FSTTCS'08). 2008. (gziped PostScript)



• Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili. On the Reachability Analysis of Acyclic Networks of Pushdown Systems. In Proc. 19th International Conference on Concurrency Theory (CONCUR'08). Lecture Notes in Computer Science, 2008. (gziped PostScript)



• Narjes Ben Rajeb, Brahim Nasraoui, Riadh Robbana, and Tayssir Touili. Verifying Multithreaded Recursive Programs with Integer Variables. In Proc. 10th International Workshop on Verification of Infinite-State Systems (INFINITY'08). 2008. (gziped PostScript)



• Ahmed Bouajjani, Peter Habermehl, Lukas Holik, Tayssir Touili, and Tomas Vojnar. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In Proc. 13th International Conference on Implementation and Application of Automata (CIAA'08). Lecture Notes in Computer Science, 2008. (gziped PostScript)



• Akash Lal, Tayssir Touili, Nicholas Kidd and Thomas Reps. Interprocedural Analysis of Concurrent Programs Under a Context Bound. In Proc. 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08). Lecture Notes in Computer Science, 2008. (gziped PostScript)



• Akash Lal, Nicholas Kidd, Thomas Reps and Tayssir Touili. Abstract Error Projection. In Proc. 14th International Static Analysis Symposium (SAS'07). Lecture Notes in Computer Science, 2007. (gziped PostScript)



• Tayssir Touili. Computing Transitive Closures of Hedge Transformations. In Proc. 1st International Workshop on Verification and Evaluation of Computer and Communication Systems (VECOS'07). eWIC Series. British Computer Society, 2007. (gziped PostScript)



• Gael Patin, Mihaela Sighireanu and Tayssir Touili. SPADE: Verification of Multithreaded Dynamic and Recursive Programs. In Proc. 19th Int. Conf. on Computer Aided Verification (CAV'07), Lecture Notes in Computer Science, 2007. (gziped PostScript)



• Eugene Asarin, Thierry Cachat, Alexander Seliverstov, Tayssir Touili and Vassily Lyubetsky. Attenuation Regulation as a Term Rewriting System. In Proc. 2nd International Conference on Algebraic Biology (AB'07). (gziped PostScript)



• Mihaela Sighireanu and Tayssir Touili. Bounded Communication Reachability Analysis of Process Rewrite Systems with Ordered Parallelism. In Proc. 8th International Workshop on Verification of Infinite-State Systems (INFINITY'06). (gziped PostScript)



• Ahmed Bouajjani, Jan Strejcek, and Tayssir Touili. On Symbolic Verification of Weakly Extended PAD. In Proc. of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS'06). ( gziped PostScript)



• Julien d'Orso and Tayssir Touili. Regular Hedge Model Checking In Proc. of the 4th IFIP International Conference on Theoretical Computer Science (TCS'06). ( gziped PostScript)



• Sagar Chaki, Edmund Clarke, Nicholas Kidd, Thomas Reps, and Tayssir Touili. Verifying Concurrent message-Passing C programs with Recursive Calls. In Proc. 12th. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06). ( gziped PostScript)



• Sagar Chaki, Edmund Clarke, Orna Grumberg, Joel Ouaknine, Natasha Sharygina, Tayssir Touili, and Helmut Veith. State/Event Software Verification for Branching-Time Specifications. In Proc. 5th International Conference on Integrated Formal Methods (IFM'05). (abstract , gziped PostScript)



• A. Bouajjani, M. Mueller-Olm, and T. Touili. Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems. In Proc. 16th Intern. Conf. on Concurrency Theory (CONCUR'05). ( gziped PostScript)



• A. Bouajjani, T. Touili. On Computing Reachability Sets of Process Rewrite Systems. In Proc. 16th Intern. Conf. on Rewriting Techniques and Applications (RTA'05). (gziped PostScript)



• Tayssir Touili. Dealing with communication for dynamic multithreaded recursive programs. Invited paper. In Proc. of VISSAS'05. (abstract , gziped PostScript)



• Edmund Clarke, Muralidhar Talupur, Tayssir Touili, and Helmut Veith. Verification by Network Decomposition.. In Proc. Intern. Conf. on Concurrency Theory (CONCUR'04). (abstract , gziped PostScript)



• Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability Analysis of Synchronized PA Systems. In Proc. 6th International Workshop on Verification of Infinite-State Systems (INFINITY'04). (abstract , gziped PostScript)



• Ahmed Bouajjani and Tayssir Touili. Reachability Analysis of Process Rewrite Systems.. In Proc. Intern. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'03). (abstract , gziped PostScript)



• Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. A generic approach to the static analysis of concurrent programs with procedures. In Proc. 30th ACM SIPGPLAN-SIGACT on Principles of Programming Languages (POPL'03). (abstract , gziped PostScript)



• Ahmed Bouajjani and Tayssir Touili. Extrapolating Tree Transformations. In Proc. 14th Int. Conf. on Computer Aided Verification (CAV'02), Lecture Notes in Computer Science, 2002. (abstract , gziped PostScript)



• Tayssir Touili. Regular Model Checking using Widening Techniques. 1st Vepas Workshop (VEPAS'01). In Volume 50 of Electronic Notes in TCS, 2001. (abstract , gziped PostScript)



• Ahmed Bouajjani, Anca Muscholl, and Tayssir Touili. Permutation Rewriting and Algorithmic Verification. In Proc. 16th IEEE Symp. on Logic in Computer Science (LICS'01), 2001. (abstract , gziped PostScript)



• Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, and Tayssir Touili. Regular Model Checking. In Proc. 12th Int. Conf. on Computer Aided Verification (CAV'00), Lecture Notes in Computer Science, 2000. (abstract , gziped PostScript)