Gennaro Parlato






Current Position

I am a Lecturer of Computer Science in the School of Electronics and Computer Science at the University of Southampton. I am a member of the Electronic & Software Systems (ESS) research group, and  GCHQ-funded Academic Centre of Excellence in Cybersecurity Southampton.



Short Biography

I received my Doctoral degree in Computer Science from the University of Salerno,  Italy, in April 2006. Before joining the University of Southampton as a Lecturer, I have been a postdoc research associate in the Department of Computer Science at UIUC (Urbana, USA, May 2006-March 2010), and a CNRS postdoc research associate in the Modeling and Verification research group at LIAFA laboratory (Paris, France, April 2010-April 2011).  

My 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 abstractions 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

Software/Tools

   - CSeq - Sequentialization tool for concurrent C programs with Pthread library
   - 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 (April 2015 - October 2015)  

Teaching

   - COMP2210: Theory of Computing                 (2015-2016)
   - COMP6233: Topics in Computer Science       (2015-2016)
   - Lecture series at
UPMARC Summer School on Multicore Computing
    
Slides (Part1, Part2)                                                         (June 2015)
   - COMP6210: Automated Software Verification (2014-2015)
   - COMP2210: Theory of Computing                  (2014-2015)
   - COMP6004: Formal Design of Systems           (2013-2014)
  
- COMP2210: Theory of Computing                  (2013-2014)
   - COMP6004: Formal Design of Systems           (2012-2013)
  
- COMP2011: Theory of Computing                  (2012-2013)
   - COMP6004: Formal Design of Systems           (2011-2012)

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

5.
  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]
6.
  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
7.
  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
8.
  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
9.
  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
10.
  Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization
 
O. Inverso,  E. 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
11.
  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
12.
  Lazy-CSeq: A Lazy Sequentialization Tool for C (Competition Contribution)
 
O. Inverso,  E. 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
13.
  MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings (Competition Contribution)
 
E. Tomasco, O. Inverso,  S. 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
14.
  Context-Bounded Analysis of TSO Systems
  with F. M. Atig, and A. Bouajjani
.
 
ETAPS Workshop in honor of Joseph Sifakis
  Grenoble, France, 2014.
  PDF

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

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

17.
  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'').
18.
  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
19.
  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
20.
  Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists
  with P. Garg, P. Madhusudan.
  20th Static Analysis Symposium (SAS),
  Seattle, WA, USA, 2013.

 
PDF, PPT, Experiments.
21.
  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)
22.
  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.
  [Cseq won the silver medal in the concurrency category]
  PDF, CSeq webpage
23.
  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)
24.
  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)
25.
  Sequentializing Parameterized Programs
  with S. La Torre, and P. Madhusudan
.
  4th International Workshop on Foundations of Interface Technologies (FIT).

  Tallinn, Estonia, 2012.
  PDF
, PPT
26.
  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
27.
  On Sequentializing Concurrent Programs
  with A. Bouajjani, and M. Emmi
.
  18th Int'l Static Analysis Symposium (SAS).
  Venice, Italy, 2011.
  PDF
, PPT
28.
  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
29.
  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
30.
  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
31.
  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
32.
  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

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

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

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

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

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

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

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

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

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

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