Stavros Tripakis

Softw. Syst. Model., April, 2024

Efficient Synthesis of Symbolic Distributed Protocols by Sketching.

[BibT_eX]

[DOI]

Derek Egolf

CoRR, 2024

Scalable, Interpretable Distributed Protocol Verification by Inductive Proof Slicing.

[BibT_eX]

[DOI]

CoRR, 2024

Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems.

[BibT_eX]

[DOI]

Yuhao Zhou

Proceedings of the NASA Formal Methods - 16th International Symposium, 2024

Shield Decentralization for Safe Reinforcement Learning in General Partially Observable Multi-Agent Environments.

[BibT_eX]

[DOI]

Daniel Melcer

Christopher Amato

Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems, 2024

2023

On tolerance of discrete systems with respect to transition perturbations.

[BibT_eX]

[DOI]

Discret. Event Dyn. Syst., December, 2023

Metrics and methods for robustness evaluation of neural networks with generative models.

[BibT_eX]

[DOI]

Igor Buzhinsky

Arseny Nerinovsky

Mach. Learn., October, 2023

Decoupled Fitness Criteria for Reactive Systems.

[BibT_eX]

[DOI]

Derek Egolf

Proceedings of the Software Engineering and Formal Methods - 21st International Conference, 2023

Safe Environmental Envelopes of Discrete Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

Synthesis of Distributed Protocols by Enumeration Modulo Isomorphisms.

[BibT_eX]

[DOI]

Derek Egolf

Proceedings of the Automated Technology for Verification and Analysis, 2023

2022

The refinement calculus of reactive systems.

[BibT_eX]

[DOI]

Inf. Comput., 2022

Decentralized Observation of Discrete-Event Systems: At Least One Can Tell.

[BibT_eX]

[DOI]

Karen Rudie

IEEE Control. Syst. Lett., 2022

Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+.

[BibT_eX]

[DOI]

Ian Dardik

CoRR, 2022

Shield Decentralization for Safe Multi-Agent Reinforcement Learning.

[BibT_eX]

[DOI]

Daniel Melcer

Christopher Amato

Proceedings of the Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, 2022

On Neural Network Equivalence Checking Using SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2022

Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA<sup>+</sup>.

[BibT_eX]

[DOI]

Ian Dardik

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems.

[BibT_eX]

[DOI]

Lisa Oakley

Alina Oprea

Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

Mapping Synthesis for Hyperproperties.

[BibT_eX]

[DOI]

Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

Formal verification of a distributed dynamic reconfiguration protocol.

[BibT_eX]

[DOI]

Ian Dardik

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2021

Artifact for Paper: On tolerance of discrete systems with respect to transition perturbations.

[BibT_eX]

[DOI]

Dataset, October, 2021

Learning Moore machines from input-output traces.

[BibT_eX]

[DOI]

Georgios Giantamidis

Stylianos Basagiannis

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

Compositional runtime enforcement revisited.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2021

Design and Verification of a Logless Dynamic Reconfiguration Protocol in MongoDB Replication.

[BibT_eX]

[DOI]

Siyuan Zhou

CoRR, 2021

Brief Announcement: Design and Verification of a Logless Dynamic Reconfiguration Protocol in MongoDB Replication.

[BibT_eX]

[DOI]

Siyuan Zhou

Proceedings of the 35th International Symposium on Distributed Computing, 2021

Design and Analysis of a Logless Dynamic Reconfiguration Protocol.

[BibT_eX]

[DOI]

Proceedings of the 25th International Conference on Principles of Distributed Systems, 2021

2020

The Refinement Calculus of Reactive Systems Toolset.

[BibT_eX]

[DOI]

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

Automated Attacker Synthesis for Distributed Protocols.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, Reliability, and Security, 2020

Efficient Translation of Safety LTL to DFA Using Symbolic Automata Learning and Inductive Inference.

[BibT_eX]

[DOI]

Georgios Giantamidis

Stylianos Basagiannis

Proceedings of the Computer Safety, Reliability, and Security, 2020

2019

