Gennaro Parlato








Short Bio

Gennaro Parlato is Full Professor of Computer Science at the
University of Molise (UNIMOL), heading the
Program Analysis in the Clouds Lab (PAC Lab)
within the Department of Biosciences and Territory (DiBT).

Prior to UNIMOL, Gennaro had a prolific international research career,
including a postdoc role at UIUC (Urbana, USA, May 2006-March 2010),
and work at LIAFA/IRIF Laboratory (Paris, France, April 2010-April 2011).
From 2011 and 2018, Gennaro was an academic at
the University of Southampton (SOTON), progressing from Lecturer
to Associate Professor in the
Department of Electronics and Computer Science (ECS),
While at the University of Southampton, he also contributed to the
GCHQ/EPSRC Academic Centre of Excellence for
Cybersecurity Research. Gennaro received his
Computer Science doctorate from the University of Salerno, Italy,
in April 2006.

His CV is available here.

Research Interests

   - Software analysis and verification
   - Model checking: algorithms and tools
   - Verification of Concurrent Software
   - Security, Access Control
   - Logics, automata theory, and graph theory


Current Research Projects

   - Sequentialization of concurrent programs (CSeq)
   - Model checking of concurrent programs using fixed-point (GetAFix)
   - Reasoning with dynamic data structures (S
TRAND)
   - Verification of access control models (V
AC)
   - Symbolic Infinite State Tree Automata (S
ISTA)
   - Programs Analysis in the Clouds (P
AC) supported by Amazon Science

Software/Tools

   - CSeq: Sequentialization framework for concurrent C programs
   - GetAFix: A Boolean program checker
   - S
TRAND: Decidable logics/SMT solver for reasoning with heaps
   - VAC: Verifier for Role Based Access Control Systems
   - V
ERISMART

