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) |