An Object-Oriented Logic Language for Modular System Specification. - Angelo Morzenti; Pierluigi San Pietro (ECOOP, 1991)

Dealing with different time scales in formal specifications. - Edoardo Corsetti; Ernani Crivelli; Dino Mandrioli; Angelo Montanari; Angelo Morzenti; Pierluigi San Pietro; Elena Ratto (IWSSD, 1991)

Testing by Executing Logic Specifications. - Miguel Felder; Pierluigi San Pietro (NATO ASI RTC, 1992)

Finite Time Semantics for Executable Logic Specifications. - Miguel Felder; Pierluigi San Pietro (NATO ASI RTC, 1992)

Reuse of Object-Oriented Requirements Specifications. - Silvana Castano; Valeria De Antonellis; Pierluigi San Pietro (ER, 1993)

Embedding Time Granularity in a Logical Specification Language for Synchronous Real-Time Systems. - Emanuele Ciapessoni; Edoardo Corsetti; Angelo Montanari; Pierluigi San Pietro (Sci. Comput. Program., 1993)

Object-Oriented Logical Specification of Time-Critical Systems. - Angelo Morzenti; Pierluigi San Pietro (ACM Trans. Softw. Eng. Methodol., 1994)

Generating Functional Test Cases in-the-large for Time-critical Systems from Logic-based Specifications. - Sandro Morasca; Angelo Morzenti; Pierluigi San Pietro (ISSTA, 1996)

A Polynomial-Time Parsing Algorithm for K-Depth Languages. - Alessandra Cherubini; Pierluigi San Pietro (J. Comput. Syst. Sci., 1996)

A Finite-Domain Semantics for Testing Temporal Logic Specifications. - Alberto Coen-Porisini; Matteo Pradella; Pierluigi San Pietro (FTRTFT, 1998)

A Tool for Automated System Analysis based on Modular Specifications. - Angelo Morzenti; Pierluigi San Pietro; Sandro Morasca (ASE, 1998)

A Case Study on Applying a Tool for Automated System Analysis Based on Modular Specifications Written in TRIO. - Sandro Morasca; Angelo Morzenti; Pierluigi San Pietro (Autom. Softw. Eng., 2000)

Associative definition of programming languages. - Stefano Crespi-Reghizzi; Matteo Pradella; Pierluigi San Pietro (Comput. Lang., 2000)

Tree Adjoining Languages and Multipushdown Languages. - Alessandra Cherubini; Pierluigi San Pietro (Theory Comput. Syst., 2000)

Generation of Execution Sequences for Modular Time Critical Systems. - Pierluigi San Pietro; Angelo Morzenti; Sandro Morasca (IEEE Trans. Software Eng., 2000)

Alias Analysis by Means of a Model Checker. - Vincenzo Martena; Pierluigi San Pietro (CC, 2001)

Liveness Verification of Reversal-Bounded Multicounter Machines with a Free Counter. - Zhe Dang; Oscar H. Ibarra; Pierluigi San Pietro (FSTTCS, 2001)

Some Structural Properties of Associative Language Descriptions. - Alessandra Cherubini; Stefano Crespi-Reghizzi; Pierluigi San Pietro (ICTCS, 2001)

On Presburger Liveness of Discrete Timed Automata. - Zhe Dang; Pierluigi San Pietro; Richard A. Kemmerer (STACS, 2001)

Software procurement and methods for specification and validation in the railway transportation industry. - Umberto Foschi; Mauro Giuliani; Angelo Morzenti; Matteo Pradella; Pierluigi San Pietro (SMC, 2002)

Associative language descriptions. - Alessandra Cherubini; Stefano Crespi-Reghizzi; Pierluigi San Pietro (Theor. Comput. Sci., 2002)

Dense Counter Machines and Verification Problems. - Gaoyan Xie; Zhe Dang; Oscar H. Ibarra; Pierluigi San Pietro (CAV, 2003)

Automatic Verification of Multi-queue Discrete Timed Automata. - Pierluigi San Pietro; Zhe Dang (COCOON, 2003)

Model-Checking TRIO Specifications in SPIN. - Angelo Morzenti; Matteo Pradella; Pierluigi San Pietro; Paola Spoletini (FME, 2003)

Presburger liveness verification of discrete timed automata. - Zhe Dang; Pierluigi San Pietro; Richard A. Kemmerer (Theor. Comput. Sci., 2003)

Verification in loosely synchronous queue-connected discrete timed automata. - Oscar H. Ibarra; Zhe Dang; Pierluigi San Pietro (Theor. Comput. Sci., 2003)

Real-Counter Automata and Their Decision Problems. - Zhe Dang; Oscar H. Ibarra; Pierluigi San Pietro; Gaoyan Xie (FSTTCS, 2004)