PhD Students

   
- Enrico Steffinlongo      
      [
Visinting PhD student,  Ca' Foscari University of Venice, Italy,  Oct 2016-Jun 2018 ]
            Reseach topic: Verification of Access Control Models

   - Mikhail Ramalho
      [
Feb 2015-Dec 2018, co-advised with Denis A Nicole)  

   - Truc Lam Nguyen         [ Oct 2013 - May 2017 ]
     
Thesis: A pragmatic verification approach for concurrent programs 

   - Ermenegildo Tomasco  [May 2012-May 2017]
     
Thesis: Separating Computation from Communication: A Design Approach for Concurrent

    - Omar Inverso               [ Oct 2011 - Oct 2015 ]
       Thesis: Bounded Model Checking of Multi-threaded Programs via Sequentialization
         


Postdocs

   - Omar Inverso (2015)
   - Truc Lam Nguyen (2016)
   - Mikhail Ramalho (2016)
   - Giulio Garbi (2022)


Service

   - PC Member: CAV 2023, Paris, France
     35th Int'l conference on Computer Aided Verification

   - PC Member: VSTTE 2023, Ames, IA, USA
     15th Working Conference on Verified Software  

   - PC Member: VMCAI 2023, Boston, MA, USA
     24th Int'l Conference on Verification, Model Checking, and Abstract Interpretation 

   - PC Member: VSTTE 2022, Oxford, UK
     14th Working Conference on Verified Software  

   - PC Member: OVERLAY 2021, Padova, Italy
     3rd Workshop on Artificial Ontelligence and fOrmal VERification, Logic,
     Automata, and sYnthesis 

   - PC Member: LATA 2020 & 2021, Milan, Italy
     14th-15th Int'l Conference on Language and Automata Theory and Applications  

   - PC Member: GandALF 2020, Brussels, Belgium
     11th Int'l Symposium on Games, Automata, Logics and Formal Verification

   - PC Member: GandALF 2019, Bordeaux, France
     10th Int'l Symposium on Games, Automata, Logics and Formal Verification

   - PC Member: VSTTE 2018, Oxford, UK
     10th Working Conference on Verified Software  

   - PC Member: LATA 2018, Bar-Ilan, Israel
     12th Int'l Conference on Language and Automata Theory and Applications  

   - PC Member: GandALF 2018, Saarbrucken, Germany
     9th Int'l Symposium on Games, Automata, Logics and Formal Verification

   - PC and Jury Member: SV-COMP 2017, Uppsala, Sweden
     6th Competition on Software Verification

   - ERC Member: CAV 2016, Toronto, Ontario, Canada
     28th Int'l Conference on Computer Aided Verification

   - PC Member: ICSE 2016, Austin, USA
     38th Int'l Conference on Software Engineering

  - PC and Jury Member: SV-COMP 2016, Eindhoven, Netherlands
     5th Competition on Software Verification

   - PC Member: TGC 2015, Madrid, Spain
     10th Int'l Symposium on Trustworthy Global Computing

   - PC Member: SPIN 2015, Stellenbosch, South Africa
     22nd Int'l SPIN Workshop on Model Checking of Software

   - PC Member: FCT 2015, Gdansk, Poland
     20th Int'l Symposium on Fundamentals of Computation Theory

   - PC and Jury Member: SV-COMP 2015, London, UK
     4th Competition on Software Verification

   - PC Member: GandALF 2015, Genoa, Italy
     5th Int'l Symposium on Games, Automata, Logics and Formal Verification

   - PC and Jury Member: SV-COMP 2014, Grenoble, France
     3rd Competition on Software Verification

   - PC Member: CAV 2012, Berkeley, USA
     24th Int'l Conference on Computer Aided Verification

   - PC Member: MFCS 2012, Bratislava, Slovakia.
     37th Int'l Symposium on Mathematical Foundations of Computer Science.

   - PC Member: GandALF 2010, Minori, Italy
     1st Int'l Symposium on Games, Automata, Logics and
     Formal Verification
Contact Information
Teaching  
   
  Univerity of Molise, Italy  
  - Algorithms and Data Structures   ( 2018-19, 2019-20,
    2020-21, 2021-22
    2022-23, 2023-24)
  - Program Analysis   ( 2019-20, 2020-21,
    2021-22, 2022-23) 
 
  University of Southampton, UK
  - Theory of Computing (COMP2210)   ( 2012-13, 2013-14,
    2014-15, 2015-16,
    2016-17, 2017-18,
    2018-19              )
  - Algorithmics (COMP1201)   ( 2016-17, 2017-18)
  - Automated Software Verification (COMP6210)   ( 2014-15 )
  - Formal Design of Systems (COMP6004)   ( 2011-12, 2012-13,
    2013-14 )

  PhD Schools  
  - Lecture series at
    UPMARC Summer School on Multicore Computing,
    Uppsala, Sweden
  ( June 2015 )
  - Module on Program Verification, PhD program,
    IMT School for Advanced Studies, Lucca, Italy
  ( Apr 2016, July 2018 )
   
Papers    (DBLP, Google Scholar)  
1.
   Reachability Games Modulo Theories with a Bounded Safety Player
  
M. Faella, and G. Parlato
   37th AAAI Conference on Artificial Intelligence (AAAI)
   Washingtonm DC, USA, 2023
   PDF, Recorded Presentation, Artifact
2.
   Verifying Programs by Bounded Tree-Width Behavior Graphs.
   O. Inverso, S. La Torre, G. Parlato, and E. Tomasco
   Multi-Agent Systems - 20th European Conference (EUMAS),
   Naples, Italy, 2023
   PDF
3.
   CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory
  
B. Fischer, S. La Torre, G. Parlato, and P. Schrammel
   37th IEEE/ACM International Conference on Automated Software Engineering (ASE)
   Oakland Center, Michigan, USA, 2022
   PDF, PPT, semantics example
4.
   Reasoning about Data Trees using CHCs
  
M. Faella, and G. Parlato
   34th Int'l Conference on Computer Aided Verification (CAV)
   Haifa, Israel, 2022
   PDF, PPT, Artifact (10MB zip)
5.
   Bounded Verification of Multi-Threaded Programs via Lazy Sequentialization
   O. Inverso, E. Tomasco, B. Fischer, S. La Torre, and G. Parlato
   ACM Transactions on Programming Languages and Systems (TOPLAS) 44(1): 1:1-1:50, 2022
   PDF
6.
   On the Model-Checking of Branching-time Temporal Logics with BDI Modalities
   S. La Torre, and G. Parlato
   19th International Conference on Autonomous Agents and Multiagent Systems (AAMAS)
   Auckland, New Zealand, 2020
   PDF
7.
   Reachability of Scope-bounded Multistack Pushdown Systems
   S. La Torre, M. Napoli, and G. Parlato
   Information and Computation, 2020
   PDF
8.
   A Fixed-point Model-checker for BDI Logics over Finite-state Worlds
   S. La Torre, and G. Parlato
   2nd Workshop on Artificial Ontelligence and fOrmal VERification, Logic, Automata,
   and sYnthesis (OVERLAY)
   Bolzano, Italy, 2020
   PDF
9.
   VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-threaded Programs with Lazy-CSeq
   B. Fischer, S. La Torre, and G. Parlato
   34th IEEE/ACM International Conference on Automated Software Engineering (ASE)
   San Diego, CA, USA, 2019
   PDF
10.
   Model Checking BDI Logics over Finite-state Worlds
   S. La Torre, and G. Parlato
   1st Workshop on Artificial Ontelligence and fOrmal VERification, Logic, Automata,
   and sYnthesis (OVERLAY)
   Rende, Italy, 2019
   PDF
11.
   Parallel bug-finding in concurrent programs via reduced interleaving instances
   T. L. Nguyen, P. Schrammel, B. Fischer, S. La Torre, and G. Parlato
   32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)
   University of Illinois at Urbana-Champaign, Illinois, USA, 2017
   PDF, PPT
