Hierarchical and Recursive State Machines with Context-Dependent Properties. - Salvatore La Torre; Margherita Napoli; Mimmo Parente; Gennaro Parlato (ICALP, 2003)

Minimum Weighted Feedback Vertex Set on Diamonds. - Francesco Carrabs; Raffaele Cerulli; Monica Gentili; Gennaro Parlato (Electron. Notes Discret. Math., 2004)

Improvements for Truthful Mechanisms with Verifiable One-Parameter Selfish Agents. - Alessandro Ferrante; Gennaro Parlato; Francesco Sorrentino 002; Carmine Ventre (WAOA, 2005)

A linear time algorithm for the minimum Weighted Feedback Vertex Set on diamonds. - Francesco Carrabs; Raffaele Cerulli; Monica Gentili; Gennaro Parlato (Inf. Process. Lett., 2005)

On the Complexity of LtlModel-Checking of Recursive State Machines. - Salvatore La Torre; Gennaro Parlato (ICALP, 2007)

Verification of Succinct Hierarchical State Machines. - Salvatore La Torre; Margherita Napoli; Mimmo Parente; Gennaro Parlato (LATA, 2007)

A Robust Class of Context-Sensitive Languages. - Salvatore La Torre; Parthasarathy Madhusudan; Gennaro Parlato (LICS, 2007)

An Infinite Automaton Characterization of Double Exponential Time. - Salvatore La Torre; P. Madhusudan; Gennaro Parlato (CSL, 2008)

Context-Bounded Analysis of Concurrent Queue Systems. - Salvatore La Torre; P. Madhusudan; Gennaro Parlato (TACAS, 2008)

Verification of scope-dependent hierarchical state machines. - Salvatore La Torre; Margherita Napoli; Mimmo Parente; Gennaro Parlato (Inf. Comput., 2008)

Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. - Salvatore La Torre; P. Madhusudan; Gennaro Parlato (CAV, 2009)

Analyzing recursive programs using a fixed-point calculus. - Salvatore La Torre; Parthasarathy Madhusudan; Gennaro Parlato (PLDI, 2009)

Fast payment schemes for truthful mechanisms with verification. - Alessandro Ferrante; Gennaro Parlato; Francesco Sorrentino 002; Carmine Ventre (Theor. Comput. Sci., 2009)

Model-Checking Parameterized Concurrent Programs Using Linear Interfaces. - Salvatore La Torre; P. Madhusudan; Gennaro Parlato (CAV, 2010)

The Language Theory of Bounded Context-Switching. - Salvatore La Torre; Parthasarathy Madhusudan; Gennaro Parlato (LATIN, 2010)

Getting Rid of Store-Buffers in TSO Analysis. - Mohamed Faouzi Atig; Ahmed Bouajjani; Gennaro Parlato (CAV, 2011)

A Tabu Search Heuristic Based on k-Diamonds for the Weighted Feedback Vertex Set Problem. - Francesco Carrabs; Raffaele Cerulli; Monica Gentili; Gennaro Parlato (INOC, 2011)

The tree width of auxiliary storage. - P. Madhusudan; Gennaro Parlato (POPL, 2011)

Decidable logics combining heap structures and data. - P. Madhusudan; Gennaro Parlato; Xiaokang Qiu (POPL, 2011)

On Sequentializing Concurrent Programs. - Ahmed Bouajjani; Michael Emmi; Gennaro Parlato (SAS, 2011)

Security Analysis of Role-Based Access Control through Program Verification. - Anna Lisa Ferrara; P. Madhusudan; Gennaro Parlato (CSF, 2012)

Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width. - Salvatore La Torre; Gennaro Parlato (FSTTCS, 2012)

Analyzing temporal role based access control models. - Emre Uzun; Vijayalakshmi Atluri; Shamik Sural; Jaideep Vaidya; Gennaro Parlato; Anna Lisa Ferrara; Parthasarathy Madhusudan (SACMAT, 2012)

Sequentializing Parameterized Programs - Salvatore La Torre; P. Madhusudan; Gennaro Parlato (FIT, 2012)

CSeq: A concurrency pre-processor for sequential C verification tools. - Bernd Fischer 002; Omar Inverso; Gennaro Parlato (ASE, 2013)

Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists. - Pranav Garg 001; P. Madhusudan; Gennaro Parlato (SAS, 2013)

CSeq: A Sequentialization Tool for C - (Competition Contribution). - Bernd Fischer 002; Omar Inverso; Gennaro Parlato (TACAS, 2013)

Policy Analysis for Self-administrated Role-Based Access Control. - Anna Lisa Ferrara; P. Madhusudan; Gennaro Parlato (TACAS, 2013)

Vac - Verifier of Administrative Role-Based Access Control Policies. - Anna Lisa Ferrara; P. Madhusudan; Truc L. Nguyen; Gennaro Parlato (CAV, 2014)

Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. - Omar Inverso; Ermenegildo Tomasco; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (CAV, 2014)

Context-Bounded Analysis of TSO Systems. - Mohamed Faouzi Atig; Ahmed Bouajjani; Gennaro Parlato (FPS@ETAPS, 2014)