Model checking-aided design of secure distributed systems. - Mario Verdicchio; Pierluigi San Pietro (IASTED Conf. on Software Engineering, 2004)

Experiences with a Formal Method for Design and Automatic Checking of User Interfaces. - Alessandro Campi; Eliseo Martinez; Pierluigi San Pietro (MBUI, 2004)

A scalable formal method for design and automatic checking of user interfaces. - Jean Berstel; Stefano Crespi-Reghizzi; Gilles Roussel 001; Pierluigi San Pietro (ACM Trans. Softw. Eng. Methodol., 2005)

Picture languages: Tiling systems versus tile rewriting grammars. - Alessandra Cherubini; Stefano Crespi-Reghizzi; Matteo Pradella; Pierluigi San Pietro (Theor. Comput. Sci., 2006)

Model Checking Temporal Metric Specifications with Trio2Promela. - Domenico Bianculli; Paola Spoletini; Angelo Morzenti; Matteo Pradella; Pierluigi San Pietro (FSEN, 2007)

Trio2Promela: A Model Checker for Temporal Metric Specifications. - Domenico Bianculli; Angelo Morzenti; Matteo Pradella; Pierluigi San Pietro; Paola Spoletini (ICSE Companion, 2007)

Extracting Coarse-Grained Parallelism in Program Loops with the Slicing Framework. - Anna Beletska; Wlodzimierz Bielecki; Pierluigi San Pietro (ISPDC, 2007)

The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties. - Matteo Pradella; Angelo Morzenti; Pierluigi San Pietro (ESEC/SIGSOFT FSE, 2007)

Regular Languages and Associative Language Descriptions. - Marcella Anselmo; Alessandra Cherubini; Pierluigi San Pietro (Discret. Math. Theor. Comput. Sci., 2007)

Finding Synchronization-Free Parallelism Represented with Trees of Dependent Operations. - Wlodzimierz Bielecki; Anna Beletska; Marek Palkowski; Pierluigi San Pietro (ICA3PP, 2008)

Finding Synchronization-Free Slices of Operations in Arbitrarily Nested Loops. - Anna Beletska; Wlodzimierz Bielecki; Krzysztof Siedlecki; Pierluigi San Pietro (ICCSA (2), 2008)

Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time. - Matteo Pradella; Angelo Morzenti; Pierluigi San Pietro (ICTAC, 2008)

Refining Real-Time System Specifications through Bounded Model- and Satisfiability-Checking. - Matteo Pradella; Angelo Morzenti; Pierluigi San Pietro (ASE, 2008)

Consensual Definition of Languages by Regular Sets. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (LATA, 2008)

A Metric Encoding for Bounded Model Checking. - Matteo Pradella; Angelo Morzenti; Pierluigi San Pietro (FM, 2009)

Languages defined by consensual computations. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (ICTCS, 2009)

A Metric Encoding for Bounded Model Checking (extended version) - Matteo Pradella; Angelo Morzenti; Pierluigi San Pietro (CoRR, 2009)

Bounded Reachability for Temporal Logic over Constraint Systems. - Marcello M. Bersani; Achille Frigeri; Angelo Morzenti; Matteo Pradella; Matteo Rossi 001; Pierluigi San Pietro (TIME, 2010)

Completeness of the Bounded Satisfiability Problem for Constraint LTL. - Marcello M. Bersani; Achille Frigeri; Matteo Rossi 001; Pierluigi San Pietro (RP, 2011)

Consensual languages and matching finite-state computations. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (RAIRO Theor. Informatics Appl., 2011)

The Tale of SOLOIST: A Specification Language for Service Compositions Interactions. - Domenico Bianculli; Carlo Ghezzi; Pierluigi San Pietro (FACS, 2012)

Strict Local Testability with Consensus Equals Regularity. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (CIAA, 2012)

From Regular to Strictly Locally Testable Languages. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (Int. J. Found. Comput. Sci., 2012)

Deciding Continuous-Time Metric Temporal Logic with Counting Modalities. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (RP, 2013)

Deterministic Counter Machines and Parallel Matching Computations. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (CIAA, 2013)

Deciding the Satisfiability of MITL Specifications. - Marcello Maria Bersani; Matteo Rossi 001; Pierluigi San Pietro (GandALF, 2013)

