Klaus Schneider

ACM Trans. Embed. Comput. Syst., September, 2023

Network-On-Chip Performance Evaluation by Synchronous Circuit Simulation.

[BibT_eX]

[DOI]

Leon Werner

Proceedings of the 16th International Workshop on Network on Chip Architectures, 2023

Towards a Basis for Endochronous Functions in Dataflow Process Networks.

[BibT_eX]

[DOI]

Daniel Theis

Proceedings of the 21st ACM-IEEE International Symposium on Formal Methods and Models for System Design, 2023

Allocation and Scheduling of Dataflow Graphs on Hybrid Dataflow/von Neumann Architectures.

[BibT_eX]

[DOI]

Nadine Kercher

Proceedings of the 21st ACM-IEEE International Symposium on Formal Methods and Models for System Design, 2023

Towards Buffers as a Scalable Alternative to Registers for Processor-Local Memory.

[BibT_eX]

[DOI]

Proceedings of the Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2023

Formal Methods-Based Optimization of Dataflow Models with Translation to Synchronous Models.

[BibT_eX]

[DOI]

Marcel Christian Werner

Proceedings of the Forum on Specification & Design Languages, 2023

Program Balancing in Compilation for Buffered Hybrid Dataflow Processors.

[BibT_eX]

[DOI]

Proceedings of the 47th IEEE Annual Computers, Software, and Applications Conference, 2023

2022

Synthesis of Parallel Software from Heterogeneous Dataflow Models.

[BibT_eX]

[DOI]

SN Comput. Sci., 2022

Buffer Allocation for Exposed Datapath Architectures.

[BibT_eX]

[DOI]

Proceedings of the 15th IEEE International Symposium on Embedded Multicore/Many-core Systems-on-Chip, 2022

Data-aware Global Scheduling of Dataflow Process Networks.

[BibT_eX]

[DOI]

Proceedings of the Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2022

Virtual Buffers for Exposed Datapath Architectures.

[BibT_eX]

[DOI]

Proceedings of the Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2022

Code generation criteria for buffered exposed datapath architectures from dataflow graphs.

[BibT_eX]

[DOI]

Proceedings of the LCTES '22: 23rd ACM SIGPLAN/SIGBED International Conference on Languages, 2022

From IEC 61131-3 Function Block Diagrams to Sequentially Constructive Statecharts.

[BibT_eX]

[DOI]

Marcel Christian Werner

Proceedings of the Forum on Specification & Design Languages, 2022

2021

Integrating Kahn Process Networks as a Model of Computation in an Extendable Model-based Design Framework.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Model-Driven Engineering and Software Development, 2021

Translation of continuous function charts to imperative synchronous quartz programs.

[BibT_eX]

[DOI]

Marcel Christian Werner

Proceedings of the MEMOCODE '21: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Virtual Event, China, November 20, 2021

Translating structured sequential programs to dataflow graphs.

[BibT_eX]

[DOI]

Proceedings of the MEMOCODE '21: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Virtual Event, China, November 20, 2021

Efficient Implementation of Heterogeneous Dataflow Models using Synchronous IO Patterns.

[BibT_eX]

[DOI]

Proceedings of the 24th Euromicro Conference on Digital System Design, 2021

A Model-based Design Flow for Asynchronous Implementations from Synchronous Specifications.

[BibT_eX]

[DOI]

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

Synthesis of Heterogeneous Dataflow Models from Synchronous Specifications.

[BibT_eX]

[DOI]

Proceedings of the IEEE 45th Annual Computers, Software, and Applications Conference, 2021

2020

Compiling synchronous languages to optimal move code for exposed datapath architectures.

[BibT_eX]

[DOI]

Marc Dahlem

Proceedings of the SCOPES '20: 23rd International Workshop on Software and Compilers for Embedded Systems, 2020

Employing OpenCL as a Standard Hardware Abstraction in a Distributed Embedded System: A Case Study.

[BibT_eX]

