|
|
|
 
|
[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)
|
|
|
|
 
|
[BaGS08]
K. Bauer and R. Gentilini and K. Schneider
Approximated Reachability on Hybrid Automata: Falsification meets Certification
Electronic Notes in Theoretical Computer Science (ENTCS)
|
|
|
|
 
|
[Baud08]
D. Baudisch
Synthesis for VLIW Architectures
Master Thesis
|
|
|
|
 
|
[Baue08b]
K. Bauer
Algebraic Methods and Abstractions for Automated 3-valued Reasoning on Hybrid Automata
Master Thesis
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[DyWi08]
S. Dyckmans and A. Willenbücher
Design and Implementation of a Dataflow-Processor for Synchronous Programs
Master Thesis
|
|
|
|
 
|
[Gemu08]
M. Gemünde
Evaluation Environment for AUTOSAR-Autocode in Motor Control Units
Master Thesis
|
|
|
|
 
|
[Gese08]
M. Gesell
Probabilistic Model Checking of Synchronous Programs
Master Thesis
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[PoSc08]
A. Poetzsch-Heffter and K. Schneider
Workshop on Verification of Adaptive Systems (VerAS)
|
|
|
|
 
|
[ScBr08]
K. Schneider and J. Brandt
Performing Causality Analysis by Bounded Model Checking
Conference on Application of Concurrency to System Design (ACSD)
|
|
|
|
 
|
[Schm08]
S. Schmitt
Supervisor Synthesis using SAT-Solvers
Master Thesis
|
|
|
|
 
|
[Baue07]
K. Bauer
On the Use of Gröbner Bases and Algebraic Methods for the Analysis of Hybrid Automata
Master Thesis
|
|
|
|
 
|
[Baue07a]
K. Bauer
Three-valued µ-Calculus on Hybrid Automata
Master Thesis
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Bran07]
J. Brandt
A Layered Approach to Polygon Processing for Safety-Critical Embedded Systems
PhD Thesis
|
|
|
|
 
|
[GeGe07]
M. Gesell and M. Gemünde
Eine Oberfläche zur Simulation synchroner Sprachen
Master Thesis
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[HoSc07]
J.C. Hoe and K. Schneider
International Conference on Formal Methods and Models for Co-Design (MEMOCODE)
|
|
|
|
 
|
[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
|
|
|
|
 
|
[ScBr07]
K. Schneider and J. Brandt
International Conference on Theorem Proving in Higher Order Logics (TPHOL)
|
|
|
|
 
|
[ScBr07a]
K. Schneider and J. Brandt
Theorem Proving in Higher Order Logics and Applications - Emerging Trends
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)
|
|
|
|
 
|
[Schu07]
T. Schuele
Verification of Infinite State Systems Using Presburger Arithmetic
PhD Thesis
|
|
|
|
 
|
[TuSG07]
T. Tuerk and K. Schneider and M. Gordon
Model Checking PSL Using HOL and SMV
Haifa Verification Conference (HVC)
|
|
|
|
 
|
[Baud06]
D. Baudisch
Implementierung und Verifikation eines RISC-Prozessors in Averest
Master Thesis
|
|
|
|
 
|
[BrSc06]
J. Brandt and K. Schneider
Multimedia-Hardwareerweiterungen
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Frie06]
M. Friedrich
Design and Implementation of a FCC Schedule Planner for an unmanned aircraft demonstrator
Master Thesis
|
|
|
|
 
|
[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
|
|
|
|
 
|
[Wagn06]
C. Wagner
Automatenbasierte Entscheidungsverfahren für Presburger-Arithmetik
Master Thesis
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Cron05]
B. Cronauer
XML-basierte Konfiguration von Steuergeräten
Master Thesis
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Schm05]
M. Schmidt
An Algorithm for Restriction of Finite Automata
Master Thesis
|
|
|
|
 
|
[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
|
|
|
|
 
|
[Tuer05]
T. Tuerk
A Hierarchy for Accellera's Property Specification Language
Master Thesis
|
|
|
|
 
|
[Wagn05a]
C. Wagner
Evaluierung von Algorithmen zur Berechnung fairer Pfade
Master Thesis
|
|
|
|
 
|
[ZiSc05]
R. Ziller and K. Schneider
Combining Supervisor Synthesis and Model Checking
Transactions on Embedded Computing Systems (TECS)
|
|
|
|
 
|
[BuKS04]
W. Büttner and W. Kunz and K. Schneider
Verifikation reaktiver Systeme
|
|
|
|
 
|
[Cron04]
B. Cronauer
Entwicklung eines embedded SPFH-Signal-Simulators für das JohnDeere GreenStar Office System
|
|
|
|
 
|
[Gent04]
R. Gentilini
Graph Algorithms for Massive Data-Sets
PhD Thesis
|
|
|
|
 
|
[Ober04]
A. Obermann
Verifikation kryptographischer Protokolle mit Baumtransduktoren
Master Thesis
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Webe04]
J. Weber
Entwurf eines RISC Prozessors mit synchronen Sprachen
Master Thesis
|
|
|
|
 
|
[Bran03]
J. Brandt
2D-Polygon-Clipping Algorithmen für eingebettete Echtzeitsysteme
Master Thesis
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[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
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[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
|
|
|
|
 
|
[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
|
|
|
|
 
|
[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)
|