12.
   Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models  
   E. Tomasco, T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato
   International Conference on Software Engineering and Formal Methods (SEFM)
   Trento, Italy, 2017.
   PDF
, PPT
13.
    Preventing Unauthorized Data Flows
   E. Uzun, G. Parlato, V. Atluri, A. L. Ferrara, J. Vaidya, S. Sural, and D. Lorenzi
   Conference on Data and Applications Security and Privacy (DBSec)
   Philadelphia, PA, USA, 2017
   PDF

14.
   Concurrent Program Verification with Lazy Sequentialization and Interval Analysis
   T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato
   Networked Systems - 5th Intl. Conference (NETYS)
   Marrakech, Marocco, 2017
   PDF, PPT
15.
   Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution).
  
T. L. Nguyen, O. Inverso, B. Fischer, S. La Torre, and G. Parlato
   6th Intl. Competition on Software Verification (SV-COMP), held at TACAS
   Uppsala, Sweden, 2017
   PDF
16.
   On the Path-Width of Integer Linear Programming
   C. Enea, P. Habermehl, O. Inverso, and G. Parlato
   Information and Computation, 2017
   PDF
17.
   Lazy Sequentialization for TSO and PSO via Shared Memory Abstractions
   E. Tomasco, T. L. Nguyen, O. Inverso, B. Fischer, S. La Torre, and G. Parlato
   Formal Methods in Computer-Aided Design (FMCAD)
   Mountain View, CA, USA, 2016
   PDF, PPT
18.
   Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs
   T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato
   14th International Symposium on Automated Technology for Verification and Analysis (ATVA)
   Chiba, Japan, 2016
   PDF, PPT
19.
   Scope-Bounded Pushdown Languages
   S. La Torre, M. Napoli, and G. Parlato
   International Journal of Foundations of Computer Science (IJFCS)
   Vol. 27, No. 2 (2016) 215-233, DOI: 10.1142/S0129054116400074
   PDF
20.
   MU-CSeq 0.4: Individual Memory Location Unwindings (Competition Contribution)
  
E. Tomasco, T. L. Nguyen, O. Inverso, B. FischerS. La Torre, and G. Parlato
   5th Intl. Competition on Software Verification (SV-COMP), held at TACAS
   Eindhoven, The Netherlands, 2016
   [MU-CSeq 0.4 won the gold medal in the concurrency category]
   PDF,
CSeq webpage for tools and experiments

21.
   Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-Threaded C-Programs
   (Tool Demonstration)
  
