Gennaro Parlato

Short Bio

Gennaro Parlato is a Full Professor of Computer Science at the University of Molise (UNIMOL), where he leads the Program Analysis in the Clouds Lab (PAC Lab). His research is in formal methods, with a focus on automated verification, program analysis, logic, automata theory, and constrained Horn clauses.

His work develops rigorous and scalable techniques for proving correctness properties of complex systems. He has worked on concurrent and recursive programs, heap- and tree-manipulating programs, access-control policies, and security-critical software. This research combines theoretical foundations with tool development, including decidable logics, automata-based methods, symbolic model checking, CHC-based verification, and game-based approaches to synthesis and planning.

At PAC Lab, his team develops verification techniques and tools for analysing real software systems. These include CSeq and Iekkë for concurrent C programs, STRAND for reasoning about heap structures, VAC for access-control policy analysis, and GetAFix for recursive programs. Tools developed in his research group have received 14 medals in the Concurrency category of the International Competition on Software Verification (SV-COMP), and his work on distributed symbolic analysis received an Amazon Research Award.

Before joining UNIMOL, Gennaro held postdoctoral positions at the University of Illinois at Urbana-Champaign and at LIAFA/IRIF in Paris. From 2011 to 2018, he was a faculty member at the University of Southampton (UK), where he became Associate Professor in the School of Electronics and Computer Science and contributed to the GCHQ/EPSRC Academic Centre of Excellence for Cyber Security Research.

His full CV is available here.

Research Areas

• Automated software verification and program analysis
• Formal methods for concurrent, recursive, heap- and tree-manipulating programs
• Constrained Horn clauses, automata theory, and decidable logics
• Program synthesis, games, planning, and temporal reasoning
• Security verification and access-control policies

Grants

• Amazon Research Awards (ARA) (Principal Investigator):Program Analysis in the Clouds (PAC). (Aug 2021–Aug 2022)
• EPSRC Grant EP/P022413/1 (Co-Investigator):VAC+: Verifier of Access Control. (Aug 2017–Aug 2018)
• EPSRC Grant EP/M008991/1 (Principal Investigator):CONSEQUENCER. (Mar 2015–Aug 2016)
• GCHQ Grant (Co-Investigator):Language-based security for distributed ledgers. (Dec 2015–Mar 2016)

Honors and Awards

• Amazon Research Award, Spring 2021
• Best Paper Award at the 12th International Conference on Networked Systems (NETYS), 2024
• 14 Medals at the International Competition on Software Verification (SV-COMP)(5 Gold, 7 Silver, 2 Bronze in Concurrency Category)
• Fellow of The Higher Education Academy (UKSPF Descriptor 2), Mar 2014

Software/Tools

• Iekkë: SAT-based bounded-round verifier for multi-threaded C programs; bronze medal at SV-COMP 2026.
• CSeq: Sequentialization framework for concurrent C program verification; basis for several SV-COMP medal-winning tools.
• GetAFix: A Symbolic Model-Checker for Recursive Programs
• STRAND: Decidable Logics / SMT Solver for Reasoning with Heaps
• VAC: Verifier of Access Control
• PAC: Program Analysis in the Clouds

PhD Students Supervised

• Enrico Steffinlongo (Oct 2016–Feb 2018)Currently Software Engineer at GitHub, UK.
• Truc Lam Nguyen (Oct 2013–May 2017)Currently Senior Data Engineer at Jagex, Cambridge, UK.
• Ermenegildo Tomasco (May 2012–May 2017)Currently Official at Italian Income Revenue Authority, Italy.
• Omar Inverso (Oct 2011–Oct 2015)Currently Associate Professor at Gran Sasso Science Institute (GSSI), Italy.

Postdoctoral Researchers

• Giulio Garbi (2022–2024)
• Mikhail Ramalho (2016)
• Truc Lam Nguyen (2016)
• Omar Inverso (2015)

BSc & MSc Research Students

