Synchronization of One-way Connected Processors. - Salvatore La Torre; Margherita Napoli; Mimmo Parente (Complex Syst., 1996)

Parallel Word Substitution. - Salvatore La Torre; Margherita Napoli; Domenico Parente (Fundam. Informaticae, 1996)

Synchronization of 1-Way Connected Processors. - Salvatore La Torre; Margherita Napoli; Mimmo Parente (FCT, 1997)

Representing Hyper-Graphs by Regular Languages. - Salvatore La Torre; Margherita Napoli (MFCS, 1998)

Synchronization of a Line of Identical Processors at a Given Time. - Salvatore La Torre; Margherita Napoli; Domenico Parente (Fundam. Informaticae, 1998)

A Decidable Dense Branching-Time Temporal Logic. - Salvatore La Torre; Margherita Napoli (FSTTCS, 2000)

A compositional approach to synchronize two dimensional networks of processors. - Salvatore La Torre; Margherita Napoli; Mimmo Parente (RAIRO Theor. Informatics Appl., 2000)

Firing Squad Synchronization Problem on Bidimensional Cellular Automata with Communication Constraints. - Salvatore La Torre; Margherita Napoli; Mimmo Parente (MCU, 2001)

Timed tree automata with an application to temporal logic. - Salvatore La Torre; Margherita Napoli (Acta Informatica, 2001)

Automata-based Representations for Infinite Graphs. - Salvatore La Torre; Margherita Napoli (RAIRO Theor. Informatics Appl., 2001)

A Model of Finite Automata on Timed omega-Trees. - Salvatore La Torre; Margherita Napoli (CATS, 2001)

Parametric temporal logic for "model measuring". - Rajeev Alur; Kousha Etessami; Salvatore La Torre; Doron A. Peled (ACM Trans. Comput. Log., 2001)

Optimal-Reachability and Control for Acyclic Weighted Timed Automata. - Salvatore La Torre; Supratik Mukhopadhyay; Aniello Murano (IFIP TCS, 2002)

Dense Real-Time Games. - Marco Faella; Salvatore La Torre; Aniello Murano (LICS, 2002)

Modular Strategies for Infinite Games on Recursive Graphs. - Rajeev Alur; Salvatore La Torre; P. Madhusudan (CAV, 2003)

Playing Games with Boxes and Diamonds. - Rajeev Alur; Salvatore La Torre; P. Madhusudan (CONCUR, 2003)

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

Model-checking the Secure Release of a Time-locked Secret over a Network. - Salvatore La Torre; Aniello Murano; Mimmo Parente (MEFISTO, 2003)

Deterministic finite automata with recursive calls and DPDAs. - Jean H. Gallier; Salvatore La Torre; Supratik Mukhopadhyay (Inf. Process. Lett., 2003)

Finite automata on timed omega-trees. - Salvatore La Torre; Margherita Napoli (Theor. Comput. Sci., 2003)

Optimal Time and Communication Solutions of Firing Squad Synchronization Problems on Square Arrays, Toruses and Rings. - Jozef Gruska; Salvatore La Torre; Mimmo Parente (Developments in Language Theory, 2004)

Reasoning About Co-Büchi Tree Automata. - Salvatore La Torre; Aniello Murano (ICTAC, 2004)

Polyhedral Flows in Hybrid Automata. - Rajeev Alur; Sampath Kannan; Salvatore La Torre (Formal Methods Syst. Des., 2004)

Optimal paths in weighted timed automata. - Rajeev Alur; Salvatore La Torre; George J. Pappas (Theor. Comput. Sci., 2004)

Deterministic generators and games for Ltl fragments. - Rajeev Alur; Salvatore La Torre (ACM Trans. Comput. Log., 2004)

Perturbed Timed Automata. - Rajeev Alur; Salvatore La Torre; P. Madhusudan (HSCC, 2005)

Various Solutions to the Firing Squad Synchronization Problems - Jozef Gruska; Salvatore La Torre; Margherita Napoli; Mimmo Parente (CoRR, 2005)

Weak Muller acceptance conditions for tree automata. - Salvatore La Torre; Aniello Murano; Margherita Napoli (Theor. Comput. Sci., 2005)

On the Membership Problem for Visibly Pushdown Languages. - Salvatore La Torre; Margherita Napoli; Mimmo Parente (ATVA, 2006)

Different time solutions for the firing squad synchronization problem on basic grid networks. - Jozef Gruska; Salvatore La Torre; Margherita Napoli; Mimmo Parente (RAIRO Theor. Informatics Appl., 2006)

Modular strategies for recursive game graphs. - Rajeev Alur; Salvatore La Torre; P. Madhusudan (Theor. Comput. Sci., 2006)

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)

The word problem for visibly pushdown languages described by grammars. - Salvatore La Torre; Margherita Napoli; Mimmo Parente (Formal Methods Syst. Des., 2007)

The Firing Squad Synchronization Problem on Squares, Toruses and Rings. - Jozef Gruska; Salvatore La Torre; Mimmo Parente (Int. J. Found. Comput. Sci., 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)

Verification of well-formed communicating recursive state machines. - Laura Bozzelli; Salvatore La Torre; Adriano Peron (Theor. Comput. Sci., 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)

Decision problems for lower/upper bound parametric timed automata. - Laura Bozzelli; Salvatore La Torre (Formal Methods Syst. Des., 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)

Winning CaRet Games with Modular Strategies. - Ilaria De Crescenzo; Salvatore La Torre (CILC, 2011)

Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations. - Salvatore La Torre; Margherita Napoli (CONCUR, 2011)

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

A Temporal Logic for Multi-threaded Programs. - Salvatore La Torre; Margherita Napoli (IFIP TCS, 2012)

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

Modular Synthesis with Open Components. - Ilaria De Crescenzo; Salvatore La Torre (RP, 2013)

Games, Automata, Logic, and Formal Verification (GandALF 2011). - Giovanna D'Agostino; Salvatore La Torre (Theor. Comput. Sci., 2013)

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)

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)

Visibly Pushdown Modular Games. - Ilaria De Crescenzo; Salvatore La Torre; Yaron Velner (GandALF, 2014)

Automata-theoretic decision of timed games. - Marco Faella; Salvatore La Torre; Aniello Murano (Theor. Comput. Sci., 2014)

Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable. - Salvatore La Torre; Anca Muscholl; Igor Walukiewicz (CONCUR, 2015)

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)

Parametric metric interval temporal logic. - Barbara Di Giampaolo; Salvatore La Torre; Margherita Napoli (Theor. Comput. Sci., 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)

A General Modular Synthesis Problem for Pushdown Systems. - Ilaria De Crescenzo; Salvatore La Torre (VMCAI, 2016)

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

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)

Reachability in Concurrent Uninterpreted Programs. - Salvatore La Torre; Parthasarathy Madhusudan (FSTTCS, 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)

Complexity of Qualitative Timeline-Based Planning. - Dario Della Monica; Nicola Gigante; Salvatore La Torre; Angelo Montanari (TIME, 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)

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)

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

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

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