Basic problems in multi-view modeling.

[BibT_eX]

[DOI]

Jan Reineke

Christos Stergiou

Softw. Syst. Model., 2019

Hybrid co-simulation: it's about time.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2019

Constrained synthesis from component libraries.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2019

Mechanically Proving Determinacy of Hierarchical Block Diagram Translations.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

Cross-Layer Interactions in CPS for Performance and Certification.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2019

Automated Synthesis of Secure Platform Mappings.

[BibT_eX]

[DOI]

Eunsuk Kang

Stéphane Lafortune

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Modeling for Verification.

[BibT_eX]

[DOI]

Sanjit A. Seshia

Natasha Sharygina

Proceedings of the Handbook of Model Checking., 2018

Checking multi-view consistency of discrete systems with respect to periodic sampling abstractions.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2018

Comparison of Two Theorem Provers: Isabelle/HOL and Coq.

[BibT_eX]

[DOI]

Artem Yushkovskiy

CoRR, 2018

Data-driven and model-based design.

[BibT_eX]

[DOI]

Proceedings of the IEEE Industrial Cyber-Physical Systems, 2018

Specification decomposition for synthesis from libraries of LTL Assume/Guarantee contracts.

[BibT_eX]

[DOI]

Proceedings of the 2018 Design, Automation & Test in Europe Conference & Exhibition, 2018

Multi-agent Coordination Subject to Counting Constraints: A Hierarchical Approach.

[BibT_eX]

[DOI]

Yunus Emre Sahin

Necmiye Ozay

Proceedings of the Distributed Autonomous Robotic Systems, 2018

Modular Code Generation from Synchronous Block Diagrams: Interfaces, Abstraction, Compositionality.

[BibT_eX]

[DOI]

Proceedings of the Principles of Modeling, 2018

2017

When Do We Not Need Complex Assume-Guarantee Rules?

[BibT_eX]

[DOI]

Antti Siirtola

Keijo Heljanko

ACM Trans. Embed. Comput. Syst., 2017

Runtime Enforcement of Cyber-Physical Systems.

[BibT_eX]

[DOI]

Reinhard von Hanxleden

ACM Trans. Embed. Comput. Syst., 2017

Automatic Synthesis of Distributed Protocols.

[BibT_eX]

[DOI]

Rajeev Alur

SIGACT News, 2017

Predictive runtime verification of timed properties.

[BibT_eX]

[DOI]

J. Syst. Softw., 2017

Predictive runtime enforcement.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2017

Supervisory control and reactive synthesis: a comparative introduction.

[BibT_eX]

[DOI]

Discret. Event Dyn. Syst., 2017

Synthesis of Property-Preserving Mappings.

[BibT_eX]

[DOI]

Eunsuk Kang

Stéphane Lafortune

CoRR, 2017

Runtime enforcement of reactive systems using synchronous enforcers.

[BibT_eX]

[DOI]

Reinhard von Hanxleden

Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

Type Inference of Simulink Hierarchical Block Diagrams in Isabelle.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

2016

Tokens vs. Signals: On Conformance between Formal Models of Dataflow and Hardware.

[BibT_eX]

[DOI]

J. Signal Process. Syst., 2016

Compositionality in the Science of System Design.

[BibT_eX]

[DOI]

Proc. IEEE, 2016

Compositional Model-Based System Design and Other Foundations for Mastering Change.

[BibT_eX]

[DOI]

LNCS Trans. Found. Mastering Chang., 2016

A Nondeterministic and Abstract Algorithm for Translating Hierarchical Block Diagrams.

[BibT_eX]

[DOI]

CoRR, 2016

Compositional Semantics and Analysis of Hierarchical Block Diagrams.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software - 23rd International Symposium, 2016

Multi-view consistency for infinitary regular languages.

[BibT_eX]

[DOI]

Maria Pittou

Proceedings of the International Conference on Embedded Computer Systems: Architectures, 2016

FIDE: an FMI integrated development environment.

[BibT_eX]

[DOI]

Fabio Cremona

Marten Lohstroh