[DOI]

Proceedings of the 9th Mediterranean Conference on Embedded Computing, 2020

Properties of Invariants and Induction Lemmata.

[BibT_eX]

[DOI]

Martin Köhler

Felix Hasselwander

Proceedings of the 23rd GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2020

Area Estimation Framework for Digital Hardware Design using Machine Learning.

[BibT_eX]

[DOI]

Proceedings of the 23rd GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2020

SHeD: A Framework for Automatic Software Synthesis of Heterogeneous Dataflow Process Networks.

[BibT_eX]

[DOI]

Proceedings of the 23rd Euromicro Conference on Digital System Design, 2020

2019

Guest Editorial: Special Issue of ACM TECS on the ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017).

[BibT_eX]

[DOI]

Patricia Derler

Jean-Pierre Talpin

ACM Trans. Embed. Comput. Syst., 2019

Evaluating OpenCL as a Standard Hardware Abstraction for a Model-based Synthesis Framework: A Case Study.

[BibT_eX]

[DOI]

Proceedings of the 7th International Conference on Model-Driven Engineering and Software Development, 2019

Automatic Software Synthesis of Static and Dynamic Dataflow Process Networks.

[BibT_eX]

[DOI]

Proceedings of the Joint Proceedings of the Workshop on Model-Driven Engineering for the Internet of Things (MDE4IoT) & of the Workshop on Interplay of Model-Driven and Component-Based Software Engineering (ModComp) Co-located with the IEEE/ACM 22nd International Conference on Model Driven Engineering Languages and Systems (MODELS 2019), 2019

Inductive Proof Rules Beyond Safety Properties.

[BibT_eX]

[DOI]

Martin Köhler

Proceedings of the 22nd Workshop Methods and Description Languages for Modelling and Verification of Circuits and Systems, 2019

Flexible Data Flow Architecture for Embedded Hardware Accelerators.

[BibT_eX]

[DOI]

Proceedings of the Algorithms and Architectures for Parallel Processing, 2019

Generating Efficient Parallel Code from the RVC-CAL Dataflow Language.

[BibT_eX]

[DOI]

Florian Krebs

Proceedings of the 22nd Euromicro Conference on Digital System Design, 2019

A Formal Semantics of Exposed Datapath Architectures with Buffered Processing Units.

[BibT_eX]

[DOI]

Markus Anders

Proceedings of the 19th International Conference on Application of Concurrency to System Design, 2019

2018

Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP.

[BibT_eX]

[DOI]

Marc Dahlem

Theory Pract. Log. Program., 2018

The Half Cleaner Lemma: Constructing Efficient Interconnection Networks from Sorting Networks.

[BibT_eX]

[DOI]

Parallel Process. Lett., 2018

Using temporal logics for specifying weak memory consistency models.

[BibT_eX]

[DOI]

Int. J. Crit. Comput. Based Syst., 2018

Routing Partial Permutations in Interconnection Networks based on Radix Sorting.

[BibT_eX]

[DOI]

Proceedings of the 13th International Symposium on Reconfigurable Communication-centric Systems-on-Chip, 2018

Optimal Self-Routing Split Modules for Radix-based Interconnection Networks.

[BibT_eX]

[DOI]

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

Routing Partial Permutations in General Interconnection Networks based on Radix Sorting.

[BibT_eX]

[DOI]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2018

A Model-based Synthesis Framework for the Execution of Dynamic Dataflow Actors.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Internet of Things, 2018

Are Synchronous Programs Logic Programs?

[BibT_eX]

[DOI]

Marc Dahlem

Proceedings of the Principled Software Development, 2018

Operational Characterization of Weak Memory Consistency Models.

[BibT_eX]

[DOI]

Proceedings of the Architecture of Computing Systems - ARCS 2018, 2018

On Memory Optimal Code Generation for Exposed Datapath Architectures with Buffered Processing Units.

[BibT_eX]

[DOI]

Markus Anders