• Paolo Di BiaseCurrently PhD student at GSSI. Co-author of the Iekkë verifier (TACAS '26).
• Nicola GentileResearch focus: Verification of Heap-manipulating programs
• Andrea Pino di CristofaroResearch focus: Symbolic partial order reduction

Program Committee Membership & Reviewing

Served as a Program Committee, Jury, or reviewer for over 26 international conferences, workshops, and competitions, including:

• International Conference on Computer-Aided Verification (CAV)
• International Conference on Software Engineering (ICSE)
• Verification, Model Checking, and Abstract Interpretation (VMCAI)
• International Competition on Software Verification (SV-COMP)

Invited Lectures

• Symbolic POR for Nearly Free: Canonical Encodings for Read-From Classes in BMCWorkshop on Verification of Distributed Systems (VDS), Agadir, Morocco, June 2026
• Verifying Tree-Manipulating Programs via CHCs
  • Gran Sasso Science Institute (GSSI), L'Aquila, Italy, Nov 2025
  • Workshop on Verification of Distributed Systems (VDS), Rabat, Morocco, May 2025
• Unifying Automata Theory and Constrained Horn Clauses for Scalable Program VerificationWorkshop on Horn Clauses for Verification and Synthesis (HCVS), Zagreb, Croatia, July 2025
• Empowering Program Verification: Harnessing Symbolic Automata and Logics on Data-trees for Automated SolutionsWorkshop on Verification of Distributed Systems (VDS), Rabat, Morocco, May 2024
• C2C-trans as a Design Methodology for Software Verification ToolsWorkshop on Democratizing Software Verification (at CAV), Haifa, Israel, Aug 2022
• Parallel Bug-finding in Concurrent Programs Via Reduced Interleaving InstancesGuest talk at Amazon (Amazon Chime), Sept 2020
• Finding Rare Concurrent Programming Bugs
  • 15th Int'l Colloquium on Theoretical Aspects of Computing (ICTAC), Stellenbosch, South Africa, Oct 2018
  • Workshop on Verification of Distributed Systems (VDS), Marrakesh, Morocco, June 2018
• A Pragmatic Bug-finding Approach for Concurrent ProgramsInstitut de Recherche en Informatique Fondamentale (IRIF), Paris, France, Nov 2016
• Security Analysis of Self-Administrated RBAC through Program VerificationInformation Security Group, Dept. of Computer Science, UCL, London, UK, July 2015
• On BMC Sequentializations of Concurrent ProgramsComputer Science Department, University of Oxford, Oxford, UK, June 2015
• On Sequentializing Concurrent ProgramsUPMARC 7th Summer School on Multicore Computing, Uppsala University, Sweden, June 2015
• Bounded Model Checking of Multi-Threaded C Programs via Lazy SequentializationLIAFA, Paris, France, May 2014
• The Tree-width of Decidable ProblemsFSTTCS post-conference workshop on Verification of Infinite-State Systems, Hyderabad, India, Dec 2012
• Sequentializing Concurrent ProgramsComputer Science Department, University of Oxford, Oxford, UK, Jan 2012
• Decidable Logics Combining Heap Structures and Data
  • LORIA-INRIA-Lorraine (CASSIS team), Nancy, France, Feb 2011
  • Workshop on Automata and Logic for Data Manipulating Programs, Paris, France, Dec 2010
  • ANR Veridyc Project, LIAFA, Paris, France, Oct 2010
• The Tree-Width of the Auxiliary Storage
  • School of Electronic Engineering and Computer Science, Queen Mary University of London, Mar 2013
  • IFIP WG 2.3: Working Group on Programming Methodology, Winchester, UK, Sept 2011
  • École normale supérieure de Cachan (ENS Cachan), Cachan, France, May 2010
  • Laboratoire Bordelais de Recherche en Informatique (LaBRI), Bordeaux, France, May 2010
  • LIAFA, Paris, France, Apr 2010
• Writing Model-Checkers for Boolean Recursive Programs using a Fixed-Point CalculusLIAFA, Paris, France, Sept 2009