# Klaus Schneider

According to our database1, Klaus Schneider authored at least 196 papers between 1981 and 2019.

Collaborative distances:

Book
In proceedings
Article
PhD thesis
Other

## Bibliography

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

Evaluating OpenCL as a Standard Hardware Abstraction for a Model-based Synthesis Framework: A Case Study.
Proceedings of the 7th International Conference on Model-Driven Engineering and Software Development, 2019

Automatic Software Synthesis of Static and Dynamic Dataflow Process Networks.
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

Generating Efficient Parallel Code from the RVC-CAL Dataflow Language.
Proceedings of the 22nd Euromicro Conference on Digital System Design, 2019

A Formal Semantics of Exposed Datapath Architectures with Buffered Processing Units.
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.
TPLP, 2018

The Half Cleaner Lemma: Constructing Efficient Interconnection Networks from Sorting Networks.
Parallel Processing Letters, 2018

Using temporal logics for specifying weak memory consistency models.
IJCCBS, 2018

Routing Partial Permutations in Interconnection Networks based on Radix Sorting.
Proceedings of the 13th International Symposium on Reconfigurable Communication-centric Systems-on-Chip, 2018

Optimal Self-Routing Split Modules for Radix-based Interconnection Networks.
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.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2018

Are Synchronous Programs Logic Programs?
Proceedings of the Principled Software Development, 2018

Operational Characterization of Weak Memory Consistency Models.
Proceedings of the Architecture of Computing Systems - ARCS 2018, 2018

On Memory Optimal Code Generation for Exposed Datapath Architectures with Buffered Processing Units.
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.
Proceedings of the Handbook of Hardware/Software Codesign., 2017

Exploring different execution paradigms in exposed datapath architectures with buffered processing units.
Proceedings of the 2017 International Conference on Embedded Computer Systems: Architectures, 2017

Deriving concentrators from binary sorters using half cleaners.
Proceedings of the International Conference on ReConFigurable Computing and FPGAs, 2017

An Efficient Self-Routing and Non-Blocking Interconnection Network on Chip.
Proceedings of the 10th International Workshop on Network on Chip Architectures, 2017

Automatic Synthesis of Optimal-Size Concentrators by Answer Set Programming.
Proceedings of the Logic Programming and Nonmonotonic Reasoning, 2017

Out-of-Order Execution of Buffered Function Units in Exposed Data Path Architectures.
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.
Proceedings of the 17th International Conference on Application of Concurrency to System Design, 2017

2016
Semantics in space systems architectures.
ISSE, 2016

Specifying Weak Memory Consistency with Temporal Logic.
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.
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.
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.
Proceedings of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip, 2016

Control-flow guided property directed reachability for imperative synchronous programs.
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.
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.
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.
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.
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.
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2016

2015
Memory-Model-Aware Testing: A Unified Complexity Analysis.
ACM Trans. Embedded Comput. Syst., 2015

Evaluation of Speculation in Out-of-Order Execution of Synchronous Dataflow Networks.
International Journal of Parallel Programming, 2015

An SMT-based Approach to analyze Non-Linear Relations of Parameters for Hybrid Systems.
Proceedings of the Formal Modeling and Verification of Cyber-Physical Systems, 2015

A Time-Predictable Model of Computation.
Proceedings of the 2015 IEEE Real-Time Systems Symposium, 2015

Verification condition generation for hybrid systems.
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.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2015

2014
Passive code in synchronous programs.
ACM Trans. Embedded Comput. Syst., 2014

Constructive polychronous systems.
Sci. Comput. Program., 2014

Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions.
Design Autom. for Emb. Sys., 2014

High level modeling of elastic circuits in SystemC.
Proceedings of the 2014 Spring Simulation Multiconference, 2014

Integrating UML Composite Structures and fUML.
Proceedings of the SOFSEM 2014: Theory and Practice of Computer Science, 2014

Reducing the Communication of Message-Passing Systems Synthesized from Synchronous Programs.
Proceedings of the 22nd Euromicro International Conference on Parallel, 2014

Using the Base Semantics given by fUML for Verification.
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.
Proceedings of the Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2014

Synthesis of Distributed Synchronous Specifications to SysteMoC.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2014

Using Different Representations of Synchronous Systems in SAL.
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.
Proceedings of the 22nd IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, 2014

Abacus: A Processor Family for Education.
Proceedings of the Workshop on Embedded and Cyber-Physical Systems Education, 2014

