Cinzia Bernardeschi

Davide Caramella

Ruggero Dell'Osso

SIGBED Rev., 2019

Formal Verification in the Loop to Enhance Verification of Safety-Critical Cyber-physical Systems.

[BibT_eX]

[DOI]

Sergio Saponara

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2019

Co-simulation and Verification of a Non-linear Control System for Cogging Torque Reduction in Brushless Motors.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods, 2019

Exploiting Model Checking for Mobile Botnet Detection.

[BibT_eX]

[DOI]

Proceedings of the Knowledge-Based and Intelligent Information & Engineering Systems: Proceedings of the 23rd International Conference KES-2019, 2019

Modeling and Simulation of Attacks on Cyber-physical Systems.

[BibT_eX]

[DOI]

Proceedings of the 5th International Conference on Information Systems Security and Privacy, 2019

Application of Model Checking to Fault Tolerance Analysis.

[BibT_eX]

[DOI]

Proceedings of the From Software Engineering to Formal Methods and Tools, and Back, 2019

2018

Verifying data secure flow in AUTOSAR models.

[BibT_eX]

[DOI]

J. Comput. Virol. Hacking Tech., 2018

A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2018

OLT(RE)<sup>2</sup>: An On-Line On-Demand Testing Approach for Permanent Radiation Effects in Reconfigurable Systems.

[BibT_eX]

[DOI]

IEEE Trans. Emerg. Top. Comput., 2018

A Flexible Framework for FMI-Based Co-Simulation of Human-Centred Cyber-Physical Systems.

[BibT_eX]

[DOI]

Proceedings of the Software Technologies: Applications and Foundations, 2018

Demo: Co-simulation of UAVs with INTO-CPS and PVSio-web.

[BibT_eX]

[DOI]

Proceedings of the Software Technologies: Applications and Foundations, 2018

Towards Stochastic FMI Co-Simulations: Implementation of an FMU for a Stochastic Activity Networks Simulator.

[BibT_eX]

[DOI]

Proceedings of the Software Technologies: Applications and Foundations, 2018

PyXEL: An Integrated Environment for the Analysis of Fault Effects in SRAM-Based FPGA Routing.

[BibT_eX]

[DOI]

Proceedings of the 2018 International Symposium on Rapid System Prototyping, 2018

ROS/Gazebo Based Simulation of Co-operative UAVs.

[BibT_eX]

[DOI]

Proceedings of the Modelling and Simulation for Autonomous Systems, 2018

Data Leakage in Java Applets with Exception Mechanism.

[BibT_eX]

[DOI]

Antonella Santone

Proceedings of the Second Italian Conference on Cyber Security, Milan, Italy, February 6th - to, 2018

2017

Co-simulation of Semi-autonomous Systems: The Line Follower Robot Case Study.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods, 2017

Modeling and generation of secure component communications in AUTOSAR.

[BibT_eX]

[DOI]

Proceedings of the Symposium on Applied Computing, 2017

Verifying Data Secure Flow in AUTOSAR Models by Static Analysis.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Conference on Information Systems Security and Privacy, 2017

2016

Towards a Formalization of System Requirements for an Integrated Clinical Environment.

[BibT_eX]

[DOI]

EAI Endorsed Trans. Self Adapt. Syst., 2016

Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2016

UA<sup>2</sup>TPG: An untestability analyzer and test pattern generator for SEUs in the configuration memory of SRAM-based FPGAs.

[BibT_eX]

[DOI]

Integr., 2016

Extending a User Interface Prototyping Tool with Automatic MISRA C Code Generation.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Formal Integrated Development Environment, 2016

Adapting the Duty Cycle to Traffic Load in a Preamble Sampling MAC for WSNs: Formal Specification and Performance Evaluation.

[BibT_eX]

[DOI]

Ad Hoc Sens. Wirel. Networks, 2016

Using Smartwatch Sensors to Support the Acquisition of Sleep Quality Data for Supervised Machine Learning.

[BibT_eX]

[DOI]

Mario G. C. A. Cimino

Proceedings of the Wireless Mobile Communication and Healthcare, 2016

Detecting Elderly Behavior Shift via Smart Devices and Stigmergic Receptive Fields.

[BibT_eX]

[DOI]

Marco Avvenuti

Mario G. C. A. Cimino

Guglielmo Cola

Proceedings of the Wireless Mobile Communication and Healthcare, 2016

Using AUTOSAR High-Level Specifications for the Synthesis of Security Components in Automotive Systems.

[BibT_eX]

[DOI]

Proceedings of the Modelling and Simulation for Autonomous Systems, 2016

Modeling communication network requirements for an integrated clinical environment in the Prototype Verification System.

[BibT_eX]

[DOI]

Proceedings of the IEEE Symposium on Computers and Communication, 2016

2015

SRAM-Based FPGA Systems for Safety-Critical Applications: A Survey on Design Standards and Proposed Methodologies.

[BibT_eX]

[DOI]

J. Comput. Sci. Technol., 2015

2014

Design and Safety Verification of a Distributed Charge Equalizer for Modular Li-Ion Batteries.

[BibT_eX]

[DOI]

IEEE Trans. Ind. Informatics, 2014

