Joseph Sifakis

Orcid: 0000-0003-2447-7981

According to our database1, Joseph Sifakis authored at least 197 papers between 1974 and 2024.

Collaborative distances:

Awards

Turing Prize recipient

Turing Prize 2007, "For their roles in developing model checking into a highly effective verification technology, widely adopted in the hardware and software industries." awarded to Edmund M. Clarke and E. Allen Emerson and Joseph Sifakis.

ACM Fellow

ACM Fellow 2012, "For contributions to hardware and software verification technology.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Design for dependability - State of the art and trends.
J. Syst. Softw., 2024

Rigorous Simulation-based Testing for Autonomous Driving Systems - Targeting the Achilles' Heel of Four Open Autopilots.
CoRR, 2024

Safe by Design Autonomous Driving Systems.
CoRR, 2024

2023
Correct by design coordination of autonomous driving systems.
Int. J. Softw. Tools Technol. Transf., December, 2023

What perceptron neural networks are (not) good for?
Inf. Sci., April, 2023

Trustworthy Autonomous System Development.
ACM Trans. Embed. Comput. Syst., 2023

Verification of component-based systems with recursive architectures.
Theor. Comput. Sci., 2023

Testing System Intelligence.
CoRR, 2023

Simulation-Based Validation for Autonomous Driving Systems.
Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, 2023

2022
A hybrid controller for safe and efficient longitudinal collision avoidance control.
J. Syst. Archit., 2022

Creating a Foundation for Next-Generation Autonomous Systems.
IEEE Des. Test, 2022

Runtime Safety Assurance for Learning-enabled Control of Autonomous Driving Vehicles.
Proceedings of the 2022 International Conference on Robotics and Automation, 2022

Specification and Validation of Autonomous Driving Systems: A Multilevel Semantic Framework.
Proceedings of the Principles of Systems Design, 2022

Understanding and Changing the World - From Information to Knowledge and Intelligence
Springer, ISBN: 978-981-19-1931-2, 2022

2021
Programming dynamic reconfigurable systems.
Int. J. Softw. Tools Technol. Transf., 2021

Checking deadlock-freedom of parametric component-based systems.
J. Log. Algebraic Methods Program., 2021

A hybrid controller for safe and efficient collision avoidance control.
CoRR, 2021

Why is it so hard to make self-driving cars? (Trustworthy autonomous systems).
Proceedings of the WI-IAT '21: IEEE/WIC/ACM International Conference on Web Intelligence, Melbourne VIC Australia, December 14, 2021

A temporal configuration logic for dynamic reconfigurable systems.
Proceedings of the SAC '21: The 36th ACM/SIGAPP Symposium on Applied Computing, 2021

2020
The DReAM framework for dynamic reconfigurable architecture modelling: theory and applications.
Int. J. Softw. Tools Technol. Transf., 2020

Autonomics: In search of a foundation for next-generation autonomous systems.
Proc. Natl. Acad. Sci. USA, 2020

Structural Invariants for the Verification of Systems with Parameterized Architectures.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

A Layered Implementation of DR-BIP Supporting Run-Time Monitoring and Analysis.
Proceedings of the Software Engineering and Formal Methods - 18th International Conference, 2020

Safe and efficient collision avoidance control for autonomous vehicles.
Proceedings of the 18th ACM/IEEE International Conference on Formal Methods and Models for System Design, 2020

2019
Rigorous design of cyber-physical systems - Linking physicality and computation.
Softw. Syst. Model., 2019

Local Reasoning about Parametric and Reconfigurable Component-based Systems.
CoRR, 2019

Structural Invariants for Parametric Verification of Systems with Almost Linear Architectures.
CoRR, 2019

Autonomous Systems - An Architectural Characterization.
Proceedings of the Models, Languages, and Tools for Concurrent and Distributed Programming, 2019

A Logic-Inspired Approach to Reconfigurable System Modelling.
Proceedings of the From Reactive Systems to Cyber-Physical Systems, 2019

Can We Trust Autonomous Systems? Boundaries and Risks.
Proceedings of the Automated Technology for Verification and Analysis, 2019

2018
Global and Local Deadlock Freedom in BIP.
ACM Trans. Softw. Eng. Methodol., 2018

Early validation of system requirements and design through correctness-by-construction.
J. Syst. Softw., 2018

System Design in the Era of IoT - Meeting the Autonomy Challenge.
Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design, 2018