A Unifying Approach for Multistack Pushdown Automata. - Salvatore La Torre; Margherita Napoli; Gennaro Parlato (MFCS (1), 2014)

Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution). - Omar Inverso; Ermenegildo Tomasco; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (TACAS, 2014)

MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution). - Ermenegildo Tomasco; Omar Inverso; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (TACAS, 2014)

On the Path-Width of Integer Linear Programming. - Constantin Enea; Peter Habermehl; Omar Inverso; Gennaro Parlato (GandALF, 2014)

Security analysis for temporal role based access control. - Emre Uzun; Vijayalakshmi Atluri; Jaideep Vaidya; Shamik Sural; Anna Lisa Ferrara; Gennaro Parlato; P. Madhusudan (J. Comput. Secur., 2014)

Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs. - Omar Inverso; Truc L. Nguyen; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (ASE, 2015)

Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches - (Competition Contribution). - Truc L. Nguyen; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (TACAS, 2015)

MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings - (Competition Contribution). - Ermenegildo Tomasco; Omar Inverso; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (TACAS, 2015)

Verifying Concurrent Programs by Memory Unwinding. - Ermenegildo Tomasco; Omar Inverso; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (TACAS, 2015)

Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs. - Truc L. Nguyen; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (ATVA, 2016)

Lazy sequentialization for TSO and PSO via shared memory abstractions. - Ermenegildo Tomasco; Truc L. Nguyen; Omar Inverso; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (FMCAD, 2016)

MU-CSeq 0.4: Individual Memory Location Unwindings - (Competition Contribution). - Ermenegildo Tomasco; Truc L. Nguyen; Omar Inverso; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (TACAS, 2016)

Scope-Bounded Pushdown Languages. - Salvatore La Torre; Margherita Napoli; Gennaro Parlato (Int. J. Found. Comput. Sci., 2016)

Preventing Unauthorized Data Flows. - Emre Uzun; Gennaro Parlato; Vijayalakshmi Atluri; Anna Lisa Ferrara; Jaideep Vaidya; Shamik Sural; David Lorenzi (DBSec, 2017)

Parallel bug-finding in concurrent programs via reduced interleaving instances. - Truc L. Nguyen; Peter Schrammel; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (ASE, 2017)

Concurrent Program Verification with Lazy Sequentialization and Interval Analysis. - Truc L. Nguyen; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (NETYS, 2017)

Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models. - Ermenegildo Tomasco; Truc Lam Nguyen; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (SEFM, 2017)

Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation - (Competition Contribution). - Truc L. Nguyen; Omar Inverso; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (TACAS (2), 2017)

Model Checking BDI Logics over Finite-state Worlds. - Salvatore La Torre; Gennaro Parlato (OVERLAY@AI*IA, 2019)

VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-threaded Programs with Lazy-CSeq. - Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (ASE, 2019)

On the Model-Checking of Branching-time Temporal Logic with BDI Modalities. - Salvatore La Torre; Gennaro Parlato (AAMAS, 2020)

A Fixed-point Model-checker for BDI Logics over Finite-state Worlds. - Salvatore La Torre; Gennaro Parlato (OVERLAY, 2020)

Reachability of scope-bounded multistack pushdown systems. - Salvatore La Torre; Margherita Napoli; Gennaro Parlato (Inf. Comput., 2020)

Automated Planning Through Program Verification. - Salvatore La Torre; Gennaro Parlato (OVERLAY@GandALF, 2021)

Reasoning About Data Trees Using CHCs. - Marco Faella; Gennaro Parlato (CAV (2), 2022)

CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory. - Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato; Peter Schrammel (ASE, 2022)

Bounded Verification of Multi-threaded Programs via Lazy Sequentialization. - Omar Inverso; Ermenegildo Tomasco; Bernd Fischer 002; Salvatore La Torre; Gennaro Parlato (ACM Trans. Program. Lang. Syst., 2022)

Reachability Games Modulo Theories with a Bounded Safety Player. - Marco Faella; Gennaro Parlato (AAAI, 2023)

Verifying Programs by Bounded Tree-Width Behavior Graphs. - Omar Inverso; Salvatore La Torre; Gennaro Parlato; Ermenegildo Tomasco (EUMAS, 2023)

A Unified Automata-Theoretic Approach to LTLf Modulo Theories. - Marco Faella; Gennaro Parlato (ECAI, 2024)

Static Data Race Detection via Lazy Sequentialization. - Bernd Fischer 002; Giulio Garbi; Salvatore La Torre; Gennaro Parlato; Peter Schrammel (NETYS, 2024)

A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version). - Marco Faella; Gennaro Parlato (CoRR, 2024)

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses. - Marco Faella; Gennaro Parlato (CoRR, 2024)

CHC-Based Verification of Programs Through Graph Decompositions. - Marco Faella; Giulio Garbi; Salvatore La Torre; Gennaro Parlato (SN Comput. Sci., 2024)

Verifying Tree-Manipulating Programs via CHCs. - Marco Faella; Gennaro Parlato (CAV (1), 2025)