Christopher X. Brooks

Proceedings of the 31st Annual ACM Symposium on Applied Computing, 2016

Compositional Runtime Enforcement.

[BibT_eX]

[DOI]

Srinivas Pinisetty

Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Step revision in hybrid Co-simulation with FMI.

[BibT_eX]

[DOI]

Proceedings of the 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, 2016

Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Learning Moore Machines from Input-Output Traces.

[BibT_eX]

[DOI]

Georgios Giantamidis

Proceedings of the FM 2016: Formal Methods, 2016

Checking Multi-view Consistency of Discrete Systems with Respect to Periodic Sampling Abstractions.

[BibT_eX]

[DOI]

Maria Pittou

Proceedings of the Formal Aspects of Component Software - 13th International Conference, 2016

2015

Translating Hierarchical Block Diagrams into Composite Predicate Transformers.

[BibT_eX]

[DOI]

CoRR, 2015

What's Decidable about Syntax-Guided Synthesis?

[BibT_eX]

[DOI]

CoRR, 2015

Efficient distribution of Triggered Synchronous Block Diagrams on asynchronous platforms.

[BibT_eX]

[DOI]

Yang Yang

Proceedings of the 2015 International Conference on Embedded Computer Systems: Architectures, 2015

Bridging the semantic gap between heterogeneous modeling formalisms and FMI.

[BibT_eX]

[DOI]

Proceedings of the 2015 International Conference on Embedded Computer Systems: Architectures, 2015

Towards cyber-physical agnosticism by enhancing IEC 61499 with PTIDES model of computations.

[BibT_eX]

[DOI]

Valeriy Vyatkin

Cheng Pang

Proceedings of the IECON 2015, 2015

Requirements for hybrid cosimulation standards.

[BibT_eX]

[DOI]

Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 2015

Automatic Completion of Distributed Protocols with Symmetry.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Optimized implementation of synchronous models on industrial LTTA systems.

[BibT_eX]

[DOI]

Marco Di Natale

Qi Zhu

J. Syst. Archit., 2014

Bridging the Gap between Supervisory Control and Reactive Synthesis: Case of Full Observation and Centralized Control.

[BibT_eX]

[DOI]

Proceedings of the 12th International Workshop on Discrete Event Systems, 2014

Basic Problems in Multi-View Modeling.

[BibT_eX]

[DOI]

Jan Reineke

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

On tokens and signals: Bridging the semantic gap between dataflow models and hardware implementations.

[BibT_eX]

[DOI]

Proceedings of the XIVth International Conference on Embedded Computer Systems: Architectures, 2014

Are interface theories equivalent to contract theories?

[BibT_eX]

[DOI]

Pierluigi Nuzzo

Proceedings of the Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2014

Game theoretic secure localization in wireless sensor networks.

[BibT_eX]

[DOI]

Susmit Jha

Sanjit A. Seshia

Krishnendu Chatterjee

Proceedings of the 4th International Conference on the Internet of Things, 2014

Synthesizing Finite-State Protocols from Scenarios and Requirements.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2014

Feedback in Synchronous Relational Interfaces.

[BibT_eX]

[DOI]

Chris Shaver

Proceedings of the From Programs to Systems. The Systems perspective in Computing, 2014

Refinement calculus of reactive systems.

[BibT_eX]

[DOI]

Proceedings of the 2014 International Conference on Embedded Software, 2014

Library-based scalable refinement checking for contract-based design.

[BibT_eX]

[DOI]

Pierluigi Nuzzo

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2014

2013

Compositionality in synchronous data flow: Modular code generation from hierarchical SDF graphs.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2013

A modular formal semantics for Ptolemy.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2013

Error-Completion in Interface Theories.

[BibT_eX]

[DOI]

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

Cyber-physical system design contracts.

[BibT_eX]

[DOI]

Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems (with CPS Week 2013), 2013

On the Verification of Timed Discrete-Event Models.

[BibT_eX]

[DOI]

Christos Stergiou

Eleftherios Matsikoudis

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2013

