Contact Information
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 verification and formal methods
- Program Synthesis and Machine Learning
- Security and Privacy
- Logic and automata theory
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-PI):
Language-based security for smart contracts. (Dec 2015-Mar 2016)
Honors and Awards
- Amazon Research Award, Spring 2021
- 14 Medals at the Int'l 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ë: Bounded Model Checker for Concurrent C Programs
- CSeq: Sequentialization framework for concurrent C programs
- GetAFix: A Boolean program checker
- STRAND: Decidable logics/SMT solver for reasoning with heaps
- VAC: Verifier for Role Based Access Control Systems
- PAC: Program Analysis in the Clouds
PhD Students Supervised
- Dr. Enrico Steffinlongo (Oct 2016-Feb 2018)
Currently Software Engineer at GitHub, UK.
- Dr. Mikhail Ramalho (Feb 2015-Dec 2018)
Co-advised with Denis A. Nicole
- Dr. Truc Lam Nguyen (Oct 2013-May 2017)
Currently Senior Data Engineer at Jagex, Cambridge, UK.
- Dr. 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 Biase
Currently PhD student at GSSI. Co-author of the Iekkë verifier (TACAS '26).
- Nicola Gentile
Research focus: Verification of Heap-manipulating programs
- Andrea Pino di Cristofaro
Research focus: Symbolic partial order reduction
Professional Activities & Service
Served as a Program Committee or Jury member for over 25 international conferences, workshops, and competitions. Selected top-tier venues include:
- International Conference on Computer-Aided Verification (CAV)
- International Conference on Software Engineering (ICSE)
- Int'l Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
Selected Invited Lectures
- Symbolic POR for Nearly Free: Canonical Encodings for Read-From Classes in BMC
Workshop 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 Verification
Workshop on Horn Clauses for Verification and Synthesis (HCVS), Zagreb, Croatia, July 2025
- C2C-trans as a Design Methodology for Software Verification Tools
Workshop on Democratizing Software Verification (at CAV), Haifa, Israel, Aug 2022
- Parallel Bug-finding in Concurrent Programs Via Reduced Interleaving Instances
Guest talk at Amazon (Amazon Chime), Sept 2020
| Teaching | |
| University of Molise, Italy | |
| - Algorithms and Data Structures | ( 2018/19 – 2023/24 ) |
| - Program Analysis & Security | ( 2019/20 – 2022/23 ) |
| - Theory of Computing | ( 2022/23 ) |
| University of Southampton, UK |
|
| - Theory of Computing | ( 2012/13 – 2018/19 ) |
| - Formal Methods & Automated Verif. | ( 2011/12 – 2014/15 ) |
| - Advanced Topics in Computer Science | ( 2015/16 – 2016/17 ) |
| 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) |
Iekkë: A SAT-Based Bounded-Round Verifier for Multi-Threaded Programs
(Competition Contribution)
P. Di Biase, B. Fischer, S. La Torre, P. Schrammel, and G. Parlato
32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Turin, Italy, 2026
PDF
(Competition Contribution)
P. Di Biase, B. Fischer, S. La Torre, P. Schrammel, and G. Parlato
32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Turin, Italy, 2026
Verifying Tree-Manipulating Programs via CHCs
M. Faella, and G. Parlato
37th International Conference on Computer Aided Verification (CAV)
Zagreb, Croatia, 2025
PDF, Extended Version
M. Faella, and G. Parlato
37th International Conference on Computer Aided Verification (CAV)
Zagreb, Croatia, 2025
PDF, Extended Version
A Unified Automata-Theoretic Approach to LTLf Modulo Theories
M. Faella, and G. Parlato
27th European Conference on Artificial Intelligence (ECAI)
Santiago de Compostela, Spain, 2024
PDF, Extended Version
M. Faella, and G. Parlato
27th European Conference on Artificial Intelligence (ECAI)
Santiago de Compostela, Spain, 2024
PDF, Extended Version
Static Data Race Detection via Lazy Sequentialization
M. Faella, G. Garbi, S. La Torre, and G. Parlato
12th International Conference on Networked Systems (NETYS)
Rabat, Marocco, 2024
PDF (Best paper award)
M. Faella, G. Garbi, S. La Torre, and G. Parlato
12th International Conference on Networked Systems (NETYS)
Rabat, Marocco, 2024
PDF (Best paper award)
CHC-Based Verification of Programs Through Graph Decompositions
B. Fischer, G. Garbi, S. La Torre, G. Parlato, and P. Schrammel
SN Computer Science journal (accepted for publication), 2024
PDF
B. Fischer, G. Garbi, S. La Torre, G. Parlato, and P. Schrammel
SN Computer Science journal (accepted for publication), 2024
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
M. Faella, and G. Parlato
37th AAAI Conference on Artificial Intelligence (AAAI)
Washingtonm DC, USA, 2023
PDF, Recorded Presentation, Artifact
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
O. Inverso, S. La Torre, G. Parlato, and E. Tomasco
Multi-Agent Systems - 20th European Conference (EUMAS),
Naples, Italy, 2023
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
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
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)
M. Faella, and G. Parlato
34th Int'l Conference on Computer Aided Verification (CAV)
Haifa, Israel, 2022
PDF, PPT, Artifact (10MB zip)
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
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
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
S. La Torre, and G. Parlato
19th International Conference on Autonomous Agents and Multiagent Systems (AAMAS)
Auckland, New Zealand, 2020
Reachability of Scope-bounded Multistack Pushdown Systems
S. La Torre, M. Napoli, and G. Parlato
Information and Computation, 2020
PDF
S. La Torre, M. Napoli, and G. Parlato
Information and Computation, 2020
A Fixed-point Model-checker for BDI Logics over Finite-state Worlds
S. La Torre, and G. Parlato
2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata,
and Synthesis (OVERLAY)
Bolzano, Italy, 2020
PDF
S. La Torre, and G. Parlato
2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata,
and Synthesis (OVERLAY)
Bolzano, Italy, 2020
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
B. Fischer, S. La Torre, and G. Parlato
34th IEEE/ACM International Conference on Automated Software Engineering (ASE)
San Diego, CA, USA, 2019
Model Checking BDI Logics over Finite-state Worlds
S. La Torre, and G. Parlato
1st Workshop on Artificial Intelligence and Formal Verification, Logic, Automata,
and Synthesis (OVERLAY)
Rende, Italy, 2019
PDF
S. La Torre, and G. Parlato
1st Workshop on Artificial Intelligence and Formal Verification, Logic, Automata,
and Synthesis (OVERLAY)
Rende, Italy, 2019
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
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
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
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
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
T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato
Networked Systems - 5th Intl. Conference (NETYS)
Marrakech, Marocco, 2017
PDF, PPT
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
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
On the Path-Width of Integer Linear Programming
C. Enea, P. Habermehl, O. Inverso, and G. Parlato
Information and Computation, 2017
PDF
C. Enea, P. Habermehl, O. Inverso, and G. Parlato
Information and Computation, 2017
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
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
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
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
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
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
MU-CSeq 0.4: Individual Memory Location Unwindings (Competition Contribution)
E. Tomasco, T. L. Nguyen, O. Inverso, B. Fischer, S. 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
E. Tomasco, T. L. Nguyen, O. Inverso, B. Fischer, S. 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
Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-Threaded C-Programs
(Tool Demonstration)
O. Inverso, T. L. Nguyen, B. Fischer, S. 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]
(Tool Demonstration)
O. Inverso, T. L. Nguyen, B. Fischer, S. 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]
Verifying Concurrent Programs by Memory Unwinding
E. Tomasco, O. Inverso, B. Fischer, S. 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
E. Tomasco, O. Inverso, B. Fischer, S. 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
MU-CSeq 0.3: Sequentialization by Read-implicit and Coarse-grained Memory Unwindings
(Competition Contribution)
E. Tomasco, O. Inverso, B. Fischer, S. 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
(Competition Contribution)
E. Tomasco, O. Inverso, B. Fischer, S. 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
Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded
Context Switches (Competition Contribution)
T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato
4th Intl. Competition on Software Verification (SV-COMP), held at TACAS
London, UK, 2015
PDF, PPT, CSeq webpage
Context Switches (Competition Contribution)
T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato
4th Intl. Competition on Software Verification (SV-COMP), held at TACAS
London, UK, 2015
PDF, PPT, CSeq webpage
Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization
O. Inverso, E. Tomasco, B. Fischer, S. 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
O. Inverso, E. Tomasco, B. Fischer, S. 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
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
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
Lazy-CSeq: A Lazy Sequentialization Tool for C (Competition Contribution)
O. Inverso, E. Tomasco, S. 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
O. Inverso, E. Tomasco, S. 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
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
(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
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
F. M. Atig, A. Bouajjani, and G. Parlato
ETAPS Workshop in honor of Joseph Sifakis
Grenoble, France, 2014
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
S. La Torre, M. Napoli, and G. Parlato
39th International Symposium on Mathematical Foundations of Computer Science (MFCS)
Budapest, Hungary, 2014
PDF, PPT
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
S. La Torre, M. Napoli, and G. Parlato
18th International Conference on Developments in Language Theory (DLT)
Ekaterinburg, Russia, 2014
PDF (full version), PPT
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'')
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'')
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
E. Uzun, V. Atluri, J. Vaidya, S. Sural, A. L. Ferrara, G. Parlato, and P. Madhusudan
Journal of Computer Security (JCS), 2014
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
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
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
P. Garg, P. Madhusudan, and G. Parlato
20th Static Analysis Symposium (SAS)
Seattle, WA, USA, 2013
PDF, PPT, Experiments
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)
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)
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 [CSEQ won the silver medal in the concurrency category]
PDF, CSeq webpage
B. Fischer, and O. Inverso, and G. Parlato
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
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)
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)
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)
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)
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
S. La Torre, P. Madhusudan, and G. Parlato
4th International Workshop on Foundations of Interface Technologies (FIT)
Tallinn, Estonia, 2012
PDF, PPT
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
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
On Sequentializing Concurrent Programs
A. Bouajjani, M. Emmi, G. Parlato
18th Int'l Static Analysis Symposium (SAS)
Venice, Italy, 2011
PDF, PPT
A. Bouajjani, M. Emmi, G. Parlato
18th Int'l Static Analysis Symposium (SAS)
Venice, Italy, 2011
PDF, PPT
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
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
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
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
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
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
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
F. Carrabs, R. Cerulli, M. Gentili, and G. Parlato
Network Optimization: 5th International Conference, (INOC)
Hamburg, Germany, 2011
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
S. La Torre, P. Madhusudan, and G. Parlato
22nd Int'l Conference on Computer Aided Verification (CAV)
Edinburgh, UK, 2010
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
S. La Torre, P. Madhusudan, G. Parlato
9th Latin American Theoretical Informatics Symposium (LATIN)
Oaxaca, Mexico, 2010
PDF, PPT
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.
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.
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
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
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
S. La Torre, P. Madhusudan, and G. Parlato
17th EACSL Annual Conference on Computer Science Logic (CSL)
Bertinoro, Italy, 2008
PDF, PPT
Verification of Scope-Dependent Hierarchical State Machines
S. La Torre, M. Napoli, M. Parente, and G. Parlato
Information and Computation 2008
PDF
S. La Torre, M. Napoli, M. Parente, and G. Parlato
Information and Computation 2008
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
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
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
S. La Torre, P. Madhusudan, and G. Parlato
22nd IEEE Symp. on Logic in Computer Science (LICS)
Wroclaw, Poland, 2007
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
S. La Torre, and G. Parlato
34th Int'l Colloquium on Automata, Languages and Programming (ICALP)
Wroclaw, Poland, 2007
Verification of Succinct Hierarchical State Machines
S. La Torre, M. Napoli, M. Parente, and G. Parlato
1st Int'l Conference on Language and Automata Theory and Applications (LATA)
Tarragona, Spain, 2007
PDF
S. La Torre, M. Napoli, M. Parente, and G. Parlato
1st Int'l Conference on Language and Automata Theory and Applications (LATA)
Tarragona, Spain, 2007
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
F. Carrabs, R. Cerulli, and M. Gentili, and G. Parlato
Information Processing Letters (IPL), 2005
Minimum Weighted Feedback Vertex Set on Diamonds
F. Carrabs, R. Cerulli, M. Gentili, and G. Parlato
Electronic Notes in Discrete Mathematics (ENDM), 2004
PDF
F. Carrabs, R. Cerulli, M. Gentili, and G. Parlato
Electronic Notes in Discrete Mathematics (ENDM), 2004
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
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