Publications: Search Result

2010

[BaBS10] D. Baudisch and J. Brandt and K. Schneider Multithreaded Code from Synchronous Programs: Extracting Independent Threads for OpenMP Design, Automation and Test in Europe (DATE)

2009

				[BaGS09] D. Baudisch and M. Gesell and K. Schneider Online Exercise System - A Web-Based Tool for Administration and Automatic Correction of Exercises International Conference on Computer Supported Education (CSEDU)
				[BaGS09a] K. Bauer and R. Gentilini and K. Schneider Property Driven Three Valued Model Checking on Hybrid Automata Workshop on Logic, Language, Information and Computation (WoLLIC)
				[BaGS09b] K. Bauer and R. Gentilini and K. Schneider A Uniform Approach to Three-Valued Semantics for µ-Calculus on Abstractions of Hybrid Automata International Haifa Verification Conference (HVC)
				[BrGS09] J. Brandt and M. Gemünde and K. Schneider Desynchronising Synchronous Programs by Modes Conference on Application of Concurrency to System Design (ACSD)
				[BrSW09] J. Brandt and K. Schneider and A. Willenbücher Using IP Cores in Synchronous Languages Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)
				[BrSc09] J. Brandt and K. Schneider Separate Compilation of Synchronous Programs Software and Compilers for Embedded Systems (SCOPES)
				[BrSc09a] J. Brandt and K. Schneider Static Data-Flow Analysis of Synchronous Programs International Conference on Formal Methods and Models for Co-Design (MEMOCODE)
				[Schn09] K. Schneider The Synchronous Programming Language Quartz Technical Report
				[VeTS09] E. Vecchié and J.-P. Talpin and K. Schneider Separate Compilation and Execution of Imperative Synchronous Modules Design, Automation and Test in Europe (DATE)

2008

				[BaGS08] K. Bauer and R. Gentilini and K. Schneider Approximated Reachability on Hybrid Automata: Falsification meets Certification Electronic Notes in Theoretical Computer Science (ENTCS)
				[BrSW08] J. Brandt and K. Schneider and A. Willenbücher Hardware Acceleration for Model Checking Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)
				[BrSc08] J. Brandt and K. Schneider Embedded Systems: Status and Perspective
				[BrSc08a] J. Brandt and K. Schneider Formal Reasoning About Causality Analysis Theorem Proving in Higher Order Logic (TPHOL)
				[MoSL08] A. Morgenstern and K. Schneider and S. Lamberti Generating Deterministic &omega-Automata for most LTL Formulas by the Breakpoint Construction Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)
				[MoSc08] A. Morgenstern and K. Schneider From LTL to Symbolically Represented Deterministic Automata Verification, Model Checking, and Abstract Interpretation (VMCAI)
				[ScBr08] K. Schneider and J. Brandt Performing Causality Analysis by Bounded Model Checking Conference on Application of Concurrency to System Design (ACSD)

2007

				[BrSc07] J. Brandt and K. Schneider Advances in Design and Specification Languages for Embedded Systems
				[BrSc07b] J. Brandt and K. Schneider How Different are Esterel and SystemC? Forum on Specification and Design Languages (FDL)
				[GeSD07a] R. Gentilini and K. Schneider and A. Dreyer Combining Interval Arithmetic and Three-Valued Temporal Logics for the Verification of Analog Systems Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)
				[GeSD07b] R. Gentilini and K. Schneider and A. Dreyer Three-Valued Automated Reasoning on Analog Properties Great Lakes Symposium on VLSI (GLSVLSI)
				[GeSM07] R. Gentilini and K. Schneider and B. Mishra Successive Abstractions of Hybrid Automata for Monotonic CTL Model Checking International Symposium on Logical Foundations of Computer Science (LFCS)
				[MoSc07] A. Morgenstern and K. Schneider Synthesizing Deterministic Controllers in Supervisory Control
				[PBSS07] M. Proetzsch and K. Berns and T. Schuele and K. Schneider Formal Verification of Safety Behaviours of the Outdoor Robot RAVON International Conference on Informatics in Control, Automation and Robotics (ICINCO)
				[PoSc07] A. Poetzsch-Heffter and K. Schneider First DASMOD Workshop on Verification of Adaptive Systems (VerAS) Technical Report
				[ScSc07] T. Schuele and K. Schneider Verification of Data Paths Using Unbounded Integers: Automata Strike Back Haifa Verification Conference (HVC)
				[ScSc07a] T. Schuele and K. Schneider Bounded Model Checking of Infinite State Systems Formal Methods in System Design (FMSD)
				[TuSG07] T. Tuerk and K. Schneider and M. Gordon Model Checking PSL Using HOL and SMV Haifa Verification Conference (HVC)