Proceedings of the 18th International Conference on Application of Concurrency to System Design, 2018

2017

Quartz: A Synchronous Language for Model-Based Design of Reactive Embedded Systems.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Hardware/Software Codesign., 2017

Exploring different execution paradigms in exposed datapath architectures with buffered processing units.

[BibT_eX]

[DOI]

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

Deriving concentrators from binary sorters using half cleaners.

[BibT_eX]

[DOI]

Ankesh Jain

Proceedings of the International Conference on ReConFigurable Computing and FPGAs, 2017

An Efficient Self-Routing and Non-Blocking Interconnection Network on Chip.

[BibT_eX]

[DOI]

Ankesh Jain

Proceedings of the 10th International Workshop on Network on Chip Architectures, 2017

Automatic Synthesis of Optimal-Size Concentrators by Answer Set Programming.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2017

Out-of-Order Execution of Buffered Function Units in Exposed Data Path Architectures.

[BibT_eX]

[DOI]

Frederik Walk

Proceedings of the 2017 IEEE International Parallel and Distributed Processing Symposium Workshops, 2017

Exploring the Potential of Instruction-Level Parallelism of Exposed Datapath Architectures with Buffered Processing Units.

[BibT_eX]

[DOI]

Proceedings of the 17th International Conference on Application of Concurrency to System Design, 2017

2016

Semantics in space systems architectures.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2016

Specifying Weak Memory Consistency with Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the 10th Workshop on Verification and Evaluation of Computer and Communication System, 2016

Towards the standardization of plug-and-play devices for model-based designs of embedded systems.

[BibT_eX]

[DOI]

Proceedings of the 11th IEEE Symposium on Industrial Embedded Systems, 2016

Introducing MoC Drivers for the Integration of Sensor-Actuator Behaviors in Model-Based Design Flows of Embedded Systems.

[BibT_eX]

[DOI]

Proceedings of the 19th International Workshop on Software and Compilers for Embedded Systems, 2016

The selector-tree network: A new self-routing and non-blocking interconnection network.

[BibT_eX]

[DOI]

Proceedings of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip, 2016

Control-flow guided property directed reachability for imperative synchronous programs.

[BibT_eX]

[DOI]

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

Verifying the concentration property of permutation networks by BDDs.

[BibT_eX]

[DOI]

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

Optimal compilation for exposed datapath architectures with buffered processing units by SAT solvers.

[BibT_eX]

[DOI]

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

Verification of Behavior-Based Control Systems in their Physical Environment.

[BibT_eX]

[DOI]

Proceedings of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2016

Towards Code Generation for the Synchronous Control Asynchronous Dataflow (SCAD) Architectures.

[BibT_eX]

[DOI]

Proceedings of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2016

Control-flow guided clause generation for property directed reachability.

[BibT_eX]

[DOI]

Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2016

2015

Memory-Model-Aware Testing: A Unified Complexity Analysis.

[BibT_eX]

[DOI]

Florian Furbach

Roland Meyer

ACM Trans. Embed. Comput. Syst., 2015

Evaluation of Speculation in Out-of-Order Execution of Synchronous Dataflow Networks.

[BibT_eX]

[DOI]

Int. J. Parallel Program., 2015

An SMT-based Approach to analyze Non-Linear Relations of Parameters for Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling and Verification of Cyber-Physical Systems, 2015

A Time-Predictable Model of Computation.

[BibT_eX]

[DOI]

Proceedings of the 2015 IEEE Real-Time Systems Symposium, 2015

Verification condition generation for hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2015

A Counterexample-Guided Approach to Symbolic Simulation of Hybrid Systems.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2015

2014

Passive code in synchronous programs.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2014

Constructive polychronous systems.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2014

Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions.

[BibT_eX]

[DOI]

Des. Autom. Embed. Syst., 2014

High level modeling of elastic circuits in SystemC.

[BibT_eX]

[DOI]

Mohamed Ammar Ben Khadra