O. Inverso, T. L. Nguyen, B. FischerS. La Torre, and G. Parlato
   30th IEEE/ACM International Conference on Automated Software Engineering (ASE)
   Lincoln, Nebraska, USA, 2015
   PDF,
CSeq webpage for tools and experiments
   [SV-COMP 2016: Lazy-CSeq 1.0 won the silver medal in the concurrency category]
22.
   Verifying Concurrent Programs by Memory Unwinding
  
E. Tomasco, O. Inverso, B. FischerS. La Torre, and G. Parlato.
   21st Int'l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
   London, UK,  2015.
   PDF, PPT,
  see also CSeq webpage for the tool and experiments
23.
   Lazy-CSeq 0.6c: An Improved Lazy Sequentialization Tool for C (Competition Contribution)
  
O. Inverso, E. Tomasco, B. FischerS. La Torre, and G. Parlato.
   4th Intl. Competition on Software Verification (SV-COMP), held at TACAS,
   London, UK, 2015.
   [Lazy-CSeq won the gold medal in the concurrency category]
   PDF,
PPT,  CSeq webpage
24.
   MU-CSeq 0.3: Sequentialization by Read-implicit and Coarse-grained Memory Unwindings
   (Competition Contribution)
  
E. Tomasco, O. Inverso, B. FischerS. La Torre, and G. Parlato
   4th Intl. Competition on Software Verification (SV-COMP), held at TACAS
   London, UK, 2015
   [MU-CSeq won the gold medal in the concurrency category]
   PDF, PPT,
CSeq webpage
25.
   Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded
   Context Switches (Competition Contribution)
  
T. L. Nguyen, B. FischerS. La Torre, and G. Parlato
   4th Intl. Competition on Software Verification (SV-COMP), held at TACAS
   London, UK, 2015
   PDF, PPT,
  CSeq webpage
26.
   Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization
  
O. InversoE. Tomasco, B. FischerS. La Torre, and G. Parlato
   26th Int'l Conference on Computer Aided Verification (CAV)
   Vienna, Austria, 2014
   PDF, PPT,
see also CSeq webpage for tools and experiments
27.
   VAC - Verifier of Administrative Role-based Access Control Policies
   A. L. Ferrara, P. Madhusudan, T. L. Nguyen
, and G. Parlato
   26th Int'l Conference on Computer Aided Verification (CAV)
   Vienna, Austria, 2014
   PDF, PPT,
see also VAC webpage for the tool and experiments
28.
   Lazy-CSeq: A Lazy Sequentialization Tool for C (Competition Contribution)
  
O. InversoE. TomascoS. La Torre, Bernd Fischer, and G. Parlato
   3rd Intl. Competition on Software Verification (SV-COMP), held at TACAS
   Grenoble, France, 2014
   [Cseq-Lazy won the gold medal in the concurrency category]
   PDF, PPT, CSeq webpage
29.
   MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings
   (Competition Contribution)
  
E. Tomasco, O. InversoS. La Torre, Bernd Fischer, and G. Parlato
   3rd Intl. Competition on Software Verification (SV-COMP), held at TACAS
   Grenoble, France, 2014
   [Cseq-MU won the silver medal in the concurrency category]
   PDF, PPT, CSeq webpage
30.
   Context-Bounded Analysis of TSO Systems
   F. M. Atig, A. Bouajjani, and G. Parlato

  
ETAPS Workshop in honor of Joseph Sifakis
   Grenoble, France, 2014
   PDF

31.
   A Unifying Approach for Multistack Pushdown Automata
   S. La Torre, M. Napoli, and G. Parlato
   39th International Symposium on Mathematical Foundations of Computer Science (MFCS)
   Budapest, Hungary, 2014
   PDF, PPT

32.
   Scope-Bounded Pushdown Languages
   S. La Torre, M. Napoli, and G. Parlato
   18th International Conference on Developments in Language Theory (DLT)
   Ekaterinburg, Russia, 2014
   PDF (full version), PPT

33.
   On the Path-Width of Integer Linear Programming
   C. Enea, P. Habermehl, O. Inverso, and G. Parlato
   5th International Symposium on Games, Automata, Logics and Formal Verification (GandALF)
   Verona, Italy, 2014
   PDF (full version)
