Nicoletta De Francesco

According to our database1, Nicoletta De Francesco
  • authored at least 63 papers between 1983 and 2016.
  • has a "Dijkstra number"2 of four.



In proceedings 
PhD thesis 




Heuristic search for equivalence checking.
Software and System Modeling, 2016

GreASE: A Tool for Efficient "Nonequivalence" Checking.
ACM Trans. Softw. Eng. Methodol., 2014

Efficient Genotype Elimination via Adaptive Allele Consolidation.
IEEE/ACM Trans. Comput. Biology Bioinform., 2012

JCSI: A tool for checking secure information flow in Java Card applications.
Journal of Systems and Software, 2012

Using abstract interpretation to add type checking for interfaces in Java bytecode verification.
Theor. Comput. Sci., 2010

Partial model checking via abstract interpretation.
Inf. Process. Lett., 2010

Celer: an Efficient Program for Genotype Elimination
Proceedings of the Proceedings First Workshop on Applications of Membrane computing, 2010

An Abstract Interpretation Approach for Enhancing the Java Bytecode Verifier.
Comput. J., 2010

Decomposing bytecode verification by abstract interpretation.
ACM Trans. Program. Lang. Syst., 2008

A user-friendly interface to specify temporal properties of concurrent systems.
Inf. Sci., 2007

Instruction-level security typing by abstract interpretation.
Int. J. Inf. Sec., 2007

Instruction-level security analysis for information flow in stack-based assembly languages.
Inf. Comput., 2007

Reduced Models for Efficient CCS Verification.
Formal Methods in System Design, 2005

Abstract Interpretation to Check Secure Information Flow in Programs with Input-Output Security Annotations.
Proceedings of the Formal Aspects in Security and Trust, Third International Workshop, 2005

Checking secure information flow in Java bytecode by code transformation and standard bytecode verification.
Softw., Pract. Exper., 2004

Concrete and Abstract Semantics to Check Secure Information Flow in Concurrent Programs.
Fundam. Inform., 2004

Analyzing Information Flow Properties in Assembly Code by Abstract Interpretation.
Comput. J., 2004

Checking security properties by model checking.
Softw. Test., Verif. Reliab., 2003

Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems.
Fundam. Inform., 2003

Authenticity in a Reliable Protocol for Mobile Computing.
Proceedings of the 2003 ACM Symposium on Applied Computing (SAC), 2003

Efficient Bytecode Verification Using Immediate Postdominators in Control Flow Graphs: Extended Abstract.
Proceedings of the On The Move to Meaningful Internet Systems 2003: OTM 2003 Workshops, 2003

Syntactic reductions for efficient deadlock analysis.
Softw. Test., Verif. Reliab., 2002

A tool supporting efficient model checking of concurrent specifications.
Microprocessors and Microsystems, 2002

An abstract semantics tool for secure information flow of stack-based assembly programs.
Microprocessors and Microsystems, 2002

Abstract interpretation of operational semantics for secure information flow.
Inf. Process. Lett., 2002

A Formula-Driven Modular Attack on State Explosion.
Int. J. Found. Comput. Sci., 2002

A Notion of Non-Interference for Timed Automata.
Fundam. Inform., 2002

Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode.
Proceedings of the Verification, 2002

Fixing the Java bytecode verifier by a suitable type domain.
Proceedings of the 14th international conference on Software engineering and knowledge engineering, 2002

Checking security of Java bytecode by abstract interpretation.
Proceedings of the 2002 ACM Symposium on Applied Computing (SAC), 2002

Using Standard Verifier to Check Secure Information Flow in Java Bytecode.
Proceedings of the 26th International Computer Software and Applications Conference (COMPSAC 2002), 2002

An approach to system design based on P/T net simulation.
Information & Software Technology, 2001

Timed Automata with non-Instantaneous Actions.
Fundam. Inform., 2001

Finite Approximations for Model Checking Non-finite-state Processes.
Comput. J., 2001

Efficient Verification of a Multicast Protocol for Mobile Computing.
Comput. J., 2001

Modelling Free Flight with Collision Avoidance.
Proceedings of the 7th International Conference on Engineering of Complex Computer Systems (ICECCS 2001), 2001

Logic Based Abstractions of Real-Time Systems.
Formal Methods in System Design, 2000

LORETO: A Tool for Reducing State Explosion in Verification of LOTOS Programs.
Softw., Pract. Exper., 1999

Selective Mu-Calculus and Formula-Based Equivalence of Transition Systems.
J. Comput. Syst. Sci., 1999

Abstract Interpretation of Trace Semantics for Concurrent Calculi.
Inf. Process. Lett., 1999

Formula Based Abstractions of Transition Systems for Real-Time Model Checking.
Proceedings of the FM'99 - Formal Methods, 1999

State Space Reduction by Non-Standard Semantics for Deadlock Analysis.
Sci. Comput. Program., 1998

Towards a Logical Semantics for Pure Prolog.
Sci. Comput. Program., 1998

A Transformation System for Concurrent Processes.
Acta Inf., 1998

Algebraic Computational Models of OR-Parallel Execution of Prolog.
Acta Inf., 1997

Selective µ-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems.
Proceedings of the Formal Description Techniques and Protocol Specification, 1997

Unfold/Fold Transformations of Concurrent Processes.
Proceedings of the Programming Languages: Implementations, 1996

A Non-Standard Semantics for Generating Reduced Transition Systems.
Proceedings of the Analysis and Verification of Multiple-Agent Languages, 1996

A Petri Nets Semantics for Data Flow Networks.
Acta Inf., 1995

Model Checking of Non-Finite State Processes by Finite Approximations.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1995

Modeling OR-Parallel Execution of Prolog using CHOCS.
Proceedings of the Logic Programming, 1995

Concurrent Behavior: A Construct to Specify the External Behavior of Objects in Object Databases.
Distributed and Parallel Databases, 1994

Proving Finiteness of CCS Processes by Non-Standard Semantics.
Acta Inf., 1994

Modelling Concurrent Accesses to Shared Data via Petri Nets.
Proceedings of the Programming Concepts, 1994

Axiomatizing CCS, Nets and Processes.
Sci. Comput. Program., 1993

Specification of Concurrency Control in Persistent Programming Languages.
Proceedings of the Persistent Object Systems, 1992

Towards innovative software engineering environments.
Journal of Systems and Software, 1991

A Semantic Driven Method to Check the Finiteness of CCS Processes.
Proceedings of the Computer Aided Verification, 3rd International Workshop, 1991

Shared Abstract Data Types: An Algebraic Methodology for Their Specification.
Proceedings of the MFDBS 89, 1989

Description of a Tool for Specifying and Prototyping Concurrent Programs.
IEEE Trans. Software Eng., 1988

Development of a Debugger for a Concurrent Language.
IEEE Trans. Software Eng., 1986

An Interactive Debugger for a Concurrent Language.
Proceedings of the Proceedings, 1985

Development of a debugger for a concurrent language.
SIGPLAN Notices, 1983