A characterization of integrated multi-view modeling in the context of embedded and cyber-physical systems.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Embedded Software, 2013

Determinate composition of FMUs for co-simulation.

[BibT_eX]

[DOI]

David Broman

Christopher X. Brooks

Proceedings of the International Conference on Embedded Software, 2013

Fault Diagnosis of Timed Systems.

[BibT_eX]

[DOI]

Proceedings of the Communicating Embedded Systems, 2013

2012

Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2012

Viewpoints, formalisms, languages, and tools for cyber-physical systems.

[BibT_eX]

[DOI]

Proceedings of the 6th International Workshop on Multi-Paradigm Modeling, 2012

An overview of the career of Paul Caspi.

[BibT_eX]

[DOI]

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

Static dataflow with access patterns: semantics and analysis.

[BibT_eX]

[DOI]

Proceedings of the 49th Annual Design Automation Conference 2012, 2012

2011

A Theory of Synchronous Relational Interfaces.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2011

The earlier the better: a theory of timed actor interfaces.

[BibT_eX]

[DOI]

Marc Geilen

Maarten Wiggers

Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, 2011

Correct and non-defensive glue design using abstract models.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Hardware/Software Codesign and System Synthesis, 2011

2010

Fault Diagnosis with Dynamic Observers

[BibT_eX]

[DOI]

CoRR, 2010

Compositionality in Synchronous Data Flow: modular code generation from hierarchical SDF graphs.

[BibT_eX]

[DOI]

Proceedings of the ACM/IEEE 1st International Conference on Cyber-Physical Systems, 2010

Modal Models in Ptolemy.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools, 2010

Exploring models of computation with ptolemy II.

[BibT_eX]

[DOI]

Christopher X. Brooks

Proceedings of the 8th International Conference on Hardware/Software Codesign and System Synthesis, 2010

2009

Checking timed Büchi automata emptiness on simulation graphs.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2009

Conformance testing for real-time systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2009

A Combined On-Line/Off-Line Framework for Black-Box Fault Diagnosis.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification, 9th International Workshop, 2009

Modular code generation from synchronous block diagrams: modularity vs. code size.

[BibT_eX]

[DOI]

Christian Szegedy

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Scalable Semantic Annotation Using Lattice-Based Ontologies.

[BibT_eX]

[DOI]

Proceedings of the Model Driven Engineering Languages and Systems, 2009

Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2009

Actors without Directors: A Kahnian View of Heterogeneous Systems.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 12th International Conference, 2009

On relational interfaces.

[BibT_eX]

[DOI]

Proceedings of the 9th ACM & IEEE International conference on Embedded software, 2009

2008

Semantics-preserving multitask implementation of synchronous programs.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2008

Automatic generation of path conditions for concurrent timed systems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2008

Implementing Synchronous Models on Loosely Time Triggered Architectures.

[BibT_eX]

[DOI]

Claudio Pinello

Albert Benveniste

Paul Caspi

Marco Di Natale

IEEE Trans. Computers, 2008

Fault Diagnosis with Static and Dynamic Observers.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2008

Resource-Aware Verification Using Randomized Exploration of Large State Spaces.

[BibT_eX]

[DOI]

Nazha Abed

Jean-Marc Vincent

Proceedings of the Model Checking Software, 2008

Modular Code Generation from Triggered and Timed Block Diagrams.

[BibT_eX]

[DOI]

Proceedings of the 14th IEEE Real-Time and Embedded Technology and Applications Symposium, 2008

Translating data flow to synchronous block diagrams.

[BibT_eX]

[DOI]

Proceedings of the 6th IEEE/ACM/IFIP Workshop on Embedded Systems for Real-Time Multimedia, 2008

Modularity vs. Reusability: Code Generation from Synchronous Block Diagrams.

[BibT_eX]

[DOI]

Proceedings of the Design, Automation and Test in Europe, 2008

2007

Synchronous Programming.

[BibT_eX]

[DOI]

Paul Caspi

Pascal Raymond

Proceedings of the Handbook of Real-Time and Embedded Systems., 2007