, PPT (with an open problem related to this paper: ''abab problem'')
34.
   Security Analysis for Temporal Role Based Access Control
   E. Uzun, V. Atluri, J. Vaidya, S. Sural, A. L. Ferrara, G. Parlato, and P. Madhusudan
   Journal of Computer Security (JCS), 2014
   PDF
35.
   CSeq: A Concurrency Pre-Processor for Sequential C Verification Tools (Tool Demonstration)
   B. Fischer, O. Inverso, and G. Parlato
   28th IEEE/ACM International Conference on Automated Software Engineering (ASE)
   Palo Alto, CA, USA, 2013
   PDF, PPT,
CSeq webpage
36.
   Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists
   P. Garg, P. Madhusudan, and G. Parlato
   20th Static Analysis Symposium (SAS)
   Seattle, WA, USA, 2013

  
PDF, PPT, Experiments
37.
   Policy Analysis for Self-Administrated Role-Based Access Control
   A. L. Ferrara, P. Madhusudan, and G. Parlato
   19th Int'l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
   Rome, Italy,  2013
   PDF
, PPT, VAC webpage (for tools, benchmarks and experiments)
38.
   CSeq: A Sequentialization Tool for C (Competition Contribution)
   B. Fischer, and O. Inverso, and G. Parlato
   2nd Int'l Competition on Software Verification (SV-COMP), held at TACAS
   Rome, Italy,  2013   [C
SEQ won the silver medal in the concurrency category]
   PDF, CSeq webpage
39.
   Scope-bounded Multistack Pushdown Systems:  Fixed-Point, Sequentialization, and Tree-Width
   S. La Torre, and G. Parlato

   32nd Foundations of Software Technology and Theoretical Computer Science conference (FSTTCS)
   IIIT Hyderabad, India, 2012

  
PDF, PPT

   Slides of a presentation I gave at the post-conference workshop on "Verification of Infinite-State Systems":
   The tree-width of Decidable Problems: PPT  (the definition of the open problem  "abab problem" can be found  in the last five slides)
40.
   Security Analysis of Role-based Access Control through Program Verification
   A. L. Ferrara, P. Madhusudan, and G. Parlato
   25th IEEE Computer Security Foundations Symposium (CSF)
   Harvard University, Cambridge MA, USA, 2012
   PDF
, PPT, VAC webpage (for tools, benchmarks and experiments)
41.
   Sequentializing Parameterized Programs
   S. La Torre, P. Madhusudan, and G. Parlato
   4th International Workshop on Foundations of Interface Technologies (FIT)

   Tallinn, Estonia, 2012
   PDF
, PPT
42.
   Analyzing Temporal Role Based Access Control Models
   E. Uzun, V. Atluri, S. Sural, J.Vaidya, G. Parlato, A. L. Ferrara, and P. Madhusudan
   17th ACM Symposium on Access Control Models and Technologies (SACMAT)
   Newark, USA, 2012
   PDF
43.
   On Sequentializing Concurrent Programs
   A. Bouajjani, M. Emmi, G. Parlato
   18th Int'l Static Analysis Symposium (SAS)
   Venice, Italy, 2011
   PDF
, PPT
44.
   Getting Rid of Store-Buffers in the Analysis of Weak Memory Models
   F. M. Atig, A. Bouajjani, and G. Parlato
   23rd Int'l Conference on Computer Aided Verification (CAV)
   Cliff Lodge, Snowbird, Utah, USA, 2011
   PDF
, PPT, Experiments
45.
   The Tree Width of Automata with Auxiliary Storage
   P. Madhusudan, and G. Parlato
   38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)
   Austin, Texas, USA, 2011
   PDF
(technical report has more proofs), PPT
46.
   Decidable  Logics Combining Heap Structures and Data
   P. Madhusudan, G. Parlato, and X. Qiu
   38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)
   Austin, Texas, USA, 2011
   PDF
