Gennaro Parlato





Short Bio

Dr Gennaro Parlato is 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

   
- Enrico Steffinlongo       [ Visinting PhD student from the University Ca' Foscari, Italy,
                                                     Advisor Michele Bugliesi,  Oct 2016-present
]
     
Working on verification of Access Control

   - Mikhail Ramalho
     
(Feb 2015-present, 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)



Teaching

   - COMP1201: Algorithmics                                         (2017-18)
   - COMP2210: Theory of Computing                            (2017-18)

   - COMP1201: Algorithmics                                         (2016-17)
   - COMP6233: Topics in Computer Science                 (2016-17)
   - 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


   - PC Member: LATA 2017, Umeň, Sweden
     11th Int'l Conference on Language and Automata Theory and Applications  

   - 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



Papers     (DBLP, Google Scholar)
Contact Information
1.
  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
2.
  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
3.
   Preventing Unauthorized Data Flows
  E. Uzun, G. Parlato, V. Atluri, A. L. Ferrara, J. Vaidya, S. Sural, D. Lorenzi
  Conference on Data and Applications Security and Privacy (DBSec)
  Philadelphia, PA, USA, 2017
  PDF
4.
  Concurrent Program Verification with Lazy Sequentialization and Interval Analysis
  T. L. Nguyen, B. Fischer, S. La Torre, G. Parlato
  Networked Systems - 5th Intl. Conference (NETYS)
  Marrakech, Marocco, 2017
  PDF
5.
  Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution).
 
T. L. Nguyen, O. Inverso, B. Fischer, S. La Torre, G. Parlato
  6th Intl. Competition on Software Verification (SV-COMP), held at TACAS
  Uppsala, Sweden, 2017
  PDF
6.
  On the Path-Width of Integer Linear Programming
  with C. Enea, P. Habermehl, O. Inverso
  Information and Computation, 2017
  PDF
7.
  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
8.
  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
9.
  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
10.
  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

11.
  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]
12.
  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
13.
  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
14.
  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
15.
  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
16.
  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
17.
  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
18.
  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
19.
  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
20.
  Context-Bounded Analysis of TSO Systems
  with F. M. Atig, and A. Bouajjani

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

21.
  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

22.
  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

23.
  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'')
24.
  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
25.
  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
26.
  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
27.
  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)
28.
  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
29.
  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)
30.
  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)
31.
  Sequentializing Parameterized Programs
  with S. La Torre, and P. Madhusudan
  4th International Workshop on Foundations of Interface Technologies (FIT)

  Tallinn, Estonia, 2012
  PDF
, PPT
32.
  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
33.
  On Sequentializing Concurrent Programs
  with A. Bouajjani, and M. Emmi
  18th Int'l Static Analysis Symposium (SAS)
  Venice, Italy, 2011
  PDF
, PPT
34.
  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
35.
  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
36.
  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
37.
  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
38.
  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

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

 
PDF
43.
  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

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

45.
  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

46.
  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

47.
  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

48.
  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

49.
  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

50.
  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

51.
  Minimum Weighted Feedback Vertex Set on Diamonds
  with F. Carrabs, R. Cerulli, and M. Gentili
  Electronic Notes in Discrete Mathematics (ENDM), 2004
  PDF
52.
  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
53.
  Looking at Computations from a Different Angle
  with O. Inverso, S. La Torre, E. Tomasco
  Technical report, 2013
  PDF