Nicoletta De Francesco

Francesco Mercaldo

Comput. Secur., 2020

2018

Design and simulation of the emergent behavior of small drones swarming for distributed target localization.

[BibT_eX]

[DOI]

Antonio L. Alfeo

Mario G. C. A. Cimino

Massimiliano Lega

J. Comput. Sci., 2018

Swarm coordination of mini-UAVs for target search using imperfect sensors.

[BibT_eX]

[DOI]

Antonio L. Alfeo

Mario G. C. A. Cimino

Alessandro Lazzeri

Massimiliano Lega

Intell. Decis. Technol., 2018

2016

Heuristic search for equivalence checking.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2016

2014

GreASE: A Tool for Efficient "Nonequivalence" Checking.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2014

2012

Efficient Genotype Elimination via Adaptive Allele Consolidation.

[BibT_eX]

[DOI]

IEEE ACM Trans. Comput. Biol. Bioinform., 2012

JCSI: A tool for checking secure information flow in Java Card applications.

[BibT_eX]

[DOI]

Marco Avvenuti

Paolo Masci

J. Syst. Softw., 2012

2010

Using abstract interpretation to add type checking for interfaces in Java bytecode verification.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2010

Partial model checking via abstract interpretation.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2010

Celer: an Efficient Program for Genotype Elimination

[BibT_eX]

[DOI]

Proceedings of the Proceedings First Workshop on Applications of Membrane computing, 2010

An Abstract Interpretation Approach for Enhancing the Java Bytecode Verifier.

[BibT_eX]

[DOI]

Comput. J., 2010

2008

Decomposing bytecode verification by abstract interpretation.

[BibT_eX]

[DOI]

Paolo Masci

ACM Trans. Program. Lang. Syst., 2008

2007

A user-friendly interface to specify temporal properties of concurrent systems.

[BibT_eX]

[DOI]

Inf. Sci., 2007

Instruction-level security typing by abstract interpretation.

[BibT_eX]

[DOI]

Int. J. Inf. Sec., 2007

Instruction-level security analysis for information flow in stack-based assembly languages.

[BibT_eX]

[DOI]

Inf. Comput., 2007

2005

Reduced Models for Efficient CCS Verification.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2005

Abstract Interpretation to Check Secure Information Flow in Programs with Input-Output Security Annotations.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects in Security and Trust, Third International Workshop, 2005

2004

Checking secure information flow in Java bytecode by code transformation and standard bytecode verification.

[BibT_eX]

[DOI]

Softw. Pract. Exp., 2004

Concrete and Abstract Semantics to Check Secure Information Flow in Concurrent Programs.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2004

Analyzing Information Flow Properties in Assembly Code by Abstract Interpretation.

[BibT_eX]

[DOI]

Comput. J., 2004

2003

Checking security properties by model checking.

[BibT_eX]

[DOI]

Softw. Test. Verification Reliab., 2003

Java bytecode verification for secure information flow.

[BibT_eX]

[DOI]

Marco Avvenuti

ACM SIGPLAN Notices, 2003

Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2003

Authenticity in a Reliable Protocol for Mobile Computing.

[BibT_eX]

[DOI]

Marinella Petrocchi

Proceedings of the 2003 ACM Symposium on Applied Computing (SAC), 2003

Efficient Bytecode Verification Using Immediate Postdominators in Control Flow Graphs: Extended Abstract.

[BibT_eX]

[DOI]

Proceedings of the On The Move to Meaningful Internet Systems 2003: OTM 2003 Workshops, 2003

2002

Syntactic reductions for efficient deadlock analysis.

[BibT_eX]

[DOI]

Softw. Test. Verification Reliab., 2002

A tool supporting efficient model checking of concurrent specifications.

[BibT_eX]

[DOI]

Microprocess. Microsystems, 2002

An abstract semantics tool for secure information flow of stack-based assembly programs.

[BibT_eX]

[DOI]

Microprocess. Microsystems, 2002

Abstract interpretation of operational semantics for secure information flow.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2002

A Formula-Driven Modular Attack on State Explosion.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2002

A Notion of Non-Interference for Timed Automata.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2002

Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2002

Fixing the Java bytecode verifier by a suitable type domain.

[BibT_eX]

[DOI]

Proceedings of the 14th international conference on Software engineering and knowledge engineering, 2002

Checking security of Java bytecode by abstract interpretation.

[BibT_eX]

[DOI]

Proceedings of the 2002 ACM Symposium on Applied Computing (SAC), 2002

Using Standard Verifier to Check Secure Information Flow in Java Bytecode.

[BibT_eX]

[DOI]

Proceedings of the 26th International Computer Software and Applications Conference (COMPSAC 2002), 2002