DesignBIP: A Design Studio for Modeling and Generating Systems with BIP.
CoRR, 2018

DReAM: Dynamic Reconfigurable Architecture Modeling (full paper).
CoRR, 2018

DReAM: Dynamic Reconfigurable Architecture Modeling.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, 2018

Four Exercises in Programming Dynamic Reconfigurable Systems: Methodology and Solution in DR-BIP.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, 2018

2017
Configuration logics: Modeling architecture styles.
J. Log. Algebraic Methods Program., 2017

Functional BIP: Embedding connectors in functional programming languages.
J. Log. Algebraic Methods Program., 2017

2016
Component-based verification using incremental design and invariants.
Softw. Syst. Model., 2016

A general framework for architecture composability.
Formal Aspects Comput., 2016

Architecture Diagrams: A Graphical Language for Architecture Style Specification.
Proceedings of the Proceedings 9th Interaction and Concurrency Experience, 2016

Architecture-Based Design: A Satellite On-Board Software Case Study.
Proceedings of the Formal Aspects of Component Software - 13th International Conference, 2016

Parameterized Systems in BIP: Design and Model Checking.
Proceedings of the 27th International Conference on Concurrency Theory, 2016

2015
Optimized distributed implementation of multiparty interactions with Restriction.
Sci. Comput. Program., 2015

System Design Automation: Challenges and Limitations.
Proc. IEEE, 2015

Configuration Logics: Modelling Architecture Styles.
Proceedings of the Formal Aspects of Component Software - 12th International Conference, 2015

A Theory Agenda for Component-Based Design.
Proceedings of the Software, 2015

2014
Keynote talk III: A framework for modeling architectures and their properties.
Proceedings of the Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2014

Toward a System Design Science.
Proceedings of the From Programs to Systems. The Systems perspective in Computing, 2014

Architecture internalisation in BIP.
Proceedings of the CBSE'14, Proceedings of the 17th International ACM SIGSOFT Symposium on Component-Based Software Engineering (part of CompArch 2014), Marcq-en-Baroeul, Lille, France, June 30, 2014

2013
Introduction to the special section on rigorous embedded systems design.
ACM Trans. Embed. Comput. Syst., 2013

Rigorous implementation of real-time systems - from theory to application.
Math. Struct. Comput. Sci., 2013

Rigorous System Design.
Found. Trends Electron. Des. Autom., 2013

An Abstract Framework for Deadlock Prevention in BIP.
Proceedings of the Formal Techniques for Distributed Systems, 2013

Model-Based Implementation of Parallel Real-Time Systems.
Proceedings of the Fundamental Approaches to Software Engineering, 2013

2012
2010 CAV award announcement.
Formal Methods Syst. Des., 2012

A framework for automated distributed implementation of component-based models.
Distributed Comput., 2012

Rigorous Component-Based System Design - (Invited Paper).
Proceedings of the Rewriting Logic and Its Applications - 9th International Workshop, 2012

Modeling Dynamic Architectures Using Dy-BIP.
Proceedings of the Software Composition - 11th International Conference, 2012

Rigorous design of cyber-physical systems.
Proceedings of the 2012 International Conference on Embedded Computer Systems: Architectures, 2012

Trustworthy Computing Systems.
Proceedings of the PECCS 2012, 2012

Knowledge-Based Distributed Conflict Resolution for Multiparty Interactions and Priorities.
Proceedings of the Formal Techniques for Distributed Systems, 2012

Optimized distributed implementation of multiparty interactions with observation.
Proceedings of the 2nd edition on Programming systems, 2012

Systems Architecture, Design, Engineering, and Verification - The Practice in Research and Research in Practice.
Proceedings of the ACM Turing Centenary Celebration, 2012

2011
Rigorous Component-Based System Design Using the BIP Framework.
IEEE Softw., 2011

Priority scheduling of distributed systems based on model checking.
Formal Methods Syst. Des., 2011

A vision for computer science - the system perspective.
Central Eur. J. Comput. Sci., 2011

Synthesizing Glue Operators from Glue Constraints for the Construction of Component-Based Systems.
Proceedings of the Software Composition - 10th International Conference, 2011

D-Finder 2: Towards Efficient Correctness of Incremental Design.
Proceedings of the NASA Formal Methods, 2011

Rigorous system level modeling and analysis of mixed HW/SW systems.
Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, 2011

Rigorous System Design: The BIP Approach.
Proceedings of the Mathematical and Engineering Methods in Computer Science, 2011