, PPT  See also the STRAND webpage for the tool and experiments
47.
   A Tabu Search Heuristic Based on k-Diamonds for the Weighted Feedback Vertex Set Problem
   F. Carrabs, R. Cerulli, M. Gentili, and G. Parlato
   Network Optimization: 5th International Conference, (INOC
   Hamburg, Germany, 2011
   PDF
48.
   Model-checking Parameterized Concurrent Programs Using Linear Interfaces
   S. La Torre, P. Madhusudan, and G. Parlato
   22nd Int'l Conference on Computer Aided Verification (CAV)
   Edinburgh, UK, 2010
   PDF

49.
   The Language Theory of Bounded Context-Switching
   S. La Torre, P. Madhusudan, G. Parlato
   9th Latin American Theoretical Informatics Symposium (LATIN)
   Oaxaca, Mexico, 2010
   PDF
, PPT
50.
   Reducing Context-bounded Concurrent Reachability to Sequential Reachability
   S. La Torre, P. Madhusudan, and G. Parlato
   21st Int'l Conference on Computer Aided Verification (CAV)
   Grenoble, France, 2009

  
PDF, PPT, See also the cbp2bp page.
51.
   Analyzing Recursive Programs using Fixed-point Calculus
   S. La Torre, P. Madhusudan, G. Parlato

   30th annual ACM SIGPLAN 2009 Conference on Programming Language Design and Implementation (PLDI)
   Dublin, Ireland, 2009
   PDF, PPT
, See also the Getafix page for the tool and experiments
52.
   Improvements for Truthful Mechanisms with Verifiable One-Parameter Selfish Agents
  
A. Ferrante, G. Parlato,  F. Sorrentino, and C. Ventre
   Theoretical Computer Science (TCS) 2009

   PDF
53.
   An Infinite Automaton Characterization of Double Exponential Time
  
S. La Torre, P. Madhusudan, and G. Parlato
   17th EACSL Annual Conference on Computer Science Logic (CSL)
   Bertinoro, Italy, 2008
   PDF, PPT

54.
   Verification of Scope-Dependent Hierarchical State Machines
   S. La Torre, M. Napoli, M. Parente, and G. Parlato
   Information and Computation 2008
   PDF

55.
   Context-Bounded Analysis of Concurrent Queue Systems
   S. La Torre, P. Madhusudan
, and G. Parlato
   14th Int'l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
   Budapest, Hungary, 2008
   PDF, PPT

56.
   A Robust Class of Context-Sensitive Languages
   S. La Torre, P. Madhusudan, and G. Parlato
   22nd IEEE Symp. on Logic in Computer Science (LICS)
   Wroclaw, Poland, 2007
   PDF

57.
   On the Complexity of LTL Model-Checking of Recursive State Machines
   S. La Torre, and G. Parlato
   34th Int'l Colloquium on Automata, Languages and Programming (ICALP)
   Wroclaw, Poland, 2007
   PDF

58.
   Verification of Succinct Hierarchical State Machines
   S. La Torre, M. Napoli, and M. Parente, and G. Parlato
   1st Int'l Conference on Language and Automata Theory and Applications (LATA)
   Tarragona, Spain, 2007
   PDF

59.
   Improvements for Truthful Mechanisms with Verifiable One-Parameter Selfish Agents
   A. Ferrante, G.Parlato, F. Sorrentino, and C. Ventre
   3rd Workshop on Approximation and Online Algorithms (WAOA)
   Palma de Mallorca, Mallorca, Balear Islands, Spain, 2005
   PDF

60.
   A Linear Time Algorithm for the Minimum Weighted Feedback Vertex Set on Diamonds
   F. Carrabs, R. Cerulli, and M. Gentili, and G. Parlato
   Information Processing Letters (IPL), 2005
   PDF

61.
   Minimum Weighted Feedback Vertex Set on Diamonds
   F. Carrabs, R. Cerulli, M. Gentili, and G. Parlato
   Electronic Notes in Discrete Mathematics (ENDM), 2004
   PDF
62.
   Hierarchical and Recursive State Machines with Context-Dependent Properties
   S. La Torre, M. Napoli, M. Parente, and G. Parlato
   30th Int'l Colloquium on Automata, Languages and Programming (ICALP)
   Eindhoven, The Netherlands, 2003
   PDF
, PPT