Isochronous networks by construction.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2014

2013
Embedding Polychrony into Synchrony.
IEEE Trans. Software Eng., 2013

Clock refinement in imperative synchronous languages.
EURASIP J. Emb. Sys., 2013

Synchronous Programming (Dagstuhl Seminar 13471).
Dagstuhl Reports, 2013

Lifting Verification Results for Preemption Statements.
Proceedings of the Software Engineering and Formal Methods - 11th International Conference, 2013

Generating hardware specific code at different abstraction levels using Averest.
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.
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.
Proceedings of the 11th ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2013

An Interactive Verification Tool for Synchronous/Reactive Systems.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2013

Solving Games Using Incremental Induction.
Proceedings of the Integrated Formal Methods, 10th International Conference, 2013

Towards the Applicability of Alf to Model Cyber-Physical Systems.
Proceedings of the 2013 Federated Conference on Computer Science and Information Systems, 2013

Interactive Verification of Cyber-physical Systems: Interfacing Averest and KeYmaera.
Proceedings of the 2013 Federated Conference on Computer Science and Information Systems, 2013

Automatic Hard Block Inference on FPGAs.
Proceedings of the 2013 Euromicro Conference on Digital System Design, 2013

Modular Verification of Synchronous Programs.
Proceedings of the 13th International Conference on Application of Concurrency to System Design, 2013

2012
Out-Of-order execution of synchronous data-flow networks.
Proceedings of the 2012 International Conference on Embedded Computer Systems: Architectures, 2012

A hoare calculus for the verification of synchronous languages.
Proceedings of the sixth workshop on Programming Languages meets Program Verification, 2012

Interactive verification of synchronous systems.
Proceedings of the Tenth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2012

Preservation of LTL properties in desynchronized systems.
Proceedings of the Tenth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2012

An Asymptotically Correct Finite Path Semantics for LTL.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Efficient Handling of Arrays in Dataflow Process Networks.
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.
Proceedings of the 2012 IEEE International High Level Design Validation and Test Workshop, 2012

Teaching cyber-physical systems: a programming approach.
Proceedings of the Workshop on Embedded and Cyber-Physical Systems Education, 2012

2011
A uniform approach to three-valued semantics for μ-calculus on abstractions of hybrid automata.
STTT, 2011

A LTL Fragment for GR(1)-Synthesis
Proceedings of the Proceedings International Workshop on Interactions, Games and Protocols, 2011

Program Sketching via CTL* Model Checking.
Proceedings of the Model Checking Software, 2011

SMT-based optimization for synchronous programs.
Proceedings of the 14th International Workshop on Software and Compilers for Embedded Systems, 2011

Translating Synchronous Systems to Data-Flow Process Networks.
Proceedings of the 12th International Conference on Parallel and Distributed Computing, 2011

Synthesis of Parallel Sorting Networks using SAT Solvers.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2011

Round Trip to Asynchrony and Synchrony.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2011

Safe Automotive Software.
Proceedings of the Knowledge-Based and Intelligent Information and Engineering Systems, 2011

Welcome to ICCD 2011!
Proceedings of the IEEE 29th International Conference on Computer Design, 2011

Causality analysis of synchronous programs with refined clocks.
Proceedings of the 2011 IEEE International High Level Design Validation and Test Workshop, 2011

Schizophrenia and causality in the context of refined clocks.
Proceedings of the 2011 Forum on Specification & Design Languages, 2011

Integrating system descriptions by clocked guarded actions.
Proceedings of the 2011 Forum on Specification & Design Languages, 2011

Data-Flow Analysis of Extended Finite State Machines.
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
Proceedings of the Proceedings First Symposium on Games, 2010

Message from the chairs.
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.
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

From Synchronous Guarded Actions to SystemC.
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.
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.
Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, 2010

Dependency-Driven Distribution of Synchronous Programs.
Proceedings of the Distributed, Parallel and Biologically Inspired Systems, 2010

From synchronous programs to symbolic representations of hybrid systems.
Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, 2010

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

A Formal Semantics of Clock Refinement in Imperative Synchronous Languages.
Proceedings of the 10th International Conference on Application of Concurrency to System Design, 2010

The Model Checking View to Clock Gating and Operand Isolation.
Proceedings of the 10th International Conference on Application of Concurrency to System Design, 2010