ASSESS: A Simulator of Soft Errors in the Configuration Memory of SRAM-Based FPGAs.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2014

Combining PVSio with Stateflow.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

An inter-processor communication interface for data-flow centric heterogeneous embedded multiprocessor systems.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Design & Technology of Integrated Systems in Nanoscale Era, 2014

Exploiting dynamic partial reconfiguration for on-line on-demand testing of permanent faults in reconfigurable systems.

[BibT_eX]

[DOI]

Proceedings of the 2014 IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems, 2014

2013

GABES: A genetic algorithm based environment for SEU testing in SRAM-FPGAs.

[BibT_eX]

[DOI]

Mario G. C. A. Cimino

J. Syst. Archit., 2013

Mitigation of Single Event Upsets in the control logic of a charge equalizer for Li-ion batteries.

[BibT_eX]

[DOI]

Proceedings of the IECON 2013, 2013

Unexcitability analysis of SEus affecting the routing structure of SRAM-based FPGAs.

[BibT_eX]

[DOI]

Proceedings of the Great Lakes Symposium on VLSI 2013 (part of ECRC), 2013

Formal approaches to SEU testing in FPGAs.

[BibT_eX]

[DOI]

Proceedings of the 2013 NASA/ESA Conference on Adaptive Hardware and Systems, 2013

2012

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

[BibT_eX]

[DOI]

Marco Avvenuti

J. Syst. Softw., 2012

SEU-X: A SEu un-excitability prover for SRAM-FPGAs.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE International On-Line Testing Symposium, 2012

Accurate simulation of SEUs in the configuration memory of SRAM-based FPGAs.

[BibT_eX]

[DOI]

Proceedings of the 2012 IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems, 2012

2011

Failure Probability and Fault Observability of SRAM-FPGA Systems.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Field Programmable Logic and Applications, 2011

Failure probability of SRAM-FPGA systems with Stochastic Activity Networks.

[BibT_eX]

[DOI]

Proceedings of the 14th IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems, 2011

2009

Analysis of Wireless Sensor Network Protocols in Dynamic Scenarios.

[BibT_eX]

[DOI]

Holger Pfeifer

Proceedings of the Stabilization, 2009

2008

Decomposing bytecode verification by abstract interpretation.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2008

Early Prototyping of Wireless Sensor Network Algorithms in PVS.

[BibT_eX]

[DOI]

Holger Pfeifer

Proceedings of the Computer Safety, 2008

2006

Using postdomination to reduce space requirements of data flow analysis.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2006

Using Control Dependencies for Space-Aware Bytecode Verification.

[BibT_eX]

[DOI]

Comput. J., 2006

2005

A Space-Aware Bytecode Verifier for Java Cards.

[BibT_eX]

[DOI]

Proceedings of the First Workshop on Bytecode Semantics, 2005

FACT: A Tool for Code Generation from Communicating Automata.

[BibT_eX]

Gianluca Dini

Proceedings of the IASTED International Conference on Software Engineering, 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

Java bytecode verification with dynamic structures.

[BibT_eX]

Proceedings of the IASTED Conference on Software Engineering and Applications, 2004

Enforcement of applet boundaries in Java card systems.

[BibT_eX]

Proceedings of the IASTED Conference on Software Engineering and Applications, 2004

2003

Java bytecode verification for secure information flow.

[BibT_eX]

[DOI]

Marco Avvenuti

ACM SIGPLAN Notices, 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

Model checking fault tolerant systems.

[BibT_eX]

[DOI]

Softw. Test. Verification Reliab., 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

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]

Luca Tesei

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

Formal validation of fault-tolerance mechanisms inside GUARDS.

[BibT_eX]

[DOI]

Reliab. Eng. Syst. Saf., 2001

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

[BibT_eX]

[DOI]

Inf. Softw. Technol., 2001

2000

Formally Verifying Fault Tolerant System Designs.

[BibT_eX]

[DOI]

Luca Simoncini

Comput. J., 2000

1999

Formal Validation of the GUARDS Inter-Consistency Mechanism.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 1999

1998

A Formal Verification Environment for Railway Signaling System Design.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1998

Temporal analysis of data flow control systems.

[BibT_eX]

[DOI]

Autom., 1998

Validating the Design of Dependable Systems.

[BibT_eX]

[DOI]

Luca Simoncini

Proceedings of the 1st International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC '98), 1998

1997

An industrial application for the JACK environment.

[BibT_eX]

[DOI]

J. Syst. Softw., 1997

1996

Formal Verification of Safety Requirements on Complex Systems.

[BibT_eX]

[DOI]

Proceedings of the 15th International Conference on Computer Safety, 1996

Proving Safety Properties for Embedded Control Systems.

[BibT_eX]

[DOI]

Proceedings of the Dependable Computing, 1996

1995

Using Process Algebras for the Semantic Analysis of Data Flow Networks.

[BibT_eX]

[DOI]

Andrea Bondavalli

Luca Simoncini

IEICE Trans. Inf. Syst., 1995

A Petri Nets Semantics for Data Flow Networks.

[BibT_eX]

[DOI]

Acta Informatica, 1995

Application of Correctness Preserving Transformations for Deriving Architectural Descriptions of Interactive Systems from User Interface Specifications.

[BibT_eX]