Proceedings of the 2014 Spring Simulation Multiconference, 2014

Integrating UML Composite Structures and fUML.

[BibT_eX]

[DOI]

Proceedings of the SOFSEM 2014: Theory and Practice of Computer Science, 2014

Reducing the Communication of Message-Passing Systems Synthesized from Synchronous Programs.

[BibT_eX]

[DOI]

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

Using the Base Semantics given by fUML for Verification.

[BibT_eX]

[DOI]

Proceedings of the MODELSWARD 2014 - Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development, Lisbon, Portugal, 7, 2014

From clock-driven to data-driven models.

[BibT_eX]

[DOI]

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

Synthesis of Distributed Synchronous Specifications to SysteMoC.

[BibT_eX]

Mohamed Ammar Ben Khadra

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2014

Using Different Representations of Synchronous Systems in SAL.

[BibT_eX]

Felipe Bichued

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2014

A New Algorithm for Carry-Free Addition of Binary Signed-Digit Numbers.

[BibT_eX]

[DOI]

Proceedings of the 22nd IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, 2014

Abacus: A Processor Family for Education.

[BibT_eX]

[DOI]

Nikita Bhardwaj

Proceedings of the Workshop on Embedded and Cyber-Physical Systems Education, 2014

Isochronous networks by construction.

[BibT_eX]

[DOI]

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

2013

Embedding Polychrony into Synchrony.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2013

Clock refinement in imperative synchronous languages.

[BibT_eX]

[DOI]

Mike Gemünde

EURASIP J. Embed. Syst., 2013

Synchronous Programming (Dagstuhl Seminar 13471).

[BibT_eX]

[DOI]

Stephen A. Edwards

Alain Girault

Dagstuhl Reports, 2013

Lifting Verification Results for Preemption Statements.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 11th International Conference, 2013

Generating hardware specific code at different abstraction levels using Averest.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Software and Compilers for Embedded Systems, 2013

Targeting different abstraction layers by model-based design methods for embedded systems: A case study.

[BibT_eX]

[DOI]

Proceedings of the 2013 IEEE 19th International Conference on Embedded and Real-Time Computing Systems and Applications, 2013

Translating synchronous guarded actions to interleaved guarded actions.

[BibT_eX]

[DOI]

Proceedings of the 11th ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2013

An Interactive Verification Tool for Synchronous/Reactive Systems.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2013

Solving Games Using Incremental Induction.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 10th International Conference, 2013

Towards the Applicability of Alf to Model Cyber-Physical Systems.

[BibT_eX]

[DOI]

Proceedings of the 2013 Federated Conference on Computer Science and Information Systems, 2013

Interactive Verification of Cyber-physical Systems: Interfacing Averest and KeYmaera.

[BibT_eX]

[DOI]

Proceedings of the 2013 Federated Conference on Computer Science and Information Systems, 2013

Automatic Hard Block Inference on FPGAs.

[BibT_eX]

[DOI]

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

Modular Verification of Synchronous Programs.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Application of Concurrency to System Design, 2013

2012

Out-Of-order execution of synchronous data-flow networks.

[BibT_eX]

[DOI]

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

A hoare calculus for the verification of synchronous languages.

[BibT_eX]

[DOI]

Proceedings of the sixth workshop on Programming Languages meets Program Verification, 2012

Interactive verification of synchronous systems.

[BibT_eX]

[DOI]

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

Preservation of LTL properties in desynchronized systems.

[BibT_eX]

[DOI]

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

An Asymptotically Correct Finite Path Semantics for LTL.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Efficient Handling of Arrays in Dataflow Process Networks.

[BibT_eX]

[DOI]

Proceedings of the 14th IEEE International Conference on High Performance Computing and Communication & 9th IEEE International Conference on Embedded Software and Systems, 2012

Monitoring distributed reactive systems.

[BibT_eX]

[DOI]

Proceedings of the 2012 IEEE International High Level Design Validation and Test Workshop, 2012