Predicting Events for the Simulation of Hybrid Systems.
Proceedings of the 10th IEEE International Conference on Computer and Information Technology, 2010

2009
Property Driven Three-Valued Model Checking on Hybrid Automata.
Proceedings of the Logic, 2009

Separate compilation for synchronous programs.
Proceedings of the 12th International Workshop on Software and Compilers for Embedded Systems, 2009

Static data-flow analysis of synchronous programs.
Proceedings of the 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 2009

Using IP Cores in Synchronous Languages.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2009

Separate compilation and execution of imperative synchronous modules.
Proceedings of the Design, Automation and Test in Europe, 2009

09481 Abstracts Collection - SYNCHRON 2009.
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.
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.
Proceedings of the Ninth International Conference on Application of Concurrency to System Design, 2009

2008
Preface.
Electr. Notes Theor. Comput. Sci., 2008

Approximated Reachability on Hybrid Automata: Falsification meets Certification.
Electr. Notes Theor. Comput. Sci., 2008

From LTL to Symbolically Represented Deterministic Automata.
Proceedings of the Verification, 2008

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.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2008

Hardware Acceleration for Model Checking.
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.
Proceedings of the Hardware and Software: Verification and Testing, 2008

Performing causality analysis by bounded model checking.
Proceedings of the 8th International Conference on Application of Concurrency to System Design (ACSD 2008), 2008

2007
Bounded model checking of infinite state systems.
Formal Methods in System Design, 2007

Combining Interval Arithmetic and Three-Valued Temporal Logics for the Verification of Analog Systems.
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.
Proceedings of the Logical Foundations of Computer Science, International Symposium, 2007

Formal verification of safety behaviours of the outdoor robot ravon.
Proceedings of the ICINCO 2007, 2007

Three-valued automated reasoning on analog properties.
Proceedings of the 17th ACM Great Lakes Symposium on VLSI 2007, 2007

How Different are Esterel and SystemC?.
Proceedings of the Forum on specification and Design Languages, 2007

2006
A Verified Compiler for Synchronous Programs with Local Declarations.
Electr. Notes Theor. Comput. Sci., 2006

Efficient Map Overlay for Safety-Critical Embedded Systems.
Proceedings of the International Symposium on Industrial Embedded Systems, 2006

Efficient code generation from synchronous programs.
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.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2006

Modular Compilation of Synchronous Programs.
Proceedings of the From Model-Driven Design to Resource Management for Distributed Embedded Systems, 2006

Verifying the adaptation behavior of embedded systems.
Proceedings of the 2006 international workshop on Self-adaptation and self-managing systems, 2006

Model Checking PSL Using HOL and SMV.
Proceedings of the Hardware and Software, 2006

Verification of Data Paths Using Unbounded Integers: Automata Strike Back.
Proceedings of the Hardware and Software, 2006

System Description Aspects as Syntactic Sugar.
Proceedings of the Forum on specification and Design Languages, 2006

2005
Combining supervisor synthesis and model checking.
ACM Trans. Embedded Comput. Syst., 2005

From PSL to LTL: A Formal Validation in HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Three-valued logic in bounded model checking.
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.
Proceedings of the ICINCO 2005, 2005

Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry.
Proceedings of the Formal Methods and Software Engineering, 2005

A unified model checking framework for the supervisor synthesis problem.
Proceedings of the Games for Logic and Programming Languages (GALOP 2005), 2005

Dependable Polygon-Processing Algorithms for Safety-Critical Embedded Systems.
Proceedings of the Embedded and Ubiquitous Computing, 2005

Maximal Causality Analysis.
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
Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-662-10778-2, 2004

Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems.
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.
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.
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.
Proceedings of the 41th Design Automation Conference, 2004

Causality analysis of synchronous programs with delayed actions.
Proceedings of the 2004 International Conference on Compilers, 2004

2003
Runtime Analysis of Synchronous Programs for Low-Level Real-Time Verification.
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.
Proceedings of the 24th IEEE Real-Time Systems Symposium (RTSS 2003), 2003

A Generalised Approach to Supervisor Synthesis.
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.
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.
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.
Proceedings of the Forum on specification and Design Languages, 2003

Exact High Level WCET Analysis of Synchronous Programs by Symbolic State Space Exploration.
Proceedings of the 2003 Design, 2003

2002
The BDD Space Complexity of Different Forms of Concurrency.
Fundam. Inform., 2002

