Enrico Tronci

Acta Informatica, 2018

Parallel Statistical Model Checking for Safety Verification in Smart Grids.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE International Conference on Communications, 2018

Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion co-located with the Federated Logic Conference, 2018

Computing Personalised Treatments through In Silico Clinical Trials.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion co-located with the Federated Logic Conference, 2018

An Efficient Algorithm for Network Vulnerability Analysis Under Malicious Attacks.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Intelligent Systems - 24th International Symposium, 2018

2017

Residential Demand Management Using Individualized Demand Aware Price Policies.

[BibT_eX]

[DOI]

IEEE Trans. Smart Grid, 2017

Linearizing Discrete-Time Hybrid Systems.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 2017

Parallelization of Cycle-Based Logic Simulation.

[BibT_eX]

[DOI]

Toni Mancini

Annalisa Massini

Parallel Process. Lett., 2017

On minimising the maximum expected verification time.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2017

Modeling cyber-physical systems for automatic verification.

[BibT_eX]

[DOI]

Youssef Driouich

Mimmo Parente

Proceedings of the 14th International Conference on Synthesis, 2017

2016

Anytime system level verification via parallel random exhaustive hardware in the loop simulation.

[BibT_eX]

[DOI]

Microprocess. Microsystems, 2016

SyLVaaS: System Level Formal Verification as a Service.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2016

2015

Simulator Semantics for System Level Formal Verification.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Sixth International Symposium on Games, 2015

Computing Biological Model Parameters by Parallel Statistical Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Bioinformatics and Biomedical Engineering, 2015

User Flexibility Aware Price Policy Synthesis for Smart Grids.

[BibT_eX]

[DOI]

Proceedings of the 2015 Euromicro Conference on Digital System Design, 2015

A Glimpse of SmartHG Project Test-bed and Communication Infrastructure.

[BibT_eX]

[DOI]

Emad Samuel Malki Ebeid

Søren Aagaard Mikkelsen

Rune Hylsberg Jacobsen

Proceedings of the 2015 Euromicro Conference on Digital System Design, 2015

2014

Model-based synthesis of control software from system-level formal specifications.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2014

Demand-aware price policy synthesis and verification services for Smart Grids.

[BibT_eX]

[DOI]

Proceedings of the 2014 IEEE International Conference on Smart Grid Communications, 2014

System Level Formal Verification via Distributed Multi-core Hardware in the Loop Simulation.

[BibT_eX]

[DOI]

Proceedings of the 22nd Euromicro International Conference on Parallel, 2014

Patient-specific models from inter-patient biological models and clinical records.

[BibT_eX]

[DOI]

Tillmann H. C. Kruger

Marcel Egli

Fabian Ille

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

Anytime System Level Verification via Random Exhaustive Hardware in the Loop Simulation.

[BibT_eX]

[DOI]

Proceedings of the 17th Euromicro Conference on Digital System Design, 2014

2013

A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET.

[BibT_eX]

[DOI]

Mob. Inf. Syst., 2013

CGMurphi: Automatic synthesis of numerical controllers for nonlinear hybrid systems.

[BibT_eX]

[DOI]

Eur. J. Control, 2013

On-the-Fly Control Software Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software - 20th International Symposium, 2013

A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software - 20th International Symposium, 2013

System Level Formal Verification via Model Checking Driven Simulation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

Undecidability of Quantized State Feedback Control for Discrete Time Linear Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2012, 2012

On model based synthesis of embedded control software.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Embedded Software, 2012

Automatic control software synthesis for quantized discrete time hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the 51th IEEE Conference on Decision and Control, 2012

2011

Flexible Plan Verification: Feasibility Results.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2011

Quantized Feedback Control Software Synthesis from System Level Formal Specifications

[BibT_eX]

[DOI]

CoRR, 2011

From Boolean Functional Equations to Control Software

[BibT_eX]

[DOI]

CoRR, 2011

Quantized Feedback Control Software Synthesis from System Level Formal Specifications for Buck DC/DC Converters

[BibT_eX]

[DOI]

CoRR, 2011

Cost-optimal Strong Planning in Non-deterministic Domains.

[BibT_eX]

Proceedings of the ICINCO 2011 - Proceedings of the 8th International Conference on Informatics in Control, Automation and Robotics, Volume 1, Noordwijkerhout, The Netherlands, 28, 2011

2010

Validation and verification issues in a timeline-based planning system.

[BibT_eX]

[DOI]

Knowl. Eng. Rev., 2010

Analyzing Flexible Timeline-based Plans.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2010, 2010

Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems.

[BibT_eX]

[DOI]

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

2009

Model Checking Coalition Nash Equilibria in MAD Distributed Systems.

[BibT_eX]

[DOI]

Proceedings of the Stabilization, 2009

Flexible Timeline-Based Plan Verification.

[BibT_eX]

[DOI]

Proceedings of the KI 2009: Advances in Artificial Intelligence, 2009

Risk analysis via heterogeneous models of SCADA interconnecting Power Grids and Telco networks.

[BibT_eX]

[DOI]

Proceedings of the CRiSIS 2009, 2009

2008

Model Checking Nash Equilibria in MAD Distributed Systems.

[BibT_eX]

[DOI]

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

2007

CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems.

[BibT_eX]

[DOI]

Federico Mari

Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Disk Based Software Verification via Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 14th Asia-Pacific Software Engineering Conference (APSEC 2007), 2007

2006

Introductory Paper.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2006