Teaching cyber-physical systems: a programming approach.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Embedded and Cyber-Physical Systems Education, 2012

2011

A uniform approach to three-valued semantics for <i>μ</i>-calculus on abstractions of hybrid automata.

[BibT_eX]

[DOI]

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

A LTL Fragment for GR(1)-Synthesis

[BibT_eX]

[DOI]

Proceedings of the Proceedings International Workshop on Interactions, Games and Protocols, 2011

Program Sketching via CTL* Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2011

SMT-based optimization for synchronous programs.

[BibT_eX]

[DOI]

Proceedings of the 14th International Workshop on Software and Compilers for Embedded Systems, 2011

Translating Synchronous Systems to Data-Flow Process Networks.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Parallel and Distributed Computing, 2011

Synthesis of Parallel Sorting Networks using SAT Solvers.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2011

Round Trip to Asynchrony and Synchrony.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2011

Safe Automotive Software.

[BibT_eX]

[DOI]

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

Welcome to ICCD 2011!

[BibT_eX]

[DOI]

Proceedings of the IEEE 29th International Conference on Computer Design, 2011

Causality analysis of synchronous programs with refined clocks.

[BibT_eX]

[DOI]

Mike Gemünde

Proceedings of the 2011 IEEE International High Level Design Validation and Test Workshop, 2011

Schizophrenia and causality in the context of refined clocks.

[BibT_eX]

[DOI]

Proceedings of the 2011 Forum on Specification & Design Languages, 2011

Integrating system descriptions by clocked guarded actions.

[BibT_eX]

[DOI]

Proceedings of the 2011 Forum on Specification & Design Languages, 2011

Data-Flow Analysis of Extended Finite State Machines.

[BibT_eX]

[DOI]

Proceedings of the 11th International Conference on Application of Concurrency to System Design, 2011

2010

Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis

[BibT_eX]

[DOI]

Proceedings of the Proceedings First Symposium on Games, 2010

Message from the chairs.

[BibT_eX]

[DOI]

Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

Compilation of imperative synchronous programs with refined clocks.

[BibT_eX]

[DOI]

Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

From Synchronous Guarded Actions to SystemC.

[BibT_eX]

Mike Gemünde

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2010

Multithreaded Code from Synchronous Programs: Generating Software Pipelines for OpenMP.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2010

Translating concurrent action oriented specifications to synchronous guarded actions.

[BibT_eX]

[DOI]

Sandeep K. Shukla

Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, 2010

Dependency-Driven Distribution of Synchronous Programs.

[BibT_eX]

[DOI]

Proceedings of the Distributed, Parallel and Biologically Inspired Systems, 2010

From synchronous programs to symbolic representations of hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, 2010

Multithreaded code from synchronous programs: Extracting independent threads for OpenMP.

[BibT_eX]

[DOI]

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

A Formal Semantics of Clock Refinement in Imperative Synchronous Languages.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Application of Concurrency to System Design, 2010

The Model Checking View to Clock Gating and Operand Isolation.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Application of Concurrency to System Design, 2010

Predicting Events for the Simulation of Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the 10th IEEE International Conference on Computer and Information Technology, 2010

2009

Property Driven Three-Valued Model Checking on Hybrid Automata.

[BibT_eX]

[DOI]

Proceedings of the Logic, 2009

Separate compilation for synchronous programs.

[BibT_eX]

[DOI]

Proceedings of the 12th International Workshop on Software and Compilers for Embedded Systems, 2009

Static data-flow analysis of synchronous programs.

[BibT_eX]

[DOI]

Proceedings of the 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 2009

Using IP Cores in Synchronous Languages.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2009

Separate compilation and execution of imperative synchronous modules.

[BibT_eX]

[DOI]

Eric Vecchié

Jean-Pierre Talpin

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

09481 Abstracts Collection - SYNCHRON 2009.

[BibT_eX]

[DOI]

Reinhard von Hanxleden