2006

				[BrSc06a] J. Brandt and K. Schneider System Description Aspects as Syntactic Sugar Forum on Specification and Design Languages (FDL)
				[BrSc06b] J. Brandt and K. Schneider Efficient Map Overlay for Safety-Critical Embedded Systems International Symposium on Industrial Embedded Systems (IES)
				[ScBS06] K. Schneider and J. Brandt and T. Schuele A Verified Compiler for Synchronous Programs with Local Declarations Electronic Notes in Theoretical Computer Science (ENTCS)
				[ScBV06a] K. Schneider and J. Brandt and E. Vecchié Modular Compilation of Synchronous Programs IFIP Conference on Distributed and Parallel Embedded Systems (DIPES)
				[ScBV06b] K. Schneider and J. Brandt and E. Vecchié Efficient Code Generation from Synchronous Programs Formal Methods and Models for Codesign (MEMOCODE)
				[ScST06] K. Schneider and T. Schuele and M. Trapp Verifying the Adaptation Behavior of Embedded Systems Software Engineering for Adaptive and Self-Managing Systems (SEAMS)
				[ScSc06a] K. Schneider and T. Schuele A Framework for Verifying and Implementing Embedded Systems Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
				[Schn06a] K. Schneider Book Review: `A Practical Theory of Reactive Systems' The Computer Journal

2005

				[BrSc05] J. Brandt and K. Schneider Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry International Conference on Formal Engineering Methods (ICFEM)
				[BrSc05a] J. Brandt and K. Schneider Dependable Polygon-Processing Algorithms for Safety-Critical Embedded Systems International Conference on Embedded and Ubiquitous Computing (EUC)
				[MoSc05] A. Morgenstern and K. Schneider A Unified Model Checking Framework for the Supervisor Synthesis Problem Games for Logic and Programming Languages
				[MoSc05a] A. Morgenstern and K. Schneider Synthesizing Deterministic Controllers in Supervisory Control International Conference on Informatics in Control, Automation and Robotics (ICINCO)
				[MoSc05b] A. Morgenstern and K. Schneider Using Model Checking to Solve Supervisor Synthesis Problems Conference on Decision and Control and European Control Conference (CDC/ECC)
				[SBST05a] K. Schneider and J. Brandt and T. Schuele and T. Tuerk Improving Constructiveness in Code Generators Synchronous Languages, Applications, and Programming (SLAP)
				[SBST05b] K. Schneider and J. Brandt and T. Schuele and T. Tuerk Maximal Causality Analysis Application of Concurrency to System Design (ACSD)
				[ScSc05] T. Schuele and K. Schneider Three-Valued Logic in Bounded Model Checking Formal Methods and Models for Codesign (MEMOCODE)
				[ScSc05a] K. Schneider and T. Schuele Averest: Specification, Verification, and Implementation of Reactive Systems Conference on Application of Concurrency to System Design (ACSD)
				[TuSc05] T. Tuerk and K. Schneider From PSL to LTL: A Formal Validation in HOL Theorem Proving in Higher Order Logic (TPHOL)
				[TuSc05a] T. Tuerk and K. Schneider Relationship between Alternating omega-Automata and Symbolically Represented Nondeterministic omega-Automata Technical Report
				[ZiSc05] R. Ziller and K. Schneider Combining Supervisor Synthesis and Model Checking Transactions on Embedded Computing Systems (TECS)

2004

				[BuKS04] W. Büttner and W. Kunz and K. Schneider Verifikation reaktiver Systeme
				[ScBS04a] K. Schneider and J. Brandt and T. Schuele A Verified Compiler for Synchronous Programs with Local Declarations(proceedings version) Synchronous Languages, Applications, and Programming (SLAP)
				[ScBS04b] K. Schneider and J. Brandt and T. Schuele Causality Analysis of Synchronous Programs with Delayed Actions Compilers, Architecture, and Synthesis for Embedded Systems (CASES)
				[ScSc04] T. Schuele and K. Schneider Global vs. Local Model Checking of Infinite State Systems Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
				[ScSc04a] T. Schuele and K. Schneider Abstraction of Assembler Programs for Symbolic Worst Case Execution Time Analysis Design Automation Conference (DAC)
				[ScSc04b] T. Schuele and K. Schneider Bounded Model Checking of Infinite State Systems: Exploiting the Automata Hierarchy Formal Methods and Models for Codesign (MEMOCODE)
				[ScSc04c] T. Schuele and K. Schneider Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems Software Engineering and Formal Methods (SEFM)

2003

				[LoSM03a] G. Logothetis and K. Schneider and C. Metzler Exact Low-Level Runtime Analysis of Synchronous Programs for Formal Verification of Real-Time Systems Forum on Specification and Design Languages (FDL)
				[LoSM03b] G. Logothetis and K. Schneider and C. Metzler Runtime Analysis of Synchronous Programs for Low-Level Real-Time Verification Symposium on Integrated Circuits and System Design (SBCCI)
				[LoSM03c] G. Logothetis and K. Schneider and C. Metzler Generating Formal Models for Real-Time Verification by Exact Low-Level Runtime Analysis of Synchronous Programs International Real-Time Systems Symposium (RTSS)
				[LoSc03] G. Logothetis and K. Schneider Exact High Level WCET Analysis of Synchronous Programs by Symbolic State Space Exploration Design, Automation and Test in Europe (DATE)
				[ScSc03] T. Schuele and K. Schneider Exact Runtime Analysis Using Automata-Based Symbolic Simulation International Conference on Formal Methods and Models for Co-Design (MEMOCODE)
				[Schn03] K. Schneider Verification of Reactive Systems - Formal Methods and Algorithms Springer
				[ZiSc03a] R. Ziller and K. Schneider A µ-Calculus Approach to Supervisor Synthesis Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
				[ZiSc03b] R. Ziller and K. Schneider A Generalized Approach to Supervisor Synthesis Formal Methods and Models for Codesign (MEMOCODE)
				[ZiSc03c] R. Ziller and K. Schneider Reducing Complexity of Supervisor Synthesis IFAC Conference on Control Systems Design (CSD)

2002

				[BaSc02] M. Baldamus and K. Schneider The BDD Space Complexity of Different Forms of Concurrency Fundamenta Informaticae
				[LoSc02] G. Logothetis and K. Schneider Extending Synchronous Languages for Generating Abstract Real-Time Models Design, Automation and Test in Europe (DATE)
				[ScSc02] T. Schuele and K. Schneider Symbolic Model Checking by Automata Based Set Representation Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
				[Schn02] K. Schneider Proving the Equivalence of Microstep and Macrostep Semantics Theorem Proving in Higher Order Logic (TPHOL)

2001

				[BSWZ01] M. Baldamus and K. Schneider and M. Wenz and R. Ziller Can American Checkers be Solved by Means of Symbolic Model Checking? Electronic Notes in Theoretical Computer Science (ENTCS)
				[BaSc01] M. Baldamus and K. Schneider The BDD Space Complexity of Different Forms of Concurrency Conference on Application of Concurrency to System Design (ACSD)
				[HHKK01] D.W. Hoffmann and L. Holt and E. Klein and T. Kropf and K. Schneider Special Issue on the PROSPER project
				[LoSc01] G. Logothetis and K. Schneider A New Approach to the Specification and Verification of Real-Time Systems Euromicro Conference on Real Time Systems
				[LoSc01a] G. Logothetis and K. Schneider Symbolic model checking of real-time systems Symposium on Temporal Representation and Reasoning (TIME)
				[ScWe01] K. Schneider and M. Wenz A new method for compiling schizophrenic synchronous programs Conference on Compilers, Architectures and Synthesis for Embedded Systems (CASES)
				[Schn01] K. Schneider Exploiting Hierarchies in Temporal Logics, Finite Automata, Arithmetics, and µ-Calculus for Efficiently Verifying Reactive Systems University of Karlsruhe
				[Schn01a] K. Schneider Embedding Imperative Synchronous Languages in Interactive Theorem Provers Conference on Application of Concurrency to System Design (ACSD)
				[Schn01b] K. Schneider Improving Automata Generation for Linear Temporal Logic by Considering the Automata Hierarchy Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)

2000

				[BSWZ00] M. Baldamus and K. Schneider and M. Wenz and R. Ziller Can American Checkers be Solved by Means of Symbolic Model Checking? Formal Methods Elsewhere, Satellite Workshop of FORTE-PSTV 2000
				[LoSc00] G. Logothetis and K. Schneider Abstraction from Counters: An Application on Real-Time Systems Design, Automation and Test in Europe (DATE)
				[Schn00] K. Schneider A Verified Hardware Synthesis for Esterel Workshop on Distributed and Parallel Embedded Systems (DIPES)

1999

				[BaSc99] M. Baldamus and K. Schneider Extending Esterel by Asynchronous Concurrency Fachtagung zum Entwurf Integrierter Schaltungen
				[HSKL99] M. Huhn and K. Schneider and T. Kropf and G. Logothetis Verifying Imprecisely Working Arithmetic Circuits Design, Automation and Test in Europe (DATE)
				[SSHL99] D. Schmid and K. Schneider and M. Huhn and G. Logothetis and V. Sabelfeld Formale Verifikation eingebetteter Systeme Informationstechnik und Technische Informatik (it+ti)
				[ScHL99] K. Schneider and M. Huhn and G. Logothetis Validation of Object Oriented Concurrent Designs by Model Checking Correct Hardware Design and Verification Methods (CHARME)
				[ScHo99] K. Schneider and D.W. Hoffmann A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata Theorem Proving in Higher Order Logic (TPHOL)
				[ScHu99] K. Schneider and M. Huhn Comparing Model-Checking and Term-Rewriting in the Verification of an Embedded System Workshop on Distributed and Parallel Embedded Systems (DIPES)
				[ScLo99] K. Schneider and G. Logothetis Abstraction of Systems with Counters for Symbolic Model Checking Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
				[ScSa99] K. Schneider and V. Sabelfeld Introducing Mutual Exclusion in Esterel Andrei Ershov Third International ConferencePerspectives of Systems Informatics
				[Schn99] K. Schneider Yet Another Look at LTL Model Checking Correct Hardware Design and Verification Methods (CHARME)
				[StSH99] T. Stauner and K. Schneider and M. Huhn Translating a Visual Description Technique to a Synchronous Language: From DiCharts to PURR Formale Beschreibungstechniken für verteilte Systeme

1998

				[GrSc98] W. Grünewald and K. Schneider Modeling and Verifying Abstract Multithreaded Systems Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
				[KRSW98] T. Kropf and J. Ruf and K. Schneider and M. Wild A Synchronous Language for Modeling and Verifying Real Time and Embedded Systems Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
				[KRSW98a] T. Kropf and J. Ruf and K. Schneider and M. Wild The Synchronous System Description Language PURR Open Project Workshop on System Design Automation (SDA98)
				[ReSK98] R. Reetz and K. Schneider and T. Kropf Formal Specification in VHDL for Formal Hardware Verification Design, Automation and Test in Europe (DATE)
				[SSFS98] I. Schreiber and J. Schönherr and E. Fordran and K. Schneider and B. Straube Kontrollfluß-Verifikation von Algorithmen mittels Modellprüfung Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
				[Schn98] K. Schneider Model Checking on Product Structures Formal Methods in Computer Aided Design (FMCAD)

1997

				[ReSK97a] R. Reetz and K. Schneider and T. Kropf Formale Spezifikation und Verifikation mit VHDL Hardwarebeschreibungssprachen und Modellierungsparadigmen
				[ReSK97b] R. Reetz and K. Schneider and T. Kropf Ein neues Konzept zur formalen Spezifikation in VHDL mit einerFallstudie zum Single Pulser Methoden des Entwurfs und der Verifikation digitaler Systeme
				[ScKr97a] K. Schneider and T. Kropf The C@S System: Combining Proof Strategies for System Verification
				[ScWe97] K. Schneider and H. Weindel An Efficient Decision Procedure for S1S Methoden des Entwurfs und der Verifikation digitaler Systeme
				[Schn97a] K. Schneider CTL and Equivalent Sublanguages of CTL* Conference on Computer Hardware Description Languages and Their Applications (CHDL)
				[Schn97b] K. Schneider Translating Linear Temporal Logic to Deterministic &omega-Automata Methoden des Entwurfs und der Verifikation digitaler Systeme

1996

				[FrKS96] J. Frößl and T. Kropf and K. Schneider Bewertung temporaler Logiken für die Hardware-Verifikation Methoden des Entwurfs und der Verifikation digitaler Systeme
				[ScKr96b] K. Schneider and T. Kropf A Unified Approach for Combining Different Formalisms for Hardware Verification Methoden des Entwurfs und der Verifikation digitaler Systeme
				[ScKr96c] K. Schneider and T. Kropf A Unified Approach for Combining Different Formalisms for Hardware Verification Formal Methods in Computer Aided Design (FMCAD)
				[Schn96a] K. Schneider Ein einheitlicher Ansatz zur Unterstützung von Abstraktionsmechanismen der Hardwareverifikation Infix

1995

				[ScKT95b] K. Schneider and T. Kropf and T. Thiessenhusen Spezifikation und Verifikation systolischer Felder mit Logik höherer Ordnung Anwendung formaler Methoden beim Entwurf von Hardwaresystemen
				[Schn95c] K. Schneider Ein automatentheoretischer Ansatz zur Strukturabstraktion für die hierarchische Verifikation Anwendung formaler Methoden beim Entwurf von Hardwaresystemen

1994

				[EiSK94] D. Eisenbiegler and K. Schneider and R. Kumar A Functional Approach for Formalizing Regular Hardware Structures Theorem Proving in Higher Order Logic (TPHOL)
				[KrSK94a] T. Kropf and K. Schneider and R. Kumar A Formal Framework for High Level Synthesis Theorem Provers in Circuit Design (TPCD)
				[PoSc94] J. Posegga and K. Schneider A First-Order Calculus Based on Propositional BDDs Anwendung formaler Methoden im Systementwurf
				[SSSK94] A. Schneider and B. Straube and K. Schneider and T. Kropf Verifikation eines digitalen Netzwerkes mit Hilfe des Beweissystems HOL Technical Report
				[ScKK94] K. Schneider and R. Kumar and T. Kropf Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification Theorem Proving in Higher Order Logic (TPHOL)
				[ScKK94a] K. Schneider and T. Kropf and R. Kumar Control-Path Oriented Verification of Sequential Generic Circuits with Control and Data Path European Design and Test Conference (EDTC)
				[ScKK94b] K. Schneider and T. Kropf and R. Kumar Accelerating Tableaux Proofs using Compact Representations Formal Methods in System Design (FMSD)
				[ScKK94c] K. Schneider and T. Kropf and R. Kumar Why Hardware Verification Needs more than Model Checking Theorem Proving in Higher Order Logic (TPHOL)
				[ScKK94d] K. Schneider and R. Kumar and T. Kropf Automating Verification by Functional Abstraction at the System Level Theorem Proving in Higher Order Logic (TPHOL)
				[ScKK94e] K. Schneider and R. Kumar and T. Kropf Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic Theorem Proving in Higher Order Logic (TPHOL)
				[ScKK94h] K. Schneider and T. Kropf and R. Kumar Hardware-Verifikation braucht mehr als Model-Checking Anwendung formaler Methoden im Systementwurf

1993

				[KrKS93a] T. Kropf and R. Kumar and K. Schneider Embedding Hardware Verification within a Commercial Design Framework Correct Hardware Design and Verification Methods (CHARME)
				[KuSK93a] R. Kumar and K. Schneider and T. Kropf Structuring and Automating Hardware Proofs in a Higher-Order Theorem-Proving Environment Formal Methods in System Design (FMSD)
				[PoSc93] J. Posegga and K. Schneider Deduction with First-Order BDDs Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX)
				[ScKK93a] K. Schneider and R. Kumar and T. Kropf Hardware-Verification using First Order BDDs Conference on Computer Hardware Description Languages and Their Applications (CHDL)
				[ScKK93e] K. Schneider and T. Kropf and R. Kumar Kontrollpfad-orientierte Verifikation generischer Datenpfade E.I.S.-Workshop (Entwurf integrierter Schaltungen)
				[ScRS93] D. Schmid and R. Reetz and K. Schneider Ein Praktikum zur Hardware-Verifikation E.I.S.-Workshop (Entwurf integrierter Schaltungen)

1992

				[KrKS92] T. Kropf and R. Kumar and K. Schneider Bridging the Gap between Hardware-Verification and Design IFIP World Conference
				[ScKK92] K. Schneider and R. Kumar and T. Kropf Automating most Parts of Hardware Proofs in HOL Computer Aided Verification (CAV)
				[ScKK92a] K. Schneider and R. Kumar and T. Kropf The FAUST prover Conference on Automated Deduction (CADE)
				[ScKK92b] K. Schneider and R. Kumar and T. Kropf Efficient Representation and Computation of Tableau Proofs Theorem Proving in Higher Order Logic (TPHOL)
				[ScKK92c] K. Schneider and R. Kumar and T. Kropf Modelling generic Hardware Structures by Abstract Datatypes Theorem Proving in Higher Order Logic (TPHOL)

1991

				[KuKS91a] R. Kumar and T. Kropf and K. Schneider Integrating a First-Order Automatic Prover in the HOL Environment Theorem Proving in Higher Order Logic (TPHOL)
				[KuKS91b] R. Kumar and T. Kropf and K. Schneider First Steps Towards Automating Hardware Proofs in HOL Theorem Proving in Higher Order Logic (TPHOL)
				[ScKK91a] K. Schneider and R. Kumar and T. Kropf Structuring Hardware Proofs: First steps towards Automation in a Higher-Order Environment Conference on Very Large Scale Integration (VLSI)
				[Schn91] K. Schneider Ein Sequenzenkalkül für HOL Master Thesis