Gennaro Parlato





Short Bio

Dr Gennaro Parlato is an Associate Professor of Computer Science in the Electronic & Software Systems (ESS) research group in the Department of Electronics and Computer Science (ECS) at the University of Southampton. He  is a member of the GCHQ/EPSRC Academic Centre of Excellence for Cybersecurity Research (ACE-CSR). He has been an academic of the University of Southampton since May 2011. He received his Doctoral degree in Computer Science from the University of Salerno,  Italy, in April 2006. Between 2006 and 2011, Gennaro worked as a postdoc research associate in the
Department of Computer Science at UIUC (Urbana, USA, May 2006-March 2010), and in the Modeling and Verification research group at LIAFA Laboratory (Paris, France, April 2010-April 2011).

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)
   - Verification of programs under weak memory models
   - Model checking of concurrent programs using fixed-point
      (GetAFix)
   - Reasoning with dynamic data structures (S
TRAND)
   - Verification of access control models (V
AC)
   - Decidable automata with auxiliary storage
   - Language-based security for distributed ledger

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

PhD Students

   - Mikhail Ramalho
     
(Feb 2015-present, co-advised with Denis A Nicole)  
   - Truc Lam Nguyen
     
(Oct 2013-present)  
   - Ermenegildo Tomasco
     
(Verification of concurrent programs, May 2012-present)
   
- Omar Inverso
       (Bounded Model Checking of Multi-threaded Programs via Sequentialization,
       Oct 2011-Oct 2015)  


Postdocs

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


Teaching

   - COMP2210: Theory of Computing                            (2016-17)
   - COMP6233: Topics in Computer Science                  (2016-17)
   - 20-hour module on Program Verification, PhD program
      IMT School for Advanced Studies, Lucca, Italy          (April 2016)
   - COMP2210: Theory of Computing                            (2015-16)
   - COMP6233: Topics in Computer Science                  (2015-16)
   - Lecture series at UPMARC Summer School on Multicore Computing
      Slides(Part1, Part2)                                                    (June 2015)
   - COMP6210: Automated Software Verification          (2014-15)
   - COMP2210: Theory of Computing                            (2014-15)
   - COMP6004: Formal Design of Systems                     (2013-14)
  
- COMP2210: Theory of Computing                            (2013-14)
   - COMP6004: Formal Design of Systems                     (2012-13)
  
- COMP2011: Theory of Computing                            (2012-13)
   - COMP6004: Formal Design of Systems                     (2011-12)

Service

   - 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

Papers     (DBLP, Google Scholar)
Contact Information
1.
  Embedding Weak Memory Models Within Eager Sequentialization
  E. Tomasco, T.L. Nguyen, B. Fischer, S. La Torre, and G. Parlato
  Technical Report, University of Southampton, October, 2016.
  PDF

2.
  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
3.
  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
4.
  On the Path-Width of Integer Linear Programming
  with C. Enea, P. Habermehl, O. Inverso
  Information and Computation, 2016
  PDF
5.
  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
6.
  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

7.
  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]
8.
  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 VAC webpage for the tool and experiments
9.
  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
10.
  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
11.
  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
12.
  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
13.
  VAC - Verifier of Administrative Role-based Access Control Policies
  with A. L. Ferrara, P. Madhusudan, and T. L. Nguyen
.
  26th Int'l Conference on Computer Aided Verification (CAV)
  Vienna, Austria, 2014
  PDF, PPT,
see also VAC webpage for the tool and experiments
14.
  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
15.
  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
16.
  Context-Bounded Analysis of TSO Systems
  with F. M. Atig, and A. Bouajjani

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

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

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

19.
  On the Path-Width of Integer Linear Programming
  with C. Enea, P. Habermehl, O. Inverso
  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'')
20.
  Security Analysis for Temporal Role Based Access Control
  with E. Uzun, V. Atluri, J. Vaidya, S. Sural, A. L. Ferrara, G. Parlato, and P. Madhusudan
  Journal of Computer Security (JCS), 2014
  PDF
21.
  CSeq: A Concurrency Pre-Processor for Sequential C Verification Tools (Tool Demonstration)
  with B. Fischer, and O. Inverso
  28th IEEE/ACM International Conference on Automated Software Engineering (ASE)
  Palo Alto, CA, USA, 2013
  PDF, PPT,
CSeq webpage
22.
  Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists
  with P. Garg, and P. Madhusudan
  20th Static Analysis Symposium (SAS)
  Seattle, WA, USA, 2013

 
PDF, PPT, Experiments
23.
  Policy Analysis for Self-Administrated Role-Based Access Control
  with A. L. Ferrara, and P. Madhusudan
  19th Int'l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
  Rome, Italy,  2013
  PDF
, PPT, VAC (for tools, benchmarks and experiments)
24.
  CSeq: A Sequentialization Tool for C (Competition Contribution)
  with B. Fischer, and O. Inverso
  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
25.
  Scope-bounded Multistack Pushdown Systems:  Fixed-Point, Sequentialization, and Tree-Width
  with S. La Torre

  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  (an open problem on words: "abab problem",  in the last 5 slides)
26.
  Security Analysis of Role-based Access Control through Program Verification
  with A. L. Ferrara, and P. Madhusudan
  25th IEEE Computer Security Foundations Symposium (CSF)
  Harvard University, Cambridge MA, USA, 2012
  PDF
, PPT, VAC (for tools, benchmarks and experiments)
27.
  Sequentializing Parameterized Programs
  with S. La Torre, and P. Madhusudan
  4th International Workshop on Foundations of Interface Technologies (FIT)

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

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

 
PDF, PPT, See also the cbp2bp page.
37.
  Analyzing Recursive Programs using Fixed-point Calculus
  with S. La Torre, and P. Madhusudan

  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
38.
  Improvements for Truthful Mechanisms with Verifiable One-Parameter Selfish Agents
  with A. FerranteF. Sorrentino, and C. Ventre
  Theoretical Computer Science (TCS) 2009

 
PDF
39.
  An Infinite Automaton Characterization of Double Exponential Time
 
with S. La Torre, and P. Madhusudan

  17th EACSL Annual Conference on Computer Science Logic (CSL)
  Bertinoro, Italy, 2008
  PDF, PPT

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

41.
  Context-Bounded Analysis of Concurrent Queue Systems
  with S. La Torre, and P. Madhusudan

  14th Int'l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
  Budapest, Hungary, 2008
  PDF, PPT

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

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

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

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

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

47.
  Minimum Weighted Feedback Vertex Set on Diamonds
  with F. Carrabs, R. Cerulli, and M. Gentili
  Electronic Notes in Discrete Mathematics (ENDM), 2004
  PDF
48.
  Hierarchical and Recursive State Machines with Context-Dependent Properties
  with S. La Torre, M. Napoli, and M. Parente
  30th Int'l Colloquium on Automata, Languages and Programming (ICALP)
  Eindhoven, The Netherlands, 2003
  PDF
, PPT
49.
  Looking at Computations from a Different Angle
  with O. Inverso, S. La Torre, E. Tomasco
  Technical report, 2013
  PDF