Proceedings of the SYNCHRON 2009, 22.11. - 27.11.2009, 2009

Online Exercise System - A Web-based Tool for Administration and Automatic Correction of Exercises.

[BibT_eX]

Proceedings of the CSEDU 2009 - Proceedings of the First International Conference on Computer Supported Education, Lisboa, Portugal, March 23-26, 2009, 2009

Desynchronizing Synchronous Programs by Modes.

[BibT_eX]

[DOI]

Proceedings of the Ninth International Conference on Application of Concurrency to System Design, 2009

2008

Approximated Reachability on Hybrid Automata: Falsification meets Certification.

[BibT_eX]

[DOI]

Proceedings of the Second Workshop on Reachability Problems in Computational Models, 2008

From LTL to Symbolically Represented Deterministic Automata.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2008

Formal Reasoning About Causality Analysis.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Generating Deterministic $\omega$-Automata for most LTL Formulas by the Breakpoint Construction.

[BibT_eX]

Sven Lamberti

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2008

Hardware Acceleration for Model Checking.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2008

A Uniform Approach to Three-Valued Semantics for µ-Calculus on Abstractions of Hybrid Automata.

[BibT_eX]

[DOI]

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

Performing causality analysis by bounded model checking.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Application of Concurrency to System Design (ACSD 2008), 2008

2007

Bounded model checking of infinite state systems.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2007

Preface.

[BibT_eX]

[DOI]

Arnd Poetzsch-Heffter

Proceedings of the First Workshop on Verification of Adaptive Systems, 2007

Combining Interval Arithmetic and Three-Valued Temporal Logics for the Verification of Analog Systems.

[BibT_eX]

Alexander Dreyer

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2007

Successive Abstractions of Hybrid Automata for Monotonic CTL Model Checking.

[BibT_eX]

[DOI]

Bud Mishra

Proceedings of the Logical Foundations of Computer Science, International Symposium, 2007

Formal verification of safety behaviours of the outdoor robot ravon.

[BibT_eX]

Proceedings of the ICINCO 2007, 2007

Three-valued automated reasoning on analog properties.

[BibT_eX]

[DOI]

Alexander Dreyer

Proceedings of the 17th ACM Great Lakes Symposium on VLSI 2007, 2007

How Different are Esterel and SystemC?.

[BibT_eX]

Proceedings of the Forum on specification and Design Languages, 2007

2006

Efficient Map Overlay for Safety-Critical Embedded Systems.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Industrial Embedded Systems, 2006

Efficient code generation from synchronous programs.

[BibT_eX]

[DOI]

Eric Vecchié

Proceedings of the 4th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2006), 2006

A Framework for Verifying and Implementing Embedded Systems.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2006

Modular Compilation of Synchronous Programs.

[BibT_eX]

[DOI]

Eric Vecchié

Proceedings of the From Model-Driven Design to Resource Management for Distributed Embedded Systems, 2006

Verifying the adaptation behavior of embedded systems.

[BibT_eX]

[DOI]

Mario Trapp

Proceedings of the 2006 international workshop on Self-adaptation and self-managing systems, 2006

Model Checking PSL Using HOL and SMV.

[BibT_eX]

[DOI]

Thomas Tuerk

Mike Gordon

Proceedings of the Hardware and Software, 2006

Verification of Data Paths Using Unbounded Integers: Automata Strike Back.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software, 2006

System Description Aspects as Syntactic Sugar.

[BibT_eX]

[DOI]

Proceedings of the Forum on specification and Design Languages, 2006

2005

Combining supervisor synthesis and model checking.

[BibT_eX]

[DOI]

Roberto Ziller

ACM Trans. Embed. Comput. Syst., 2005

From PSL to LTL: A Formal Validation in HOL.

[BibT_eX]

[DOI]

Thomas Tuerk

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Three-valued logic in bounded model checking.

[BibT_eX]

[DOI]

Proceedings of the 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), 2005

