Gennaro Parlato

72 papers A* 17A 12B 9C 6Misc 1Journal 14Unranked 13
YearRankTypeTitle / Venue / Authors
2026 — conf
Iekkë: A SAT-Based Bounded-Round Verifier for Multi-Threaded Programs (Competition Contribution).
TACAS (2)
Paolo Di Biase, Bernd Fischer, Salvatore La Torre, Peter Schrammel, Gennaro Parlato
2025 — conf
Verifying Tree-Manipulating Programs via CHCs.
CAV (1)
Marco Faella, Gennaro Parlato
2025 J jnl
Verifying Tree-Manipulating Programs via CHCs.
CoRR
Marco Faella, Gennaro Parlato
2024 A conf
A Unified Automata-Theoretic Approach to LTL
ECAI
Marco Faella, Gennaro Parlato
2024 J jnl
A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version).
CoRR
Marco Faella, Gennaro Parlato
2024 J jnl
Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses.
CoRR
Marco Faella, Gennaro Parlato
2024 J jnl
CHC-Based Verification of Programs Through Graph Decompositions.
SN Comput. Sci.
Marco Faella, Giulio Garbi, Salvatore La Torre, Gennaro Parlato
2024 — conf
Static Data Race Detection via Lazy Sequentialization.
NETYS
Bernd Fischer, Giulio Garbi, Salvatore La Torre, Gennaro Parlato, Peter Schrammel
2023 A* conf
Reachability Games Modulo Theories with a Bounded Safety Player.
AAAI
Marco Faella, Gennaro Parlato
2023 C conf
Verifying Programs by Bounded Tree-Width Behavior Graphs.
EUMAS
Omar Inverso, Salvatore La Torre, Gennaro Parlato, Ermenegildo Tomasco
2022 J jnl
Bounded Verification of Multi-threaded Programs via Lazy Sequentialization.
ACM Trans. Program. Lang. Syst.
Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2022 A* conf
CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory.
ASE
Bernd Fischer, Salvatore La Torre, Gennaro Parlato, Peter Schrammel
2022 — conf
Reasoning About Data Trees Using CHCs.
CAV (2)
Marco Faella, Gennaro Parlato
2021 — conf
Automated Planning Through Program Verification.
OVERLAY@GandALF
Salvatore La Torre, Gennaro Parlato
2020 — conf
A Fixed-point Model-checker for BDI Logics over Finite-state Worlds.
OVERLAY
Salvatore La Torre, Gennaro Parlato
2020 A conf
On the Model-Checking of Branching-time Temporal Logic with BDI Modalities.
AAMAS
Salvatore La Torre, Gennaro Parlato
2020 J jnl
Reachability of scope-bounded multistack pushdown systems.
Inf. Comput.
Salvatore La Torre, Margherita Napoli, Gennaro Parlato
2019 — conf
Model Checking BDI Logics over Finite-state Worlds.
OVERLAY@AI*IA
Salvatore La Torre, Gennaro Parlato
2019 A* conf
VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-threaded Programs with Lazy-CSeq.
ASE
Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2017 — conf
Concurrent Program Verification with Lazy Sequentialization and Interval Analysis.
NETYS
Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2017 — conf
Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation - (Competition Contribution).
TACAS (2)
Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2017 J jnl
On the path-width of integer linear programming.
Inf. Comput.
Constantin Enea, Peter Habermehl, Omar Inverso, Gennaro Parlato
2017 A* conf
Parallel bug-finding in concurrent programs via reduced interleaving instances.
ASE
Truc L. Nguyen, Peter Schrammel, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2017 B conf
Preventing Unauthorized Data Flows.
DBSec
Emre Uzun, Gennaro Parlato, Vijayalakshmi Atluri, Anna Lisa Ferrara, Jaideep Vaidya, Shamik Sural, David Lorenzi
2017 B conf
Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models.
SEFM
Ermenegildo Tomasco, Truc Lam Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2016 B conf
Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs.
ATVA
Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2016 B conf
Lazy sequentialization for TSO and PSO via shared memory abstractions.
FMCAD
Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2016 A conf
MU-CSeq 0.4: Individual Memory Location Unwindings - (Competition Contribution).
TACAS
Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2016 J jnl
Scope-Bounded Pushdown Languages.
Int. J. Found. Comput. Sci.
Salvatore La Torre, Margherita Napoli, Gennaro Parlato
2015 A* conf
Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs.
ASE
Omar Inverso, Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2015 A conf
MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings - (Competition Contribution).
TACAS
Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2015 A conf
Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches - (Competition Contribution).
TACAS
Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2015 A conf
Verifying Concurrent Programs by Memory Unwinding.
TACAS
Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2014 — conf
A Unifying Approach for Multistack Pushdown Automata.
MFCS (1)
Salvatore La Torre, Margherita Napoli, Gennaro Parlato
2014 A* conf
Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization.
CAV
Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2014 — conf
Context-Bounded Analysis of TSO Systems.
FPS@ETAPS
Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato
2014 A conf
Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution).
TACAS
Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2014 A conf
MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution).
TACAS
Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
2014 — conf
On the Path-Width of Integer Linear Programming.
GandALF
Constantin Enea, Peter Habermehl, Omar Inverso, Gennaro Parlato
2014 C conf
Scope-Bounded Pushdown Languages.
Developments in Language Theory
Salvatore La Torre, Margherita Napoli, Gennaro Parlato
2014 J jnl
Security analysis for temporal role based access control.
J. Comput. Secur.
Emre Uzun, Vijayalakshmi Atluri, Jaideep Vaidya, Shamik Sural, Anna Lisa Ferrara, Gennaro Parlato, P. Madhusudan
2014 A* conf
Vac - Verifier of Administrative Role-Based Access Control Policies.
CAV
Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen, Gennaro Parlato
2013 A conf
CSeq: A Sequentialization Tool for C - (Competition Contribution).
TACAS
Bernd Fischer, Omar Inverso, Gennaro Parlato
2013 A* conf
CSeq: A concurrency pre-processor for sequential C verification tools.
ASE
Bernd Fischer, Omar Inverso, Gennaro Parlato
2013 A conf
Policy Analysis for Self-administrated Role-Based Access Control.
TACAS
Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato
2013 B conf
Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists.
SAS
Pranav Garg, P. Madhusudan, Gennaro Parlato
2013 J jnl
Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists
CoRR
Pranav Garg, P. Madhusudan, Gennaro Parlato
2012 C conf
Analyzing temporal role based access control models.
SACMAT
Emre Uzun, Vijayalakshmi Atluri, Shamik Sural, Jaideep Vaidya, Gennaro Parlato, Anna Lisa Ferrara, Parthasarathy Madhusudan
2012 — conf
Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width.
FSTTCS
Salvatore La Torre, Gennaro Parlato
2012 A conf
Security Analysis of Role-Based Access Control through Program Verification.
CSF
Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato
2012 Misc conf
Sequentializing Parameterized Programs
FIT
Salvatore La Torre, P. Madhusudan, Gennaro Parlato
2011 C conf
A Tabu Search Heuristic Based on k-Diamonds for the Weighted Feedback Vertex Set Problem.
INOC
Francesco Carrabs, Raffaele Cerulli, Monica Gentili, Gennaro Parlato
2011 A* conf
Decidable logics combining heap structures and data.
POPL
P. Madhusudan, Gennaro Parlato, Xiaokang Qiu
2011 A* conf
Getting Rid of Store-Buffers in TSO Analysis.
CAV
Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato
2011 B conf
On Sequentializing Concurrent Programs.
SAS
Ahmed Bouajjani, Michael Emmi, Gennaro Parlato
2011 A* conf
The tree width of auxiliary storage.
POPL
P. Madhusudan, Gennaro Parlato
2010 A* conf
Model-Checking Parameterized Concurrent Programs Using Linear Interfaces.
CAV
Salvatore La Torre, P. Madhusudan, Gennaro Parlato
2010 B conf
The Language Theory of Bounded Context-Switching.
LATIN
Salvatore La Torre, Parthasarathy Madhusudan, Gennaro Parlato
2009 A* conf
Analyzing recursive programs using a fixed-point calculus.
PLDI
Salvatore La Torre, Parthasarathy Madhusudan, Gennaro Parlato
2009 J jnl
Fast payment schemes for truthful mechanisms with verification.
Theor. Comput. Sci.
Alessandro Ferrante, Gennaro Parlato, Francesco Sorrentino, Carmine Ventre
2009 A* conf
Reducing Context-Bounded Concurrent Reachability to Sequential Reachability.
CAV
Salvatore La Torre, P. Madhusudan, Gennaro Parlato
2008 B conf
An Infinite Automaton Characterization of Double Exponential Time.
CSL
Salvatore La Torre, P. Madhusudan, Gennaro Parlato
2008 A conf
Context-Bounded Analysis of Concurrent Queue Systems.
TACAS
Salvatore La Torre, P. Madhusudan, Gennaro Parlato
2008 J jnl
Verification of scope-dependent hierarchical state machines.
Inf. Comput.
Salvatore La Torre, Margherita Napoli, Mimmo Parente, Gennaro Parlato
2007 A* conf
A Robust Class of Context-Sensitive Languages.
LICS
Salvatore La Torre, Parthasarathy Madhusudan, Gennaro Parlato
2007 A* conf
On the Complexity of LtlModel-Checking of Recursive State Machines.
ICALP
Salvatore La Torre, Gennaro Parlato
2007 C conf
Verification of Succinct Hierarchical State Machines.
LATA
Salvatore La Torre, Margherita Napoli, Mimmo Parente, Gennaro Parlato
2005 J jnl
A linear time algorithm for the minimum Weighted Feedback Vertex Set on diamonds.
Inf. Process. Lett.
Francesco Carrabs, Raffaele Cerulli, Monica Gentili, Gennaro Parlato
2005 B conf
Improvements for Truthful Mechanisms with Verifiable One-Parameter Selfish Agents.
WAOA
Alessandro Ferrante, Gennaro Parlato, Francesco Sorrentino, Carmine Ventre
2004 C conf
Minimum Weighted Feedback Vertex Set on Diamonds.
CTW
Francesco Carrabs, Raffaele Cerulli, Monica Gentili, Gennaro Parlato
2004 J jnl
Minimum Weighted Feedback Vertex Set on Diamonds.
Electron. Notes Discret. Math.
Francesco Carrabs, Raffaele Cerulli, Monica Gentili, Gennaro Parlato
2003 A* conf
Hierarchical and Recursive State Machines with Context-Dependent Properties.
ICALP
Salvatore La Torre, Margherita Napoli, Mimmo Parente, Gennaro Parlato