2001

An approach to system design based on P/T net simulation.

[BibT_eX]

[DOI]

Inf. Softw. Technol., 2001

Timed Automata with non-Instantaneous Actions.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2001

Finite Approximations for Model Checking Non-finite-state Processes.

[BibT_eX]

[DOI]

Alessandro Fantechi

Stefania Gnesi

Comput. J., 2001

Efficient Verification of a Multicast Protocol for Mobile Computing.

[BibT_eX]

[DOI]

Giuseppe Anastasi

Alberto Bartoli

Comput. J., 2001

Modelling Free Flight with Collision Avoidance.

[BibT_eX]

[DOI]

Mieke Massink

Proceedings of the 7th International Conference on Engineering of Complex Computer Systems (ICECCS 2001), 2001

2000

Logic Based Abstractions of Real-Time Systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2000

1999

LORETO: A Tool for Reducing State Explosion in Verification of LOTOS Programs.

[BibT_eX]

[DOI]

Softw. Pract. Exp., 1999

Selective Mu-Calculus and Formula-Based Equivalence of Transition Systems.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1999

Abstract Interpretation of Trace Semantics for Concurrent Calculi.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1999

Formula Based Abstractions of Transition Systems for Real-Time Model Checking.

[BibT_eX]

[DOI]

Proceedings of the FM'99 - Formal Methods, 1999

1998

State Space Reduction by Non-Standard Semantics for Deadlock Analysis.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1998

Towards a Logical Semantics for Pure Prolog.

[BibT_eX]

[DOI]

Paolo Mancarella

Sci. Comput. Program., 1998

A Transformation System for Concurrent Processes.

[BibT_eX]

[DOI]

Acta Informatica, 1998

1997

Algebraic Computational Models of OR-Parallel Execution of Prolog.

[BibT_eX]

[DOI]

Acta Informatica, 1997

Selective µ-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems.

[BibT_eX]

Proceedings of the Formal Description Techniques and Protocol Specification, 1997

1996

Unfold/Fold Transformations of Concurrent Processes.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages: Implementations, 1996

A Non-Standard Semantics for Generating Reduced Transition Systems.

[BibT_eX]

[DOI]

Proceedings of the Analysis and Verification of Multiple-Agent Languages, 1996

1995

A Petri Nets Semantics for Data Flow Networks.

[BibT_eX]

[DOI]

Acta Informatica, 1995

Model Checking of Non-Finite State Processes by Finite Approximations.

[BibT_eX]

[DOI]

Alessandro Fantechi

Stefania Gnesi

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

Modeling OR-Parallel Execution of Prolog using CHOCS.

[BibT_eX]

Proceedings of the Logic Programming, 1995

1994

Concurrent Behavior: A Construct to Specify the External Behavior of Objects in Object Databases.

[BibT_eX]

[DOI]

Distributed Parallel Databases, 1994

Proving Finiteness of CCS Processes by Non-Standard Semantics.

[BibT_eX]

[DOI]

Acta Informatica, 1994

Modelling Concurrent Accesses to Shared Data via Petri Nets.

[BibT_eX]

Ugo Montanari

Gioia Ristori

Proceedings of the Programming Concepts, 1994

1993

Axiomatizing CCS, Nets and Processes.

[BibT_eX]

[DOI]

Ugo Montanari

Daniel Yankelevich

Sci. Comput. Program., 1993

1992

Specification of Concurrency Control in Persistent Programming Languages.

[BibT_eX]

Luigi V. Mancini

A. Pereira Paz

Proceedings of the Persistent Object Systems, 1992

1991

Towards innovative software engineering environments.

[BibT_eX]

[DOI]

Vincenzo Ambriola

Paolo Ciancarini

Andrea Corradini

J. Syst. Softw., 1991

A Semantic Driven Method to Check the Finiteness of CCS Processes.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 3rd International Workshop, 1991

1989

Shared Abstract Data Types: An Algebraic Methodology for Their Specification.

[BibT_eX]

[DOI]

Andrea Bondavalli

Diego Latella

Proceedings of the MFDBS 89, 1989

1988

Description of a Tool for Specifying and Prototyping Concurrent Programs.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1988

1986

Development of a Debugger for a Concurrent Language.

[BibT_eX]

[DOI]

Fabrizio Baiardi

IEEE Trans. Software Eng., 1986

1985

An Interactive Debugger for a Concurrent Language.

[BibT_eX]

[DOI]

Diego Latella

Proceedings of the Proceedings, 1985

1983

Development of a debugger for a concurrent language.

[BibT_eX]

[DOI]

Fabrizio Baiardi

E. Matteoli

S. Stefanini