Synthesis Of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete-Event Systems.

[BibT_eX]

[DOI]

Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

A Simplified Approach for Testing Real-Time Systems Based on Action Refinement.

[BibT_eX]

[DOI]

Proceedings of the ISoLA 2007, 2007

Test Case Generation for Ultimately Periodic Paths.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2007

Loosely time-triggered architectures based on communication-by-sampling.

[BibT_eX]

[DOI]

Proceedings of the 7th ACM & IEEE International conference on Embedded software, 2007

Monitoring, Fault Diagnosis and Testing Real-time Systems using Analog and Digital Clocks.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification, 02.01. - 06.01.2007, 2007

Sensor Minimization Problems with Static or Dynamic Observers for Fault Diagnosis.

[BibT_eX]

[DOI]

Proceedings of the Seventh International Conference on Application of Concurrency to System Design (ACSD 2007), 2007

2006

Folk theorems on the determinization and minimization of timed automata.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2006

Ultimately Periodic Simple Temporal Problems (UPSTPs).

[BibT_eX]

[DOI]

Jean-François Condotta

Gérard Ligozat

Mahmoud Saade

Proceedings of the 13th International Symposium on Temporal Representation and Reasoning (TIME 2006), 2006

Deep Random Search for Efficient Model Checking of Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Composition of Embedded Systems. Scientific and Industrial Issues, 2006

Interesting Properties of the Real-Time Conformance Relation.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2006

State-Identification Problems for Finite-State Transducers.

[BibT_eX]

[DOI]

Proceedings of the Formal Approaches to Software Testing and Runtime Verification, 2006

A memory-optimal buffering protocol for preservation of synchronous semantics under preemptive scheduling.

[BibT_eX]

[DOI]

Christos Sofronis

Paul Caspi

Proceedings of the 6th ACM & IEEE International conference on Embedded software, 2006

Communication by sampling in time-sensitive distributed systems.

[BibT_eX]

[DOI]

Proceedings of the 6th ACM & IEEE International conference on Embedded software, 2006

Monitoring and fault-diagnosis with digital clocks

[BibT_eX]

[DOI]

Proceedings of the Sixth International Conference on Application of Concurrency to System Design (ACSD 2006), 2006

2005

Translating discrete-time simulink to lustre.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2005

Checking Timed Büchi Automata Emptiness Efficiently.

[BibT_eX]

[DOI]

Ahmed Bouajjani

Formal Methods Syst. Des., 2005

An Expressive and Implementable Formal Framework for Testing Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the Testing of Communicating Systems, 2005

State Identification Problems for Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Testing of Communicating Systems, 2005

Generating Path Conditions for Timed Systems.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 5th International Conference, 2005

Ultimately Periodic Qualitative Constraint Networks for Spatial and Temporal Reasoning.

[BibT_eX]

[DOI]

Jean-François Condotta

Gérard Ligozat

Proceedings of the 17th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2005), 2005

Implementation of Timed Automata: An Issue of Semantics or Modeling?

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2005

Semantics-preserving and memory-efficient implementation of inter-task communication on static-priority or EDF schedulers.

[BibT_eX]

[DOI]

Proceedings of the EMSOFT 2005, 2005

Decentralized Observation Problems.

[BibT_eX]

[DOI]

Proceedings of the 44th IEEE IEEE Conference on Decision and Control and 8th European Control Conference Control, 2005

Two-Phase Distributed Observation Problems.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), 2005

2004

Decentralized control of discrete-event Systems With bounded or Unbounded Delay communication.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 2004

Undecidable problems of decentralized observation and control on regular languages.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2004

Testing Conformance of Real-Time Applications by Automatic Generation of Observers.

[BibT_eX]

[DOI]

Proceedings of the Fourth Workshop on Runtime Verification, 2004

Black-Box Conformance Testing for Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2004

Automatic Generation of Path Conditions for Timed Systems.

[BibT_eX]

Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2004

Real-Time Testing with Timed Automata Testers and Coverage Criteria.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques, 2004