On the Satisfiability of Metric Temporal Logics over the Reals. - Marcello Maria Bersani; Matteo Rossi 001; Pierluigi San Pietro (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Strict Local Testability with Consensus Equals Regularity, and Other Properties. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (Int. J. Found. Comput. Sci., 2013)

Bounded satisfiability checking of metric temporal logic specifications. - Matteo Pradella; Angelo Morzenti; Pierluigi San Pietro (ACM Trans. Softw. Eng. Methodol., 2013)

SMT-Based Checking of SOLOIST over Sparse Traces. - Marcello Maria Bersani; Domenico Bianculli; Carlo Ghezzi; Srdan Krstic; Pierluigi San Pietro (FASE, 2014)

A Logical Characterization of Timed (non-)Regular Languages. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (MFCS (1), 2014)

Offline Trace Checking of Quantitative Properties of Service-Based Applications. - Domenico Bianculli; Carlo Ghezzi; Srdan Krstic; Pierluigi San Pietro (SOCA, 2014)

Commutative Languages and their Composition by Consensual Methods. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (AFL, 2014)

Constraint LTL satisfiability checking without automata. - Marcello M. Bersani; Achille Frigeri; Angelo Morzenti; Matteo Pradella; Matteo Rossi 001; Pierluigi San Pietro (J. Appl. Log., 2014)

Dense-choice Counter Machines revisited. - Florent Bouchy; Alain Finkel; Pierluigi San Pietro (Theor. Comput. Sci., 2014)

An SMT-based approach to satisfiability checking of MITL. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (Inf. Comput., 2015)

Efficient large-scale trace checking using mapreduce. - Marcello M. Bersani; Domenico Bianculli; Carlo Ghezzi; Srdan Krstic; Pierluigi San Pietro (ICSE, 2016)

The Missing Case in Chomsky-Schützenberger Theorem. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (LATA, 2016)

A tool for deciding the satisfiability of continuous-time metric temporal logic. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (Acta Informatica, 2016)

A logical characterization of timed regular languages. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (Theor. Comput. Sci., 2017)

Counter machines, Petri Nets, and consensual computation. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (Theor. Comput. Sci., 2017)

Deque Languages, Automata and Planar Graphs. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (DLT, 2018)

Non-erasing Chomsky-Sch{ü}tzenberger theorem with grammar-independent alphabet. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (CoRR, 2018)

A Flexible Approach for Checking Timed Automata on Continuous Time Semantics. - Claudio Menghi; Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (CoRR, 2018)

Regular Languages as Local Functions with Small Alphabets. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (CAI, 2019)

Deque Languages, Automata and Planar Graphs (text not included). - Stefano Crespi-Reghizzi; Pierluigi San Pietro (ICTCS, 2019)

Non-erasing Chomsky-Schützenberger theorem with grammar-independent alphabet. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (Inf. Comput., 2019)

Preface. - Aniello Murano; Patricia Bouyer; Pierluigi San Pietro; Andrea Orlandini (Inf. Comput., 2020)

On the initialization of clocks in timed formalisms. - Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (Theor. Comput. Sci., 2020)

Deque automata, languages, and planar graph representations. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (Theor. Comput. Sci., 2020)

Model Checking MITL Formulae on Timed Automata: A Logic-based Approach. - Claudio Menghi; Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (ACM Trans. Comput. Log., 2020)

Reducing Local Alphabet Size in Recognizable Picture Languages. - Stefano Crespi-Reghizzi; Antonio Restivo; Pierluigi San Pietro (DLT, 2021)

Improved Bounded Model Checking of Timed Automata. - Robert L. Smith; Marcello M. Bersani; Matteo Rossi 001; Pierluigi San Pietro (FormaliSE@ICSE, 2021)

Reducing the Local Alphabet Size in Tiling Systems for Picture Languages. - Stefano Crespi-Reghizzi; Antonio Restivo; Pierluigi San Pietro (ICTCS, 2021)

Homomorphic Characterization of Tree Languages Based on Comma-Free Encoding. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (LATA, 2021)

Reducing the local alphabet size in tiling systems by means of 2D comma-free codes. - Stefano Crespi-Reghizzi; Antonio Restivo; Pierluigi San Pietro (Theor. Comput. Sci., 2022)

Two-Dimensional Dyck Words (short paper) (text not included). - Stefano Crespi-Reghizzi; Antonio Restivo; Pierluigi San Pietro (ICTCS, 2023)

Two-dimensional Dyck words. - Stefano Crespi-Reghizzi; Antonio Restivo; Pierluigi San Pietro (CoRR, 2023)

Regular languages as images of local functions over small alphabets. - Stefano Crespi-Reghizzi; Pierluigi San Pietro (Inf. Comput., 2024)

From words to pictures: Row-column combinations and Chomsky-Schützenberger theorem. - Stefano Crespi-Reghizzi; Antonio Restivo; Pierluigi San Pietro (Theor. Comput. Sci., 2024)

Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation. - Andrea Manini; Matteo G. Rossi; Pierluigi San Pietro (TASE, 2025)

On Decidability Timed Automata with 2 Parametric Clocks. - Marcello M. Bersani; Matteo G. Rossi; Pierluigi San Pietro (CoRR, 2025)

Row-column combination of Dyck words. - Stefano Crespi-Reghizzi; Antonio Restivo; Pierluigi San Pietro (Acta Informatica, 2025)