Finite horizon analysis of Markov Chains with the Murphi verifier.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2006

Automatic generation of optimal controllers through model checking techniques.

[BibT_eX]

Proceedings of the ICINCO 2006, 2006

A Case Study on Automated Generation of Integration Tests.

[BibT_eX]

[DOI]

Proceedings of the Forum on specification and Design Languages, 2006

2005

Automatic Analysis of a Safety Critical Tele Control System.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 2005

A Model Checking Technique for the Verification of Fuzzy Control Systems.

[BibT_eX]

[DOI]

Proceedings of the 2005 International Conference on Computational Intelligence for Modelling Control and Automation (CIMCA 2005), 2005

Exploiting Hub States in Automatic Verification.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2005

2004

Exploiting transition locality in automatic verification of finite-state concurrent systems.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2004

Automated analysis of timed security: a case study on web privacy.

[BibT_eX]

[DOI]

Roberto Gorrieri

Fabio Martinelli

Int. J. Inf. Sec., 2004

Electric Power System Anomaly Detection Using Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the Knowledge-Based Intelligent Information and Engineering Systems, 2004

Automatic Covert Channel Analysis of a Multilevel Secure Component.

[BibT_eX]

[DOI]

Angelo Troina

Proceedings of the Information and Communications Security, 6th International Conference, 2004

Bounded Probabilistic Model Checking with the Mur<i>alpha</i> Verifier.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

2003

Fluid Petri Nets and hybrid model-checking: a comparative case study.

[BibT_eX]

[DOI]

Reliab. Eng. Syst. Saf., 2003

Automatic Analysis of the NRL Pump.

[BibT_eX]

[DOI]

Angelo Troina

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

Automatic Timeliness Verification of a Public Mobile Network.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 2003

Finite Horizon Analysis of Stochastic Systems with the Mur varphi Verifier.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

Automatic Verification of a Turbogas Control System with the Mur varphi Verifier.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 2003

Finite Horizon Analysis of Markov Chains with the Mur-phi Verifier.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2003

Integrating RAM and Disk Based Verification within the Mur-phi Verifier.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002

Model-Checking Based on Fluid Petri Nets for the Temperature Control System of the ICARO Co-generative Plant.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 2002

Exploiting Transition Locality in the Disk Based Mur phi Verifier.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

2001

Synchronized Regular Expressions.

[BibT_eX]

[DOI]

Proceedings of the Theory of Concurrency, Higher Order Languages and Types, 2001

Formal Models of Timing Attacks on Web Privacy.

[BibT_eX]

[DOI]

Riccardo Focardi

Roberto Gorrieri

Fabio Martinelli

Proceedings of the Theory of Concurrency, Higher Order Languages and Types, 2001

Integrating Automatic Verification of Safety Requirements in Railway Interlocking System Design.

[BibT_eX]

[DOI]

Giovanni Dipoppa

Giovanni D'Alessandro

Roberto Semprini

Proceedings of the 6th IEEE International Symposium on High-Assurance Systems Engineering (HASE 2001), 2001

Exploiting Transition Locality in Automatic Verification.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2001

A Probabilistic Approach to Automatic Verification of Concurrent Systems.

[BibT_eX]

[DOI]

Proceedings of the 8th Asia-Pacific Software Engineering Conference (APSEC 2001), 2001

2000

Requirements formalization and validation for a telecommunication equipment protection switcher.

[BibT_eX]

[DOI]

Michele Cecconi

Proceedings of the 5th IEEE International Symposium on High-Assurance Systems Engineering (HASE 2000), 2000

1999

Automatic Synthesis of Control Software for an Industrial Automation Control System.

[BibT_eX]

[DOI]

Proceedings of the 14th IEEE International Conference on Automated Software Engineering, 1999

Formally Modeling a Metal Processing Plant and its Closed Loop Specifications.

[BibT_eX]

[DOI]

Proceedings of the 4th IEEE International Symposium on High-Assurance Systems Engineering (HASE '99), 1999

1998

Automatic Synthesis of Controllers from Formal Specifications.

[BibT_eX]

[DOI]

Proceedings of the Second IEEE International Conference on Formal Engineering Methods, 1998

A Symbolic Model Checker for ACTL.

[BibT_eX]

[DOI]

Proceedings of the Applied Formal Methods, 1998

1996

Equational Programming in Lambda-Calculus via SL-Systems. Part 2.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1996

Equational Programming in Lambda-Calculus via SL-Systems. Part 1.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1996

Automatic Verification of a Hydroelectric Power Plant.

[BibT_eX]

[DOI]

Rosario Pugliese

Proceedings of the FME '96: Industrial Benefit and Advances in Formal Methods, 1996

1995

Defining Data Structures via Böhm-Out.

[BibT_eX]

[DOI]

J. Funct. Program., 1995

Hardware Verification, Boolean Logic Programming, Boolean Functional Programming

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 1995

1991

About Systems of Equations, X-Separability, and Left-Invertibility in the lambda-Calculus

[BibT_eX]

[DOI]

Corrado Böhm

Inf. Comput., January, 1991

Equational Prgoramming in lambda-calculus

[BibT_eX]

[DOI]

Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

1990

Regular Systems in lambda-Calculus.

[BibT_eX]

[DOI]

Adolfo Piperno

Int. J. Found. Comput. Sci., 1990

1987

X-Separability and Left-Invertibility in lambda-calculus

[BibT_eX]

Corrado Böhm