Salvatore La Torre

Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, 2021

2020

Reachability of scope-bounded multistack pushdown systems.

[BibT_eX]

[DOI]

Inf. Comput., 2020

Complexity of Qualitative Timeline-Based Planning.

[BibT_eX]

[DOI]

Proceedings of the 27th International Symposium on Temporal Representation and Reasoning, 2020

A Fixed-point Model-checker for BDI Logics over Finite-state Worlds.

[BibT_eX]

[DOI]

Proceedings of the 2nd Workshop on Artificial Intelligence and Formal Verification, 2020

On the Model-Checking of Branching-time Temporal Logic with BDI Modalities.

[BibT_eX]

[DOI]

Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, 2020

2019

VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-threaded Programs with Lazy-CSeq.

[BibT_eX]

[DOI]

Bernd Fischer

Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, 2019

Reachability in Concurrent Uninterpreted Programs.

[BibT_eX]

[DOI]

Proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2019

Model Checking BDI Logics over Finite-state Worlds.

[BibT_eX]

[DOI]

Proceedings of the 1st Workshop on Artificial Intelligence and Formal Verification, 2019

2017

Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 15th International Conference, 2017

Concurrent Program Verification with Lazy Sequentialization and Interval Analysis.

[BibT_eX]

[DOI]

Proceedings of the Networked Systems - 5th International Conference, 2017

Parallel bug-finding in concurrent programs via reduced interleaving instances.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

2016

Scope-Bounded Pushdown Languages.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2016

A General Modular Synthesis Problem for Pushdown Systems.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

MU-CSeq 0.4: Individual Memory Location Unwindings - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Lazy sequentialization for TSO and PSO via shared memory abstractions.

[BibT_eX]

[DOI]

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2016

2015

Parametric metric interval temporal logic.

[BibT_eX]

[DOI]

Barbara Di Giampaolo

Theor. Comput. Sci., 2015

Verifying Concurrent Programs by Memory Unwinding.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering, 2015

Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable.

[BibT_eX]

[DOI]

Anca Muscholl

Igor Walukiewicz

Proceedings of the 26th International Conference on Concurrency Theory, 2015

2014

Automata-theoretic decision of timed games.

[BibT_eX]

[DOI]

Marco Faella

Theor. Comput. Sci., 2014

Visibly Pushdown Modular Games.

[BibT_eX]

[DOI]

Yaron Velner

Proceedings of the Proceedings Fifth International Symposium on Games, 2014

MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

A Unifying Approach for Multistack Pushdown Automata.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2014, 2014

Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Games, Automata, Logic, and Formal Verification (GandALF 2011).

[BibT_eX]

[DOI]

Giovanna D'Agostino

Theor. Comput. Sci., 2013

Modular Synthesis with Open Components.

[BibT_eX]

[DOI]

Proceedings of the Reachability Problems - 7th International Workshop, 2013

2012

Sequentializing Parameterized Programs

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fourth Workshop on Foundations of Interface Technologies, 2012

A Temporal Logic for Multi-threaded Programs.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 2012

Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width.

[BibT_eX]

[DOI]

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2012

2011

Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Winning CaRet Games with Modular Strategies.

[BibT_eX]

[DOI]

Proceedings of the 26th Italian Conference on Computational Logic, Pescara, Italy, August 31, 2011

2010

The Language Theory of Bounded Context-Switching.

[BibT_eX]

[DOI]

Proceedings of the LATIN 2010: Theoretical Informatics, 2010

Model-Checking Parameterized Concurrent Programs Using Linear Interfaces.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

Decision problems for lower/upper bound parametric timed automata.

[BibT_eX]

[DOI]

Laura Bozzelli

Formal Methods Syst. Des., 2009

Analyzing recursive programs using a fixed-point calculus.

[BibT_eX]

[DOI]

Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

Reducing Context-Bounded Concurrent Reachability to Sequential Reachability.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Verification of well-formed communicating recursive state machines.

[BibT_eX]

[DOI]

Laura Bozzelli

Adriano Peron

Theor. Comput. Sci., 2008

Verification of scope-dependent hierarchical state machines.

[BibT_eX]

[DOI]

Inf. Comput., 2008

Context-Bounded Analysis of Concurrent Queue Systems.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