Proving the Equivalence of Microstep and Macrostep Semantics.
Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Symbolic Model Checking by Automata Based Set Representation.
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.
Proceedings of the 2002 Design, 2002

2001
Can American Checkers be Solved by Means of Symbolic Model Checking?
Electr. Notes Theor. Comput. Sci., 2001

Symbolic Model Checking of Real-Time Systems.
Proceedings of the Eigth International Symposium on Temporal Representation and Reasoning, 2001

Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy.
Proceedings of the Logic for Programming, 2001

A New Approach to the Specification and Verification of Real-Time Systems.
Proceedings of the 13th Euromicro Conference on Real-Time Systems (ECRTS 2001), 2001

Embedding Imperative Synchronous Languages in Interactive Theorem Provers.
Proceedings of the 2nd International Conference on Application of Concurrency to System Design (ACSD 2001), 2001

2000
A Verified Hardware Synthesis of Esterel Programs.
Proceedings of the Architecture and Design of Distributed Embedded Systems, 2000

Abstraction from Counters: An Application on Real-Time Systems.
Proceedings of the 2000 Design, 2000

1999
Formale Verifikation eingebetteter Systeme.
it+ti - Informationstechnik und Technische Informatik, 1999

A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata.
Proceedings of the Theorem Proving in Higher Order Logics, 12th International Conference, 1999

Abstraction of Systems with Counters for Symbolic Model Checking.
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.
Proceedings of the Formale Beschreibungstechniken für verteilte Systeme, 1999

Introducing Mutual Exclusion in Esterel.
Proceedings of the Perspectives of System Informatics, 1999

Verifying Imprecisely Working Arithmetic Circuits.
Proceedings of the 1999 Design, 1999

Validation of Object-Oriented Concurrent Designs by Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

Yet another Look at the LTL Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

1998
Kontrollfluss-Verifikation von Algorithmen mittels Modellprüfung.
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.
Proceedings of the Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 1998

Modeling and Verifying Abstract Multithreaded Systems.
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.
Proceedings of the Distributed and Parallel Embedded Systems, 1998

Model Checking on Product Structures.
Proceedings of the Formal Methods in Computer-Aided Design, 1998

Formal Specification in VHDL for Hardware Verification.
Proceedings of the 1998 Design, 1998

1997
The C@S System.
Proceedings of the Formal Hardware Verification - Methods and Systems in Comparison, 1997

1996
A Unified Approach for Combining Different Formalisms for Hardware Verification.
Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Ein einheitlicher Ansatz zur Unterstützung von Abstraktionsmechanismen der Hardware-Verifikation.
DISKI 116, Infix, ISBN: 978-3-89601-116-9, 1996

1995
Formal synthesis of circuits with a simple handshake protocol.
Proceedings of the 8th International Conference on VLSI Design (VLSI Design 1995), 1995

1994
Accelerating Tableaux Proofs Using Compact Representations.
Formal Methods in System Design, 1994

Automating Verification by Functional Abstraction at the System Level.
Proceedings of the Higher Order Logic Theorem Proving and Its Applications, 1994

A Formal Framework for High Level Synthesis.
Proceedings of the Theorem Provers in Circuit Design, 1994

Control Path Oriented Verification of Sequential Generic Circuits with Control and Data Path.
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.
Formal Methods in System Design, 1993

Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification.
Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic.
Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

A Functional Approach for Formalizing Regular Hardware Structures.
Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

Hardware-Verification using First Order BDDs.
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.
Proceedings of the Correct Hardware Design and Verification Methods, 1993

1992
Modelling Generic Hardware Structures by Abstract Datatypes.
Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1992

Efficient Representation and Computation of Tableau Proofs.
Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1992

The FAUST - Prover.
Proceedings of the Automated Deduction, 1992

1991
Structure in Hardware Proofs: First Steps Towards Automation in a Higher-Order Environment.
Proceedings of the VLSI 91, 1991

First Steps Towards Automating Hardware Proofs in HOL.
Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, 1991

Integrating a First-Order Automatic Prover in the HOL Environment.
Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, 1991

Automating Most Parts of Hardware Proofs in HOL.
Proceedings of the Computer Aided Verification, 3rd International Workshop, 1991

1981
Ein System-Diagnoseprozessor für zentralen und dezentralen Einsatz in Prozeßrechner-Systemen.
Proceedings of the Fachtagung Prozeßrechner 1981, 1981