Component Assemblies in the Context of Manycore.
Proceedings of the Formal Methods for Components and Objects, 10th International Symposium, 2011

Time-predictable and composable architectures for dependable embedded systems.
Proceedings of the 11th International Conference on Embedded Software, 2011

Methods and tools for component-based system design.
Proceedings of the Design, Automation and Test in Europe, 2011

2010
Source-to-Source Architecture Transformation for Performance Optimization in BIP.
IEEE Trans. Ind. Informatics, 2010

Compositional verification for component-based systems and application.
IET Softw., 2010

2009 CAV award announcement.
Formal Methods Syst. Des., 2010

Causal semantics for the algebra of connectors.
Formal Methods Syst. Des., 2010

Incremental Invariant Generation for Compositional Design.
Proceedings of the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2010

Embedded Systems Design - Scientific Challenges and Work Directions.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Systematic Correct Construction of Self-stabilizing Systems: A Case Study.
Proceedings of the Stabilization, Safety, and Security of Distributed Systems, 2010

Compositional Translation of Simulink Models into Synchronous BIP.
Proceedings of the IEEE Fifth International Symposium on Industrial Embedded Systems, 2010

Automated Conflict-free distributed implementation of component-based models.
Proceedings of the IEEE Fifth International Symposium on Industrial Embedded Systems, 2010

Incremental component-based construction and verification using invariants.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

From high-level component-based models to distributed implementations.
Proceedings of the 10th International conference on Embedded software, 2010

Model-based implementation of real-time applications.
Proceedings of the 10th International conference on Embedded software, 2010

Component-based Construction of Heterogeneous Real-time Systems in BIP.
Proceedings of the Future of Software Engineering., 2010

Knowledge Based Scheduling of Distributed Systems.
Proceedings of the Time for Verification, 2010

2009
Model checking: algorithmic verification and debugging.
Commun. ACM, 2009

Brief Announcement: Incremental Component-Based Modeling, Verification, and Performance Evaluation of Distributed Reset.
Proceedings of the Distributed Computing, 23rd International Symposium, 2009

The Quest for Correctness-Beyond a Posteriori Verification.
Proceedings of the Model Checking Software, 2009

Modeling synchronous systems in BIP.
Proceedings of the 9th ACM & IEEE International conference on Embedded software, 2009

Component-Based Construction of Real-Time Systems in BIP.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

D-Finder: A Tool for Compositional Deadlock Detection and Verification.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
The Algebra of Connectors - Structuring Interaction in BIP.
IEEE Trans. Computers, 2008

Symbolic quality control for multimedia applications.
Real Time Syst., 2008

Specification and Verification of Conurrent Systems in Cesar.
Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008

Translating AADL into BIP - Application to the Verification of Real-Time Systems.
Proceedings of the Models in Software Engineering, Workshops and Symposia at MODELS 2008, Toulouse, France, September 28, 2008

Distributed Semantics and Implementation for Systems with Interaction and Priority.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2008

Incremental Component-Based Construction and Verification of a Robotic System.
Proceedings of the ECAI 2008, 2008

A Notion of Glue Expressiveness for Component-Based Systems.
Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

2007
The Discipline of Embedded Systems Design.
Computer, 2007

An Approach to Modelling and Verification of Component Based Systems.
Proceedings of the SOFSEM 2007: Theory and Practice of Computer Science, 2007

Using BIP for Modeling and Verification of Networked Systems -- A Case Study on TinyOS-based Networks.
Proceedings of the Sixth IEEE International Symposium on Network Computing and Applications (NCA 2007), 12, 2007

Using Speed Diagrams for Symbolic Quality Management.
Proceedings of the 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), 2007

2006
Modeling Heterogeneous Real-time Components in BIP.
Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), 2006

A Methodology and Supporting Tools for the Development of Component-Based Embedded Systems.
Proceedings of the Composition of Embedded Systems. Scientific and Industrial Issues, 2006

WPDRTS keynote: component-based construction of embedded systems.
Proceedings of the 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), 2006

The Embedded Systems Design Challenge.
Proceedings of the FM 2006: Formal Methods, 2006

Ensuring Properties of Interaction Systems.
Proceedings of the Program Analysis and Compilation, 2006

2005
Guidelines for a graduate curriculum on embedded software and systems.
ACM Trans. Embed. Comput. Syst., 2005

Composition for component-based modeling.
Sci. Comput. Program., 2005

A Framework for Component-based Construction Extended Abstract.
Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