An Infinite Automaton Characterization of Double Exponential Time.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

2007

The Firing Squad Synchronization Problem on Squares, Toruses and Rings.

[BibT_eX]

[DOI]

Jozef Gruska

Int. J. Found. Comput. Sci., 2007

The word problem for visibly pushdown languages described by grammars.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2007

A Robust Class of Context-Sensitive Languages.

[BibT_eX]

[DOI]

Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

Verification of Succinct Hierarchical State Machines.

[BibT_eX]

Proceedings of the LATA 2007. Proceedings of the 1st International Conference on Language and Automata Theory and Applications., 2007

On the Complexity of LtlModel-Checking of Recursive State Machines.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 34th International Colloquium, 2007

2006

Modular strategies for recursive game graphs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2006

Different time solutions for the firing squad synchronization problem on basic grid networks.

[BibT_eX]

[DOI]

RAIRO Theor. Informatics Appl., 2006

On the Membership Problem for Visibly Pushdown Languages.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2006

2005

Weak Muller acceptance conditions for tree automata.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

Various Solutions to the Firing Squad Synchronization Problems

[BibT_eX]

[DOI]

CoRR, 2005

Perturbed Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 8th International Workshop, 2005

2004

Deterministic generators and games for Ltl fragments.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2004

Optimal paths in weighted timed automata.

[BibT_eX]

[DOI]

George J. Pappas

Theor. Comput. Sci., 2004

Polyhedral Flows in Hybrid Automata.

[BibT_eX]

[DOI]

Sampath Kannan

Formal Methods Syst. Des., 2004

Reasoning About Co-Büchi Tree Automata.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2004

Optimal Time and Communication Solutions of Firing Squad Synchronization Problems on Square Arrays, Toruses and Rings.

[BibT_eX]

[DOI]

Jozef Gruska

Proceedings of the Developments in Language Theory, 2004

2003

Finite automata on timed omega-trees.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2003

Deterministic finite automata with recursive calls and DPDAs.

[BibT_eX]

[DOI]

Jean H. Gallier

Supratik Mukhopadhyay

Inf. Process. Lett., 2003

Model-checking the Secure Release of a Time-locked Secret over a Network.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Security and Time: Proceedings of the MEFISTO Project 2003, 2003

Hierarchical and Recursive State Machines with Context-Dependent Properties.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

Playing Games with Boxes and Diamonds.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2003, 2003

Modular Strategies for Infinite Games on Recursive Graphs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002

Dense Real-Time Games.

[BibT_eX]

[DOI]

Marco Faella

Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Optimal-Reachability and Control for Acyclic Weighted Timed Automata.

[BibT_eX]

[DOI]

Supratik Mukhopadhyay

Proceedings of the Foundations of Information Technology in the Era of Networking and Mobile Computing, 2002

2001

Parametric temporal logic for "model measuring".

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2001

A Model of Finite Automata on Timed omega-Trees.

[BibT_eX]

[DOI]

Proceedings of the Computing: The Australasian Theory Symposium, 2001

Automata-based Representations for Infinite Graphs.

[BibT_eX]

[DOI]

RAIRO Theor. Informatics Appl., 2001

Timed tree automata with an application to temporal logic.

[BibT_eX]

[DOI]

Acta Informatica, 2001

Firing Squad Synchronization Problem on Bidimensional Cellular Automata with Communication Constraints.

[BibT_eX]

[DOI]

Proceedings of the Machines, 2001

2000

A compositional approach to synchronize two dimensional networks of processors.

[BibT_eX]

[DOI]

RAIRO Theor. Informatics Appl., 2000

A Decidable Dense Branching-Time Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 2000

1998

Synchronization of a Line of Identical Processors at a Given Time.

[BibT_eX]

[DOI]

Domenico Parente

Fundam. Informaticae, 1998

Representing Hyper-Graphs by Regular Languages.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 1998, 1998

1997

Synchronization of 1-Way Connected Processors.

[BibT_eX]

[DOI]

Proceedings of the Fundamentals of Computation Theory, 11th International Symposium, 1997

1996

Parallel Word Substitution.

[BibT_eX]

[DOI]

Domenico Parente

Fundam. Informaticae, 1996

Synchronization of One-way Connected Processors.

[BibT_eX]

[DOI]