Synthesizing deterministic controllers in supervisory control.

[BibT_eX]

Proceedings of the ICINCO 2005, 2005

Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2005

A unified model checking framework for the supervisor synthesis problem.

[BibT_eX]

Proceedings of the 1st Workshop on Games for Logic and Programming Languages, 2005

Dependable Polygon-Processing Algorithms for Safety-Critical Embedded Systems.

[BibT_eX]

[DOI]

Proceedings of the Embedded and Ubiquitous Computing, 2005

Using Model Checking to Solve Supervisor Synthesis Problems.

[BibT_eX]

[DOI]

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

Maximal Causality Analysis.

[BibT_eX]

[DOI]

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

2004

Verification of Reactive Systems - Formal Methods and Algorithms

[BibT_eX]

[DOI]

Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-662-10778-2, 2004

A Verified Compiler for Synchronous Programs with Local Declarations.

[BibT_eX]

[DOI]

Proceedings of the Third International Workshop on Synchronous Languages, 2004

Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

Bounded model checking of infinite state systems: exploiting the automata hierarchy.

[BibT_eX]

[DOI]

Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004

Global vs. Local Model Checking of Infinite State Systems.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2004

Abstraction of assembler programs for symbolic worst case execution time analysis.

[BibT_eX]

[DOI]

Proceedings of the 41th Design Automation Conference, 2004

Causality analysis of synchronous programs with delayed actions.

[BibT_eX]

[DOI]

Proceedings of the 2004 International Conference on Compilers, 2004

2003

Runtime Analysis of Synchronous Programs for Low-Level Real-Time Verification.

[BibT_eX]

[DOI]

C. Metzler

Proceedings of the 16th Annual Symposium on Integrated Circuits and Systems Design, 2003

Generating Formal Models for Real-Time Verification by Exact Low-Level Runtime Analysis of Synchronous Programs.

[BibT_eX]

[DOI]

C. Metzler

Proceedings of the 24th IEEE Real-Time Systems Symposium (RTSS 2003), 2003

A Generalised Approach to Supervisor Synthesis.

[BibT_eX]

[DOI]

Roberto Ziller

Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003

Exact Runtime Analysis Using Automata-Based Symbolic Simulation.

[BibT_eX]

[DOI]

Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003

A μ-Calculus Approach to Supervisor Synthesis.

[BibT_eX]

Roberto Ziller

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2003

Exact Low-Level Runtime Analysis of Synchronous Programs for Formal Verification of Real-Time Systems.

[BibT_eX]

[DOI]

C. Metzler

Proceedings of the Forum on specification and Design Languages, 2003

Exact High Level WCET Analysis of Synchronous Programs by Symbolic State Space Exploration.

[BibT_eX]

[DOI]

Proceedings of the 2003 Design, 2003

2002

The BDD Space Complexity of Different Forms of Concurrency.

[BibT_eX]

[DOI]

Michael Baldamus

Fundam. Informaticae, 2002

Proving the Equivalence of Microstep and Macrostep Semantics.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Symbolic Model Checking by Automata Based Set Representation.

[BibT_eX]

Tobias Schuele

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2002

Extending Synchronous Languages for Generating Abstract Real-Time Models.

[BibT_eX]

[DOI]

Proceedings of the 2002 Design, 2002

2001

Symbolic Model Checking of Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the Eigth International Symposium on Temporal Representation and Reasoning, 2001

Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2001

A New Approach to the Specification and Verification of Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the 13th Euromicro Conference on Real-Time Systems (ECRTS 2001), 2001

Embedding Imperative Synchronous Languages in Interactive Theorem Provers.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Conference on Application of Concurrency to System Design (ACSD 2001), 2001

2000

Can American Checkers be Solved by Means of Symbolic Model Checking?

[BibT_eX]

[DOI]

Proceedings of the Formal Methods Elsewhere, 2000

A Verified Hardware Synthesis of Esterel Programs.

[BibT_eX]

