Silvano Dal Zilio

Latest

• Property Directed Reachability for Generalized Petri Nets
• Hippo: A formal-model execution engine to control and verify critical real-time systems
• Accelerating the Computation of Dead and Concurrent Places Using Reductions
• On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets
• RT-MOBS: A compositional observer semantics of time Petri net for real-time property specification language based on μ-calculus
• A New Product Construction for the Diagnosability of Patterns in Time Petri Net
• A Short Overview on Diagnosability of Patterns in Timed Petri Net
• Checking marking reachability with the state equation in Petri net subclasses
• MCC: a Tool for Unfolding Colored Petri Nets in PNML Format
• On the Petri Nets with a Single Shared Place and Beyond
• Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites
• A State Class Construction for Computing the Intersection of Time Petri Nets Languages
• Counting Petri net markings from reduction equations
• Presentation of the 9th Edition of the Model Checking Contest
• On the Semantics of the GenoM3 Framework
• Formal Verification of Complex Robotic Systems on Resource-Constrained Platforms
• Petri Net Reductions for Counting Markings
• Time-accurate Middleware for the Virtualization of Communication Protocols
• Timed Formal Model and Verification of Satellite FDIR in Early Design Phase
• A Model-Checking Approach to Analyse Temporal Failure Propagation with AltaRica
• Formal Verification of User-Level Real-Time Property Patterns
• Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots
• Solving Language Equations Using Flanked Automata
• Building Confidence on Formal Verification Models
• Symmetry reduction for time Petri net state classes
• Integrating Model Checking in an Industrial Verification Process: a Structuring Approach
• Outillage pour la modélisation, la vérification et la génération d'applications temporisées et embarquées
• On the Complexity of Flanked Finite State Automata
• Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus
• Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina
• Symmetry reduced state classes for time petri nets
• Real-Time Model Checking Support for AADL
• Time Petri Nets with Dynamic Firing Dates: Semantics and Applications
• Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre
• Time Petri nets with dynamic firing dates: semantics and applications
• A formal framework to specify and verify real-time properties on critical systems
• An Experiment on Parallel Model Checking of a CTL Fragment
• Towards Timed Requirement Verification for Service Choreographies
• A Verified Approach for Checking Real-Time Specification Patterns
• Real-Time Specification Patterns and Tools
• A Timed Graphical Interval Logic
• Who Checks the Model-Checkers?
• Vérification formelle de spécifications AADL via FIACRE
• Mixed Shared-Distributed Hash Tables Approaches for Parallel State Space Construction
• Verification of Real-Time Specification Patterns on Time Transitions Systems
• Definition of the Fiacre Real-Time Specification Patterns Language
• A General Lock-Free Algorithm for Parallel State Space Construction
• Real-time Extensions for the Fiacre modeling language
• Formal Verification of AADL models with Fiacre and Tina
• Langage intermédiaire et transformations de modèles pour le développement de systèmes temps-réel: retour d'expérience sur la chaîne de vérification formelle Fiacre
• Enumerative Parallel and Distributed State Space Construction
• Formal Verification of AADL Specifications in the Topcased Environment
• Observation Graph implementation for TINA toolbox
• A Concurrent Calculus with Atomic Transactions
• A Typed Calculus for Querying Distributed XML Documents
• A Concurrent Calculus with Atomic Transactions
• XML schema, tree logic and sheaves automata
• Resource Control for Synchronous Cooperative Threads
• Resource Bound Certification for a Tail-Recursive Virtual Machine
• A Typed Calculus for Querying Distributed XML Documents
• A Functional Scenario for Bytecode Verification of Resource Bounds
• Resource Control for Synchronous Cooperative Threads
• A Functional Scenario for Bytecode Verification of Resource Bounds
• A Logic you Can Count On
• On the Dynamics of PB Systems: A Petri Net View
• Model Checking Mobile Ambients
• XML Schema, Tree Logic and Sheaves Automata
• Multitrees Automata, Presburger's Constraints and Tree Logics
• Region analysis and a pi-calculus with groups
• Fixed Points in the Ambient Logic
• Mobile Processes: a Commented Bibliography
• The Complexity of Model Checking Mobile Ambients
• Spatial Congruence for the Ambients is Decidable
• An Interpretation of Typed Concurrent Objects in the Blue Calculus
• Region analysis and a pi-calculus with groups
• An Interpretation of Extensible Objects
• Le calcul bleu: types et objets
• A Bisimulation for the Blue Calculus
• Concurrent Objects in the Blue Calculus
• Quiet and Bouncing Objects: Two Migration Abstractions in a Simple Distributed Blue Calculus
• Implicit Polymorphic Type System for the Blue Calculus
• Learning Binary Shapes as Compression and its Cellular Implementation