| 2008 |
| 78 | EE | Klaus Schneider,
Jens Brandt:
Performing causality analysis by bounded model checking.
ACSD 2008: 78-87 |
| 77 | EE | Kerstin Bauer,
Raffaella Gentilini,
Klaus Schneider:
A Uniform Approach to Three-Valued Semantics for µ-Calculus on Abstractions of Hybrid Automata.
Haifa Verification Conference 2008: 38-52 |
| 76 | EE | Jens Brandt,
Klaus Schneider:
Formal Reasoning About Causality Analysis.
TPHOLs 2008: 118-133 |
| 75 | EE | Andreas Morgenstern,
Klaus Schneider:
From LTL to Symbolically Represented Deterministic Automata.
VMCAI 2008: 279-293 |
| 74 | EE | Arnd Poetzsch-Heffter,
Klaus Schneider:
Preface.
Electr. Notes Theor. Comput. Sci. 200(2): 1 (2008) |
| 73 | EE | Kerstin Bauer,
Raffaella Gentilini,
Klaus Schneider:
Approximated Reachability on Hybrid Automata: Falsification meets Certification.
Electr. Notes Theor. Comput. Sci. 223: 47-60 (2008) |
| 2007 |
| 72 | | Klaus Schneider,
Jens Brandt:
Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings
Springer 2007 |
| 71 | EE | Raffaella Gentilini,
Klaus Schneider,
Alexander Dreyer:
Three-valued automated reasoning on analog properties.
ACM Great Lakes Symposium on VLSI 2007: 485-488 |
| 70 | | Jens Brandt,
Klaus Schneider:
How Different are Esterel and SystemC?.
FDL 2007: 98-103 |
| 69 | EE | Raffaella Gentilini,
Klaus Schneider,
B. Mishra:
Successive Abstractions of Hybrid Automata for Monotonic CTL Model Checking.
LFCS 2007: 224-240 |
| 68 | EE | Tobias Schüle,
Klaus Schneider:
Bounded model checking of infinite state systems.
Formal Methods in System Design 30(1): 51-81 (2007) |
| 2006 |
| 67 | EE | Klaus Schneider,
Jens Brandt,
Eric Vecchié:
Modular Compilation of Synchronous Programs.
DIPES 2006: 75-84 |
| 66 | EE | Jens Brandt,
Klaus Schneider:
System Description Aspects as Syntactic Sugar.
FDL 2006: 293-301 |
| 65 | EE | Thomas Tuerk,
Klaus Schneider,
Mike Gordon:
Model Checking PSL Using HOL and SMV.
Haifa Verification Conference 2006: 1-15 |
| 64 | EE | Tobias Schüle,
Klaus Schneider:
Verification of Data Paths Using Unbounded Integers: Automata Strike Back.
Haifa Verification Conference 2006: 65-80 |
| 63 | EE | Klaus Schneider,
Jens Brandt,
Eric Vecchié:
Efficient code generation from synchronous programs.
MEMOCODE 2006: 165-174 |
| 62 | EE | Klaus Schneider,
Jens Brandt,
Tobias Schüle:
A Verified Compiler for Synchronous Programs with Local Declarations.
Electr. Notes Theor. Comput. Sci. 153(4): 71-97 (2006) |
| 2005 |
| 61 | EE | Klaus Schneider,
Jens Brandt,
Tobias Schüle,
Thomas Tuerk:
Maximal Causality Analysis.
ACSD 2005: 106-115 |
| 60 | EE | Jens Brandt,
Klaus Schneider:
Dependable Polygon-Processing Algorithms for Safety-Critical Embedded Systems.
EUC 2005: 405-417 |
| 59 | | Andreas Morgenstern,
Klaus Schneider:
A unified model checking framework for the supervisor synthesis problem.
GALOP 2005: 140-156 |
| 58 | EE | Jens Brandt,
Klaus Schneider:
Using Three-Valued Logic to Specify and Verify Algorithms of Computational Geometry.
ICFEM 2005: 405-420 |
| 57 | | Andreas Morgenstern,
Klaus Schneider:
Synthesizing deterministic controllers in supervisory control.
ICINCO 2005: 24-31 |
| 56 | EE | Tobias Schüle,
Klaus Schneider:
Three-valued logic in bounded model checking.
MEMOCODE 2005: 177-186 |
| 55 | EE | Thomas Tuerk,
Klaus Schneider:
From PSL to LTL: A Formal Validation in HOL.
TPHOLs 2005: 342-357 |
| 54 | EE | Roberto Ziller,
Klaus Schneider:
Combining supervisor synthesis and model checking.
ACM Trans. Embedded Comput. Syst. 4(2): 331-362 (2005) |
| 2004 |
| 53 | EE | Klaus Schneider,
Jens Brandt,
Tobias Schüle:
Causality analysis of synchronous programs with delayed actions.
CASES 2004: 179-189 |
| 52 | EE | Tobias Schüle,
Klaus Schneider:
Abstraction of assembler programs for symbolic worst case execution time analysis.
DAC 2004: 107-112 |
| 51 | EE | Tobias Schüle,
Klaus Schneider:
Bounded model checking of infinite state systems: exploiting the automata hierarchy.
MEMOCODE 2004: 17-26 |
| 50 | EE | Tobias Schüle,
Klaus Schneider:
Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems.
SEFM 2004: 67-76 |
| 2003 |
| 49 | EE | George Logothetis,
Klaus Schneider:
Exact High Level WCET Analysis of Synchronous Programs by Symbolic State Space Exploration.
DATE 2003: 10196-10203 |
| 48 | EE | George Logothetis,
Klaus Schneider,
C. Metzler:
Exact Low-Level Runtime Analysis of Synchronous Programs for Formal Verification of Real-Time Systems.
FDL 2003: 385-405 |
| 47 | EE | Tobias Schüle,
Klaus Schneider:
Exact Runtime Analysis Using Automata-Based Symbolic Simulation.
MEMOCODE 2003: 153-162 |
| 46 | EE | Roberto Ziller,
Klaus Schneider:
A Generalised Approach to Supervisor Synthesis.
MEMOCODE 2003: 217-226 |
| 45 | EE | George Logothetis,
Klaus Schneider,
C. Metzler:
Generating Formal Models for Real-Time Verification by Exact Low-Level Runtime Analysis of Synchronous Programs.
RTSS 2003: 256-264 |
| 44 | EE | George Logothetis,
Klaus Schneider,
C. Metzler:
Runtime Analysis of Synchronous Programs for Low-Level Real-Time Verification.
SBCCI 2003: 211-216 |
| 2002 |
| 43 | EE | George Logothetis,
Klaus Schneider:
Extending Synchronous Languages for Generating Abstract Real-Time Models.
DATE 2002: 795-803 |
| 42 | EE | Klaus Schneider:
Proving the Equivalence of Microstep and Macrostep Semantics.
TPHOLs 2002: 314-331 |
| 41 | | Michael Baldamus,
Klaus Schneider:
The BDD Space Complexity of Different Forms of Concurrency.
Fundam. Inform. 50(2): 111-133 (2002) |
| 2001 |
| 40 | EE | Klaus Schneider:
Embedding Imperative Synchronous Languages in Interactive Theorem Provers.
ACSD 2001: 143- |
| 39 | EE | Michael Baldamus,
Klaus Schneider:
The BDD Space Complexity of Different Forms of Concurrency.
ACSD 2001: 231- |
| 38 | EE | George Logothetis,
Klaus Schneider:
A New Approach to the Specification and Verification of Real-Time Systems.
ECRTS 2001: 171- |
| 37 | EE | Klaus Schneider:
Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy.
LPAR 2001: 39-54 |
| 36 | EE | George Logothetis,
Klaus Schneider:
Symbolic Model Checking of Real-Time Systems.
TIME 2001: 214-223 |
| 35 | EE | Michael Baldamus,
Klaus Schneider,
Michael Wenz,
Roberto Ziller:
Can American Checkers be Solved by Means of Symbolic Model Checking?
Electr. Notes Theor. Comput. Sci. 43: (2001) |
| 2000 |
| 34 | EE | George Logothetis,
Klaus Schneider:
Abstraction from Counters: An Application on Real-Time Systems.
DATE 2000: 486-493 |
| 33 | | Klaus Schneider:
A Verified Hardware Synthesis of Esterel Programs.
DIPES 2000: 205-214 |
| 1999 |
| 32 | EE | Klaus Schneider:
Yet another Look at the LTL Model Checking.
CHARME 1999: 321-325 |
| 31 | EE | Klaus Schneider,
Michaela Huhn,
George Logothetis:
Validation of Object-Oriented Concurrent Designs by Model Checking.
CHARME 1999: 360-364 |
| 30 | EE | Michaela Huhn,
Klaus Schneider,
Thomas Kropf,
George Logothetis:
Verifying Imprecisely Working Arithmetic Circuits.
DATE 1999: 65- |
| 29 | EE | Klaus Schneider,
Viktor K. Sabelfeld:
Introducing Mutual Exclusion in Esterel.
Ershov Memorial Conference 1999: 445-459 |
| 28 | | Thomas Stauner,
Klaus Schneider,
Michaela Huhn:
Translating a Visual Description Technique to a Synchronous Language: From DiChartsto PURR.
FBT 1999: 223-232 |
| 27 | EE | Klaus Schneider,
Dirk W. Hoffmann:
A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata.
TPHOLs 1999: 255-272 |
| 1998 |
| 26 | EE | Ralf Reetz,
Klaus Schneider,
Thomas Kropf:
Formal Specification in VHDL for Hardware Verification.
DATE 1998: 257- |
| 25 | | Klaus Schneider,
Michaela Huhn:
Comparing Model Checking and Term Rewriting for the Verification of an Embedded System.
DIPES 1998: 129-138 |
| 24 | EE | Klaus Schneider:
Model Checking on Product Structures.
FMCAD 1998: 483-500 |
| 1997 |
| 23 | | Klaus Schneider,
Thomas Kropf:
The C@S System.
Formal Hardware Verification 1997: 248-329 |
| 1996 |
| 22 | | Klaus Schneider,
Thomas Kropf:
A Unified Approach for Combining Different Formalisms for Hardware Verification.
FMCAD 1996: 202-217 |
| 1995 |
| 21 | EE | Ramayya Kumar,
Thomas Kropf,
Klaus Schneider:
Formal synthesis of circuits with a simple handshake protocol.
VLSI Design 1995: 255-259 |
| 1994 |
| 20 | | Klaus Schneider,
Thomas Kropf,
Ramayya Kumar:
Control Path Oriented Verification of Sequential Generic Circuits with Control and Data Path.
EDAC-ETC-EUROASIC 1994: 648-652 |
| 19 | | Thomas Kropf,
Klaus Schneider,
Ramayya Kumar:
A Formal Framework for High Level Synthesis.
TPCD 1994: 223-238 |
| 18 | | Klaus Schneider,
Ramayya Kumar,
Thomas Kropf:
Automating Verification by Functional Abstraction at the System Level.
TPHOLs 1994: 391-406 |
| 17 | | Klaus Schneider,
Ramayya Kumar,
Thomas Kropf:
Accelerating Tableaux Proofs Using Compact Representations.
Formal Methods in System Design 5(1/2): 145-176 (1994) |
| 1993 |
| 16 | | Thomas Kropf,
Ramayya Kumar,
Klaus Schneider:
Embedding Hardware Verification Within a Commercial Design Framework.
CHARME 1993: 242-257 |
| 15 | | Klaus Schneider,
Ramayya Kumar,
Thomas Kropf:
Hardware-Verification using First Order BDDs.
CHDL 1993: 45-62 |
| 14 | | Dirk Eisenbiegler,
Klaus Schneider,
Ramayya Kumar:
A Functional Approach for Formalizing Regular Hardware Structures.
HUG 1993: 101-114 |
| 13 | | Klaus Schneider,
Ramayya Kumar,
Thomas Kropf:
Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic.
HUG 1993: 213-226 |
| 12 | | Klaus Schneider,
Ramayya Kumar,
Thomas Kropf:
Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification.
HUG 1993: 385-398 |
| 11 | | Ramayya Kumar,
Klaus Schneider,
Thomas Kropf:
Structuring and Automating Hardware Proofs in a Higher-Order Theorem-Proving Environment.
Formal Methods in System Design 2(2): 165-223 (1993) |
| 1992 |
| 10 | | Klaus Schneider,
Ramayya Kumar,
Thomas Kropf:
The FAUST - Prover.
CADE 1992: 766-770 |
| 9 | | Klaus Schneider,
Ramayya Kumar,
Thomas Kropf:
Modelling Generic Hardware Structures by Abstract Datatypes.
TPHOLs 1992: 165-175 |
| 8 | | Klaus Schneider,
Ramayya Kumar,
Thomas Kropf:
Efficient Representation and Computation of Tableau Proofs.
TPHOLs 1992: 39-57 |
| 1991 |
| 7 | | Klaus Schneider,
Ramayya Kumar,
Thomas Kropf:
Automating Most Parts of Hardware Proofs in HOL.
CAV 1991: 365-375 |
| 6 | | Ramayya Kumar,
Thomas Kropf,
Klaus Schneider:
Integrating a First-Order Automatic Prover in the HOL Environment.
TPHOLs 1991: 170-176 |
| 5 | | Ramayya Kumar,
Thomas Kropf,
Klaus Schneider:
First Steps Towards Automating Hardware Proofs in HOL.
TPHOLs 1991: 190-193 |
| 4 | | Klaus Schneider,
Ramayya Kumar,
Thomas Kropf:
Structurein Hardware Proofs: Fist Steps Towards Automation in a Higher-Order Environment.
VLSI 1991: 81-90 |
| 1981 |
| 3 | | Klaus Schneider:
Ein System-Diagnoseprozessor für zentralen und dezentralen Einsatz in Prozeßrechner-Systemen.
Fachtagung Prozessrechner 1981: 186-195 |
| 1977 |
| 2 | | Klaus Pasemann,
Klaus Schneider:
Ein CAD-Anwendungssystem für Autoelektrik.
CAD-Fachgespräch 1977: 197-206 |
| 1976 |
| 1 | | Klaus Pasemann,
Klaus Schneider,
Ernst Vöge:
Das grafische Ausgabesystem am VW-Prozeß-Leit-System (PLS).
Elektronische Rechenanlagen 18(5): 241-245 (1976) |