QoS control for optimality and safety.
Proceedings of the EMSOFT 2005, 2005

Fine Grain QoS Control for Multimedia Application Software.
Proceedings of the 2005 Design, 2005

Embedded Systems Design: The ARTIST Roadmap for Research and Development
Lecture Notes in Computer Science 3436, Springer, ISBN: 3-540-25107-3, 2005

2004
The IF Toolset.
Proceedings of the Formal Methods for the Design of Real-Time Systems, 2004

Modeling Real-Time Systems.
Proceedings of the 25th IEEE Real-Time Systems Symposium (RTSS 2004), 2004

Embedded Systems - Challenges and Work Directions.
Proceedings of the Principles of Distributed Systems, 8th International Conference, 2004

2003
Building models of real-time systems from application software.
Proc. IEEE, 2003

Component-Based Construction of Deadlock-Free Systems: Extended Abstract.
Proceedings of the FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 2003

Priority Systems.
Proceedings of the Formal Methods for Components and Objects, 2003

2002
Scheduler Modeling Based on the Controller Synthesis Paradigm.
Real Time Syst., 2002

Abstracts of Invited Talks.
Proceedings of the Theory and Practice of Timed Systems, 2002

Scheduler Modeling Based on the Controller Synthesis Paradigm.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

2001
Modeling Real-Time Systems-Challenges and Work Directions.
Proceedings of the Embedded Software, First International Workshop, 2001

TAXYS=Esterel+Kronos. A tool for verifying real-time properties of embedded systems.
Proceedings of the 40th IEEE Conference on Decision and Control, 2001

TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000
An Algebraic Framework for Urgency.
Inf. Comput., 2000

On the Construction of Live Timed Systems.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

A Methodology for the Construction of Scheduled Systems.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2000

Towards validated real-time software.
Proceedings of the 12th Euromicro Conference on Real-Time Systems (ECRTS 2000), 2000

1999
Decidable Integration Graphs.
Inf. Comput., 1999

IF: An intermediate representation for SDL and its applications.
Proceedings of the SDL '99 The Next Millennium, 1999

A Framework for Scheduler Synthesis.
Proceedings of the 20th IEEE Real-Time Systems Symposium, 1999

Integration, the Price of Success.
Proceedings of the FM'99 - Formal Methods, 1999

The Compositional Specification of Timed Systems - A Tutorial.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998
On the Composition of Hybrid Systems.
Proceedings of the Hybrid Systems: Computation and Control, First International Workshop, 1998

A General Framework for the Composition of Timed Systems Extended Abstract.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1998

1997
Relating Time Progress and Deadlines in Hybrid Systems.
Proceedings of the Hybrid and Real-Time Systems, 1997

Modeling Urgency in Timed Systems.
Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

On the Composition of Timed Systems.
Proceedings of the Application and Theory of Petri Nets 1997, 1997

1996
Research Directions for Formal Methods.
ACM Comput. Surv., 1996

Research Directions for Concurrency.
ACM Comput. Surv., 1996

Compositional Specification of Timed Systems (Extended Abstract).
Proceedings of the STACS 96, 1996

Formal Methods for the Validation of Fault Tolerance in Autonomous Spacecraft.
Proceedings of the Digest of Papers: FTCS-26, 1996

1995
The Algorithmic Analysis of Hybrid Systems.
Theor. Comput. Sci., 1995

Property Preserving Abstractions for the Verification of Concurrent Systems.
Formal Methods Syst. Des., 1995

On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract).
Proceedings of the STACS 95, 1995

Real-time systems specification and verification.
Proceedings of the 8th International Symposium on System Synthesis (ISSS 1995), 1995

Specification and Verification of Timed Systems.
Proceedings of the Formal Description Techniques VIII, 1995

1994
The Algebra of Timed Processes, ATP: Theory and Application
Inf. Comput., October, 1994

Symbolic Model Checking for Real-Time Systems
Inf. Comput., June, 1994

Model-Based Verification Methods and Tools (Abstract).
Proceedings of the CONCUR '94, 1994

Using Abstractions for the Verification of Linear Hybrid Systems.
Proceedings of the Computer Aided Verification, 6th International Conference, 1994

1993
From ATP to Timed Graphs and Hybrid Systems.
Acta Informatica, 1993

On Model Checking for Real-Time Properties with Durations
Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

1992
Compiling Real-Time Specifications into Extended Automata.
IEEE Trans. Software Eng., 1992