Proceedings of the Architecture and Design of Distributed Embedded Systems, 2000

Abstraction from Counters: An Application on Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the 2000 Design, 2000

1999

Formale Verifikation eingebetteter Systeme.

[BibT_eX]

[DOI]

Informationstechnik Tech. Inform., 1999

A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata.

[BibT_eX]

[DOI]

Dirk W. Hoffmann

Proceedings of the Theorem Proving in Higher Order Logics, 12th International Conference, 1999

Abstraction of Systems with Counters for Symbolic Model Checking.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 1999

Translating a Visual Description Technique to a Synchronous Language: From DiChartsto PURR.

[BibT_eX]

Thomas Stauner

Michaela Huhn

Proceedings of the Formale Beschreibungstechniken für verteilte Systeme, 1999

Introducing Mutual Exclusion in Esterel.

[BibT_eX]

[DOI]

Viktor K. Sabelfeld

Proceedings of the Perspectives of System Informatics, 1999

Verifying Imprecisely Working Arithmetic Circuits.

[BibT_eX]

[DOI]

Proceedings of the 1999 Design, 1999

Validation of Object-Oriented Concurrent Designs by Model Checking.

[BibT_eX]

[DOI]

Michaela Huhn

Proceedings of the Correct Hardware Design and Verification Methods, 1999

Yet another Look at the LTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1999

1998

Kontrollfluss-Verifikation von Algorithmen mittels Modellprüfung.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 1998

A Synchronous Language for Modeling and Verifying Real Time and Embedded Systems.

[BibT_eX]

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 1998

Modeling and Verifying Abstract Multithreaded Systems.

[BibT_eX]

Winfried Grünewald

Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 1998

Comparing Model Checking and Term Rewriting for the Verification of an Embedded System.

[BibT_eX]

Michaela Huhn

Proceedings of the Distributed and Parallel Embedded Systems, 1998

Model Checking on Product Structures.

[BibT_eX]

[DOI]

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

Formal Specification in VHDL for Hardware Verification.

[BibT_eX]

[DOI]

Ralf Reetz

Proceedings of the 1998 Design, 1998

1997

The C@S System.

[BibT_eX]

[DOI]

Proceedings of the Formal Hardware Verification - Methods and Systems in Comparison, 1997

1996

A Unified Approach for Combining Different Formalisms for Hardware Verification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Ein einheitlicher Ansatz zur Unterstützung von Abstraktionsmechanismen der Hardware-Verifikation.

[BibT_eX]

[DOI]

DISKI 116, Infix, ISBN: 978-3-89601-116-9, 1996

1995

Formal synthesis of circuits with a simple handshake protocol.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on VLSI Design (VLSI Design 1995), 1995

1994

Accelerating Tableaux Proofs Using Compact Representations.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1994

Automating Verification by Functional Abstraction at the System Level.

[BibT_eX]

[DOI]

Proceedings of the Higher Order Logic Theorem Proving and Its Applications, 1994

A Formal Framework for High Level Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Theorem Provers in Circuit Design, 1994

Control Path Oriented Verification of Sequential Generic Circuits with Control and Data Path.

[BibT_eX]

[DOI]

Proceedings of the EDAC - The European Conference on Design Automation, ETC - European Test Conference, EUROASIC - The European Event in ASIC Design, Proceedings, February 28, 1994

1993

Structuring and Automating Hardware Proofs in a Higher-Order Theorem-Proving Environment.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1993

Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification.

[BibT_eX]

[DOI]

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

A Functional Approach for Formalizing Regular Hardware Structures.

[BibT_eX]

[DOI]

Dirk Eisenbiegler

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

Hardware-Verification using First Order BDDs.

[BibT_eX]

Proceedings of the Computer Hardware Description Languages and their Applications, Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications, 1993

Embedding Hardware Verification Within a Commercial Design Framework.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1993

1992

Modelling Generic Hardware Structures by Abstract Datatypes.

[BibT_eX]