Defining and translating a "safe" subset of simulink/stateflow into lustre.

[BibT_eX]

[DOI]

Proceedings of the EMSOFT 2004, 2004

2003

Building models of real-time systems from application software.

[BibT_eX]

[DOI]

Joseph Sifakis

Proc. IEEE, 2003

Automated Module Composition.

[BibT_eX]

[DOI]

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

From simulink to SCADE/lustre to TTA: a layered approach for distributed embedded applications.

[BibT_eX]

[DOI]

Proceedings of the 2003 Conference on Languages, 2003

Translating Discrete-Time Simulink to Lustre.

[BibT_eX]

[DOI]

Proceedings of the Embedded Software, Third International Conference, 2003

2002

Automated Composition of Module Chains.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Software Composition, 2002

Algorithms for the Multi-constrained Routing Problem.

[BibT_eX]

[DOI]

Anuj Puri

Proceedings of the Algorithm Theory, 2002

Fault Diagnosis for Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

Description and Schedulability Analysis of the Software Architecture of an Automated Vehicle Control System.

[BibT_eX]

[DOI]

Proceedings of the Embedded Software, Second International Conference, 2002

A Protocol for Loosely Time-Triggered Architectures.

[BibT_eX]

[DOI]

Proceedings of the Embedded Software, Second International Conference, 2002

Decentralized diagnosability of regular languages is undecidable.

[BibT_eX]

[DOI]

Raja Sengupta

Proceedings of the 41st IEEE Conference on Decision and Control, 2002

2001

Analysis of Timed Systems Using Time-Abstracting Bisimulations.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2001

Timing Analysis and Code Generation of Vehicle Control Software using Taxys.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Runtime Verification, 2001

Hybrid Systems Applications: An Oxymoron?

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 4th International Workshop, 2001

A service network architecture for a multi-vehicle search mission.

[BibT_eX]

[DOI]

Proceedings of the 40th IEEE Conference on Decision and Control, 2001

Undecidable problems of decentralized observation and control.

[BibT_eX]

[DOI]

Proceedings of the 40th IEEE Conference on Decision and Control, 2001

2000

Verification of Hybrid Systems with Linear Differential Inclusions Using Ellipsoidal Approximations.

[BibT_eX]

[DOI]

Oleg Botchkarev

Proceedings of the Hybrid Systems: Computation and Control, Third International Workshop, 2000

1999

Timed Diagnostics for Reachability Properties.

[BibT_eX]

[DOI]

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

A Framework for Scheduler Synthesis.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE Real-Time Systems Symposium, 1999

On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the FM'99 - Formal Methods, 1999

Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics.

[BibT_eX]

[DOI]

Marius Bozga

Oded Maler

Proceedings of the Correct Hardware Design and Verification Methods, 1999

Verifying Progress in Timed Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Real-Time and Probabilistic Systems, 1999

1998

L'analyse formelle des systèmes temporisés en pratique. (The Formal Analysis of Timed Systems in Practice).

[BibT_eX]

[DOI]

PhD thesis, 1998

Model Checking of Real-Time Reachability Properties Using Abstractions.

[BibT_eX]

[DOI]

Conrado Daws

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

Verification of the Fast Reservation Protocol with Delayed Transmission using the Tool Kronos.

[BibT_eX]

[DOI]

Proceedings of the Fourth IEEE Real-Time Technology and Applications Symposium, 1998

KRONOS: A Model-Checking Tool for Real-Time Systems (Tool-Presentation for FTRTFT '98).

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1998

Kronos: A Model-Checking Tool for Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997

On-the-fly symbolic model checking for real-time systems.

[BibT_eX]

[DOI]

Ahmed Bouajjani

Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS '97), 1997

Modeling Urgency in Timed Systems.

[BibT_eX]

[DOI]

Sébastien Bornot

Joseph Sifakis

Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

1996

Extending Promela and Spin for Real Time.

[BibT_eX]

[DOI]

Costas Courcoubetis

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

Analysis of Timed Systems Based on Time-Abstracting Bisimulation.

[BibT_eX]

[DOI]