| 2026 | ICGT | LR-Based Parsing of Hypergraph Languages: A Positional Grammar Approach. | Gennaro Costagliola, Mattia De Rosa, Salvatore La Torre |
| 2026 | TACAS | Iekk: A SAT-Based Bounded-Round Verifier for Multi-Threaded Programs (Competition Contribution). | Paolo Di Biase, Bernd Fischer, Salvatore La Torre, Peter Schrammel, Gennaro Parlato |
| 2023 | EUMAS | Verifying Programs by Bounded Tree-Width Behavior Graphs. | Omar Inverso, Salvatore La Torre, Gennaro Parlato, Ermenegildo Tomasco |
| 2020 | TIME | Complexity of Qualitative Timeline-Based Planning. | Dario Della Monica, Nicola Gigante, Salvatore La Torre, Angelo Montanari |
| 2017 | SEFM | Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models. | Ermenegildo Tomasco, Truc Lam Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2017 | TACAS | Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation - (Competition Contribution). | Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2016 | ATVA | Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs. | Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2016 | FMCAD | Lazy sequentialization for TSO and PSO via shared memory abstractions. | Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2016 | TACAS | MU-CSeq 0.4: Individual Memory Location Unwindings - (Competition Contribution). | Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2016 | VMCAI | A General Modular Synthesis Problem for Pushdown Systems. | Ilaria De Crescenzo, Salvatore La Torre |
| 2015 | CONCUR | Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable. | Salvatore La Torre, Anca Muscholl, Igor Walukiewicz |
| 2015 | TACAS | Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches - (Competition Contribution). | Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2015 | TACAS | MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings - (Competition Contribution). | Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2015 | TACAS | Verifying Concurrent Programs by Memory Unwinding. | Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2014 | CAV | Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. | Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2014 | DLT | Scope-Bounded Pushdown Languages. | Salvatore La Torre, Margherita Napoli, Gennaro Parlato |
| 2014 | MFCS | A Unifying Approach for Multistack Pushdown Automata. | Salvatore La Torre, Margherita Napoli, Gennaro Parlato |
| 2014 | TACAS | Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution). | Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2014 | TACAS | MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution). | Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2011 | CONCUR | Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations. | Salvatore La Torre, Margherita Napoli |
| 2010 | CAV | Model-Checking Parameterized Concurrent Programs Using Linear Interfaces. | Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2010 | LATA | Parametric Metric Interval Temporal Logic. | Barbara Di Giampaolo, Salvatore La Torre, Margherita Napoli |
| 2010 | LATIN | The Language Theory of Bounded Context-Switching. | Salvatore La Torre, Parthasarathy Madhusudan, Gennaro Parlato |
| 2009 | CAV | Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. | Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2009 | PLDI | Analyzing recursive programs using a fixed-point calculus. | Salvatore La Torre, Parthasarathy Madhusudan, Gennaro Parlato |
| 2008 | CSL | An Infinite Automaton Characterization of Double Exponential Time. | Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2008 | TACAS | Context-Bounded Analysis of Concurrent Queue Systems. | Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2007 | ICALP | Decision Problems for Lower/Upper Bound Parametric Timed Automata. | Laura Bozzelli, Salvatore La Torre |
| 2007 | ICALP | On the Complexity of LtlModel-Checking of Recursive State Machines. | Salvatore La Torre, Gennaro Parlato |
| 2007 | LATA | Verification of Succinct Hierarchical State Machines. | Salvatore La Torre, Margherita Napoli, Mimmo Parente, Gennaro Parlato |
| 2007 | LICS | A Robust Class of Context-Sensitive Languages. | Salvatore La Torre, Parthasarathy Madhusudan, Gennaro Parlato |
| 2006 | ATVA | On the Membership Problem for Visibly Pushdown Languages. | Salvatore La Torre, Margherita Napoli, Mimmo Parente |
| 2006 | VMCAI | Verification of Well-Formed Communicating Recursive State Machines. | Laura Bozzelli, Salvatore La Torre, Adriano Peron |
| 2004 | DLT | Optimal Time and Communication Solutions of Firing Squad Synchronization Problems on Square Arrays, Toruses and Rings. | Jozef Gruska, Salvatore La Torre, Mimmo Parente |
| 2004 | ICTAC | Reasoning About Co-Bchi Tree Automata. | Salvatore La Torre, Aniello Murano |
| 2003 | CAV | Modular Strategies for Infinite Games on Recursive Graphs. | Rajeev Alur, Salvatore La Torre, P. Madhusudan |
| 2003 | CONCUR | Playing Games with Boxes and Diamonds. | Rajeev Alur, Salvatore La Torre, P. Madhusudan |
| 2003 | ICALP | Hierarchical and Recursive State Machines with Context-Dependent Properties. | Salvatore La Torre, Margherita Napoli, Mimmo Parente, Gennaro Parlato |
| 2003 | TACAS | Modular Strategies for Recursive Game Graphs. | Rajeev Alur, Salvatore La Torre, P. Madhusudan |
| 2002 | LICS | Dense Real-Time Games. | Marco Faella, Salvatore La Torre, Aniello Murano |
| 2002 | VMCAI | Automata-Theoretic Decision of Timed Games. | Marco Faella, Salvatore La Torre, Aniello Murano |
| 2002 | VMCAI | Weak Muller Acceptance Conditions for Tree Automata. | Salvatore La Torre, Aniello Murano, Margherita Napoli |
| 2001 | LICS | Deterministic Generators and Games for LTL Fragments. | Rajeev Alur, Salvatore La Torre |
| 2001 | MCU | Firing Squad Synchronization Problem on Bidimensional Cellular Automata with Communication Constraints. | Salvatore La Torre, Margherita Napoli, Mimmo Parente |
| 1999 | ICALP | Parametric Temporal Logic for "Model Measuring". | Rajeev Alur, Kousha Etessami, Salvatore La Torre, Doron A. Peled |
| 1998 | MFCS | Representing Hyper-Graphs by Regular Languages. | Salvatore La Torre, Margherita Napoli |
| 1997 | FCT | Synchronization of 1-Way Connected Processors. | Salvatore La Torre, Margherita Napoli, Mimmo Parente |