A Toolbox for the Verification of LOTOS Programs.
Proceedings of the 14th International Conference on Software Engineering, 1992

An Approach to the Description and Analysis of Hybrid Systems.
Proceedings of the Hybrid Systems, 1992

Integration Graphs: A Class of Decidable Hybrid Systems.
Proceedings of the Hybrid Systems, 1992

Property Preserving Simulations.
Proceedings of the Computer Aided Verification, Fourth International Workshop, 1992

1991
Verification for Finite Systems (Extended Abstract).
Proceedings of the TAPSOFT'91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1991

Safety for Branching Time Semantics.
Proceedings of the Automata, Languages and Programming, 18th International Colloquium, 1991

An Overview and Synthesis on Timed Process Algebras.
Proceedings of the Computer Aided Verification, 3rd International Workshop, 1991

An Algebra of Boolean Processes.
Proceedings of the Computer Aided Verification, 3rd International Workshop, 1991

1990
Compilation and verification of LOTOS specifications.
Proceedings of the Protocol Specification, 1990

ATP: an Algebra for Timed Processes.
Proceedings of the Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 1990

1988
A logig for the description of behaviours and properties of concurrent systems.
Proceedings of the Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands, May 30, 1988

1987
An Expressive Logic for a Process Algebra with Silent Actions.
Proceedings of the Temporal Logic in Specification, 1987

Verification in XESAR of the Sliding Window Protocol.
Proceedings of the Protocol Specification, 1987

Readiness Semantics for Regular Processes with Silent Actions.
Proceedings of the Automata, Languages and Programming, 14th International Colloquium, 1987

1986
A Logic for the Description of Non-deterministic Programs and Their Properties
Inf. Control., 1986

A Modal Characterization of Observational Congruence on Finite Terms of CCS
Inf. Control., 1986

A Logic for the Specification and Proof of Regular Controllable Processes of CCS.
Acta Informatica, 1986

Specification and Development of Reactive Systems - Response.
Proceedings of the Information Processing 86, 1986

1985
Frm Synchronization Tree Logic to Acceptance Model Logic.
Proceedings of the Logics of Programs, 1985

1984
A Logic for the Specification and Proof of Controllable Processes of CCS.
Proceedings of the Logics and Models of Concurrent Systems, 1984

1983
Fairness and Related Properties in Transition Systems - A Temporal Logic to Deal with Fairness.
Acta Informatica, 1983

Property Preserving Homomorphisms of Transition Systems.
Proceedings of the Logics of Programs, 1983

An Example of Specification and Verification in Cesar.
Proceedings of the Analysis of Concurrent Systems, 1983

1982
A Unified Approach for Studying the Properties of Transition Systems.
Theor. Comput. Sci., 1982

Global and Local Invariants in Transition Systems
Inf. Control., 1982

Specification and verification of concurrent systems in CESAR.
Proceedings of the International Symposium on Programming, 1982

Comments on Schiffers.
Proceedings of the Adequate Modeling of Systems, 1982

A Temporal Logic to Deal with Fairness in Transition Systems
Proceedings of the 23rd Annual Symposium on Foundations of Computer Science, 1982

1981
Iterative Methods for the Analysis of Petri Nets.
Proceedings of the Application and Theory of Petri Nets, 1981

1980
Deadlocks and Livelocks in Transition Systems.
Proceedings of the Mathematical Foundations of Computer Science 1980 (MFCS'80), 1980

1979
Le contrôle des systèmes asynchrones : concepts, propriétés, analyse statique. (The control of asynchronous systems: concepts, properties, static analysis).
PhD thesis, 1979

Use of Petri nets for performance evaluation.
Acta Cybern., 1979

Performance Evaluation of Systems Using Nets.
Proceedings of the Net Theory and Applications, 1979

Survey of French Research and Applications Based on Petri Nets.
Proceedings of the Net Theory and Applications, 1979

1978
Structural Properties of Petri Nets.
Proceedings of the Mathematical Foundations of Computer Science 1978, 1978

Synchronized Petri Nets: A Model for the Description of Non-Autonomous Systems.
Proceedings of the Mathematical Foundations of Computer Science 1978, 1978

1976
A Design Tool for the Multilevel Description and Simulation of Systems of Interconnected Modules.
Proceedings of the 3rd Annual Symposium on Computer Architecture, 1976

1974
Modèles temporels des systèmes logiques. (temporal Models of logic systems).
PhD thesis, 1974


  Loading...