|
|
|
 
|
[BELS10]
A. Benveniste and S.A. Edwards and E. Lee and K. Schneider and R. von Hanxleden
SYNCHRON'09: Abstracts Collection of Dagstuhl Seminar 09481
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[BaBS10a]
D. Baudisch and J. Brandt and K. Schneider
Multithreaded Code from Synchronous Programs: Generating Software Pipelines for OpenMP
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)
|
|
|
|
 
|
[BaSc10]
K. Bauer and K. Schneider
From Synchronous Programs to Symbolic Representations of Hybrid Systems
Hybrid Systems: Computation and Control (HSCC)
|
|
|
|
 
|
[BrGS10]
J. Brandt and M. Gemünde and K. Schneider
From Synchronous Guarded Actions to SystemC
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)
|
|
|
|
 
|
[BrSS10]
J. Brandt and K. Schneider and S. Shukla
Translating Concurrent Action Oriented Specifications to Synchronous Guarded Actions
Languages, Compilers, and Tools for Embedded Systems (LCTES)
|
|
|
|
 
|
[GeBS10]
M. Gemünde and J. Brandt and K. Schneider
Clock Refinement in Imperative Synchronous Languages
SYNCHRON'09: Abstracts Collection of Dagstuhl Seminar 09481
|
|
|
|
 
|
[Morg10]
A. Morgenstern
Symbolic Controller Synthesis for LTL Specifications
PhD Thesis
|
|
|
|
 
|
[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
Desynchronizing 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 for 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)
|
|
|
|
 
|
[AdSS08]
R. Adler and I. Schaefer and T. Schuele
Model-Based Development of an Adaptive Vehicle Stability Control System
Modellbasierte Entwicklung von eingebetteten Fahrzeugfunktionen (MBEFF)
|
|
|
|
 
|
[BFKG08]
K. Bauer and T. Fischer and S.O. Krumke and K. Gerhardt and S. Westphal and P. Merz
Improved Construction Heuristics and Iterated Local Search for the Routing and Wavelength Assignment Problem
European Conference on Evolutionary Computation in Combinatorial Optimisation (EvoCOP)
|
|
|
|
 
|
[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 Logics (TPHOL)
|
|
|
|
 
|
[DyWi08]
S. Dyckmans and A. Willenbücher
Design and Implementation of a Dataflow-Processor for Synchronous Programs
Master Thesis
|
|
|
|
 
|
[FiBM08]
T. Fischer and K. Bauer and P. Merz
A Multilevel Approach for the Routing and Wavelength Assignment Problem
IEEE/IPSJ International Symposium on Applications and the Internet
|
|
|
|
 
|
[FiBM08a]
T. Fischer and K. Bauer and P. Merz
A Distributed Memetic Algorithm for the Routing and Wavelength Assignment Problem
International Conference on Parallel Problem Solving from Nature (PPSN)
|
|
|
|
 
|
[GePP08]
R. Gentilini and C. Piazza and A. Policriti
Symbolic Graphs: Linear Solutions to Some Connectivity Problems
Algorithmica
|
|
|
|
 
|
[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)
Electronic Notes in Theoretical Computer Science (ENTCS)
|
|
|
|
 
|
[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
|
|
|
|
 
|
[ASSV07]
R. Adler and I. Schaefer and T. Schuele and E. Vecchié
From Model-Based Design to Formal Verification of Adaptive Embedded Systems
International Conference on Formal Engineering Methods (ICFEM)
|
|
|
|
 
|
[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
Different Kinds of System Descriptions as Synchronous Programs
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Zimm07]
G. Zimmermann
Modeling and simulation of individual user behavior for building performance predictions
Summer Computer Simulation Conference (SCSC)
|
|
|
|
 
|
[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
|
|
|
|
 
|
[VeSi06]
E. Vecchié and R. de Simone
Syntax-driven Behavior Partitioning for Model-checking of Esterel Programs
Electronic Notes in Theoretical Computer Science (ENTCS)
|
|
|
|
 
|
[Wagn06]
C. Wagner
Automatenbasierte Entscheidungsverfahren für Presburger-Arithmetik
Master Thesis
|
|
|
|
 
|
[ZiSc06a]
R. Ziller and D. Schmid
Erstellung korrekter Spezifikationen für diskrete Systeme
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
|
|
|
|
 
|
[Zimm06]
G. Zimmermann
Modeling and simulation of dynamic user behavior in buildings - a lighting control case study
European Conference of Product and Process Modelling (ECPPM)
|
|
|
|
 
|
[Zimm06a]
G. Zimmermann
Multi-Agent Model to Multi-Process Transformation - A housing market case study
|
|
|
|
 
|
[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
|
|
|
|
 
|
[Gent05]
R. Gentilini
Reachability Problems on Extended O-Minimal Hybrid Automata
Formal Modeling and Analysis of Timed Systems (FORMATS)
|
|
|
|
 
|
[Gent05a]
R. Gentilini
Toward Integration of Systems Biology Formalism: The Gene Regulatory Networks Case
Genome Informatics
|
|
|
|
 
|
[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 Logics (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
|
|
|
|
 
|
[VeSi05]
E. Vecchié and R. de Simone
Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs
Computer Aided Verification (CAV)
|
|
|
|
 
|
[ViZi05]
O. Vityaz and G. Zimmermann
Real-Time Simulation Using Graceful Degradation of Accuracy
Energy and Buildings
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[ZiSu05]
G. Zimmermann and G. Suter
A multi-floor topology to geometry transformation procedure based on shape functions
International Conference on Information Technology in Construction
|
|
|
|
 
|
[Zill05a]
R. Ziller
An Application of Generalized Supervisor Synthesis to the Control of a Call Center
Forum on Specification and Design Languages (FDL)
|
|
|
|
 
|
[Zill05b]
R. Ziller
Eine Verallgemeinerung der Überwachersynthese mit Hilfe des µ-Kalküls
PhD Thesis
|
|
|
|
 
|
[Zimm05]
G. Zimmermann
From Floor Plan Drafting to Building Simulation - an Efficient Software Supported Process
International IBPSA Conference Building Simulation
|
|
|
|
 
|
[BGGS04]
J. Brandt and R. Gotzhein and R. Grammes and B. Schürmann
Chatroom over WLAN - Systematic Development of an QoS-Integrated Distributed System
European Wireless 2004
|
|
|
|
 
|
[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
|
|
|
|
 
|
[Logo04]
G. Logothetis
Forward and Time-Jumping Symbolic Model Checking for Real Time Systems
Conference on Real-Time and Embedded Computing Systems and Applications (RTCSA)
|
|
|
|
 
|
[Logo04b]
G. Logothetis
Specification, Modelling, Verification and Runtime Analysis of Real Time Systems
IOS Press
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Vecc04]
E. Vecchié
Calcul des etats atteignables de programmes Esterel partitionne selon la syntaxe
PhD Thesis
|
|
|
|
 
|
[Webe04]
J. Weber
Entwurf eines RISC Prozessors mit synchronen Sprachen
Master Thesis
|
|
|
|
 
|
[ZiMe04]
G. Zimmermann and A. Metzger
A Software Generation Process for User-centered Dynamic Building System Models
European Conference of Product and Process Modelling in the Building and Construction Industry (ECPPM)
|
|
|
|
 
|
[ZiSu04]
G. Zimmermann and G. Suter
A Model for hierarchical floor plan generation based on shape functions
European Conference of Product and Process Modelling in the Building and Construction Industry (ECPPM)
|
|
|
|
 
|
[Bran03]
J. Brandt
2D-Polygon-Clipping Algorithmen für eingebettete Echtzeitsysteme
Master Thesis
|
|
|
|
 
|
[GePP03]
R. Gentilini and C. Piazza and A. Policriti
Computing Strongly Connected Components in a Linear Number of Symbolic Steps
Symposium on Discrete Algorithms (SODA)
|
|
|
|
 
|
[GePP03a]
R. Gentilini and C. Piazza and A. Policriti
From Bisimulation to Simulation - Coarsest Partition Problems
Journal of Automated Reasoning
|
|
|
|
 
|
[GePo03]
R. Gentilini and A. Policriti
Biconnectivity on Symbolically Represented Graphs: A Linear Solution
International Symposium on Algorithms and Computation (ISAAC)
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[MeZi03]
A. Metzger and G. Zimmermann
Modellierung Reaktiver Systeme: Ein Fallbeispiel
Technical Report
|
|
|
|
 
|
[Morg03]
A. Morgenstern
Werkzeuge zur Verifikation diskreter Ereignis-Systeme
Master Thesis
|
|
|
|
 
|
[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
|
|
|
|
 
|
[Tuer03]
T. Tuerk
Constraint-basierte Vervollständigungstechniken: Gleichheitsconstraints
Master Thesis
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Zimm03]
G. Zimmermann
Modeling the building as a system
International IBPSA Conference Building Simulation
|
|
|
|
 
|
[BaSc02]
M. Baldamus and K. Schneider
The BDD Space Complexity of Different Forms of Concurrency
Fundamenta Informaticae
|
|
|
|
 
|
[DGPP02]
A. Dovier and R. Gentilini and C. Piazza and A. Policriti
Rank-Based Symbolic Bisimulation (and Model Checking)
Electronic Notes in Theoretical Computer Science (ENTCS)
|
|
|
|
 
|
[GePP02]
R. Gentilini and C. Piazza and A. Policriti
Simulation as Coarsest Partition Problem
Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
|
|
|
|
 
|
[GePP02a]
R. Gentilini and C. Piazza and A. Policriti
Simulation Reduction as Constraint
Electronic Notes in Theoretical Computer Science (ENTCS)
|
|
|
|
 
|
[LoSc02]
G. Logothetis and K. Schneider
Extending Synchronous Languages for Generating Abstract Real-Time Models
Design, Automation and Test in Europe (DATE)
|
|
|
|
 
|
[MaMZ02a]
A. Mahdavi and A. Metzger and G. Zimmermann
Towards a Virtual Laboratory for Building Performance and Control
European Meeting on Cybernetics and Systems Research (EMCSR)
|
|
|
|
 
|
[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 Logics (TPHOL)
|
|
|
|
 
|
[Zill02]
R. Ziller
Finding Bad States during Symbolic Supervisor Synthesis
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
|
|
|
|
 
|
[Zimm02]
G. Zimmermann
Efficient creation of building performance simulators using automatic code generation
Energy and Buildings
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[ScSt01a]
T. Schuele and A.P. Ströle
Test Scheduling for Minimal Energy Consumption under Power Constraints
VLSI Test Symposium (VTS)
|
|
|
|
 
|
[ScSt01b]
T. Schuele and A.P. Ströle
Scheduling Tests for Low Power Built-In Self-Test
International Symposium on Circuits and Systems (ISCAS)
|
|
|
|
 
|
[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, Germany
|
|
|
|
 
|
[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
International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)
|
|
|
|
 
|
[Zill01]
R. Ziller
System Modelling Using Marker States in the RW-Framework
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
|
|
|
|
 
|
[Zimm01]
G. Zimmermann
A New Approach To Building Simulation Based on Communicating Objects
International Conference on Building Performance Simulation Association (IBPSA)
|
|
|
|
 
|
[BaSc99]
M. Baldamus and K. Schneider
Extending Esterel by Asynchronous Concurrency
Fachtagung zum Entwurf Integrierter Schaltungen
|
|
|
|
 
|
[FMQV99]
R.L. Feldmann and J. Münch and S. Queins and S. Vorwieger and G. Zimmermann
Baselining a Domain-Specific Software Development Process
Technical Report
|
|
|
|
 
|
[HSKL99]
M. Huhn and K. Schneider and T. Kropf and G. Logothetis
Verifying Imprecisely Working Arithmetic Circuits
Design, Automation and Test in Europe (DATE)
|
|
|
|
 
|
[HeZi99]
A. Heß and G. Zimmermann
Interconnection Length Estimation During Hierarchical VLSI Design
Workshop on System-Level Interconnect Prediction (SLIP)
|
|
|
|
 
|
[QuZi99]
S. Queins and G. Zimmermann
A First Iteration of a Reuse-Driven, Domain-Specific System Requirements Analysis Process
Technical Report
|
|
|
|
 
|
[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 Logics (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
|
|
|
|
 
|
[ScRZ99]
M. Schütze and J.P. Riegel and G. Zimmermann
PSiGene: A pattern-based component generator for building simulation
Theory and Practice of Object Systems (TAPOS)
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Schu99]
T. Schuele
Test von Systems-On-A-Chip mit eingebetteten Prozessoren
Master Thesis
|
|
|
|
 
|
[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
|
|
|
|
 
|
[Zill99]
R. Ziller
Microprocessadores: Conceitos Importantes
|
|
|
|
 
|
[AGHL98]
J. Avenhaus and R. Gotzhein and T. Härder and L. Litz and K. Madlener and J. Nehmer and M. Richter and N. Ritter and D. Rombach and B. Schürmann and G. Zimmermann
Entwicklung großer Systeme mit generischen Methoden - Eine Übersicht über den Sonderforschungsbereich 501
Informatik - Forschung und Entwicklung
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Zill98]
R. Ziller
Aplicação de Autômatos em Especificações de Comportamento
Anais da I Semana Tecnológica da UNIVALI e III Semana da Computação de Biguaçu
|
|
|
|
 
|
[Zimm98a]
G. Zimmermann
Modeling embedded digital controllers
International Conference on New Information Technologies in Science, Education, Telecommunications and Business (IT+SE)
|
|
|
|
 
|
[Zimm98b]
G. Zimmermann
A domain Specific Model Architecture for Complex Embedded Systems: A Building Automation Case Study
Technical Report
|
|
|
|
 
|
[Zimm98c]
G. Zimmermann
Domain Specific Model Architecture for Complex Embedded Systems: A Building Automation Case Study
Adaptation and Evolution in Embedded Information Systems (Seminar No. 98441)
|
|
|
|
 
|
[ARSS97]
J. Altmeyer and J.P. Riegel and B. Schürmann and M. Schütze and G. Zimmermann
Application of a Generator-Based Software Development Method Supporting Model Reuse
International Conference on Advanced Information Systems Engineering (CAiSE)
|
|
|
|
 
|
[HRSS97]
F. Heister and J.P. Riegel and M. Schütze and S. Schulz and G. Zimmermann
Pattern-Based Code Generation for Well-Defined Application Domains
European Conference on Pattern Languages of Programming (EuroPLoP)
|
|
|
|
 
|
[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
|
|
|
|
 
|
[RiSZ97]
J.P. Riegel and M. Schütze and G. Zimmermann
Pattern-Based Generation of Customized, Flexible Building Simulators
International Conference on Computer-aided Architectural Design Futures (CAADFutures)
|
|
|
|
 
|
[ScKr97a]
K. Schneider and T. Kropf
The C@S System: Combining Proof Strategies for System Verification
|
|
|
|
 
|
[ScRZ97]
M. Schütze and J.P. Riegel and G. Zimmermann
A Pattern-Based Application Generator for Building Simulation
European Software Engineering Conference (ESEC)
|
|
|
|
 
|
[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
|
|
|
|
 
|
[Zimm97]
G. Zimmermann
Building Automation: A Software Engineer's View
Technical Report
|
|
|
|
 
|
[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
|
|
|
|
 
|
[RiSZ96]
J.P. Riegel and M. Schütze and G. Zimmermann
Objektorientierte Modellierung einer Simulationsumgebung mit Patterns
Technical Report
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[ScZi96]
B. Schürmann and G. Zimmermann
PLAYOUT - A Hierarchical Layout System
|
|
|
|
 
|
[Schn96a]
K. Schneider
Ein einheitlicher Ansatz zur Unterstützung von Abstraktionsmechanismen der Hardwareverifikation
Infix
|
|
|
|
 
|
[EiSK94]
D. Eisenbiegler and K. Schneider and R. Kumar
A Functional Approach for Formalizing Regular Hardware Structures
Theorem Proving in Higher Order Logics (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 Logics (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 Automation Conference (EDAC)
|
|
|
|
 
|
[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 Logics (TPHOL)
|
|
|
|
 
|
[ScKK94d]
K. Schneider and R. Kumar and T. Kropf
Automating Verification by Functional Abstraction at the System Level
Theorem Proving in Higher Order Logics (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 Logics (TPHOL)
|
|
|
|
 
|
[ScKK94h]
K. Schneider and T. Kropf and R. Kumar
Hardware-Verifikation braucht mehr als Model-Checking
Anwendung formaler Methoden im Systementwurf
|
|
|
|
 
|
[ZiCu94a]
R. Ziller and J. Cury
On the Supremal Lm-Closed and L-Controllable Sublanguages of a Given Language
Conference on Analysis and Optimization of Systems - Discrete Event Systems
|
|
|
|
 
|
[ZiCu94b]
R. Ziller and J. Cury
On the Supremal L-controllable Sublanguage of a non Prefix-Closed Language
Anais do 10. Congresso Brasileiro de Automática e 6. Congresso Latino-Americano de Controle Automático
|
|
|
|
 
|
[AlSZ93]
J. Altmeyer and B. Schürmann and G. Zimmermann
Three-Phase Chip Planning - Strategy and Flow Control
Technical Report
|
|
|
|
 
|
[HeNZ93]
W. Hebgen and P. Nuhn and G. Zimmermann
RETO: an Optimal Clocking Algorithm for Digital synchronous Circuits
Technical Report
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[MiZi93]
G. Mittelhäußer and G. Zimmermann
Segmentierung von MR-Volumendaten mit Bereichswachstumsverfahren
DAGM-Symposium
|
|
|
|
 
|
[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)
|
|
|
|
 
|
[Zill93]
R. Ziller
A Abordagem Ramadge-Wonham no Controle de Sistemas a Eventos Discretos: Contribuições à Teoria
Master Thesis
|
|
|
|
 
|
[Zimm93]
G. Zimmermann
From Computer Aided Design to the Design of Computer Aids
Technical Report
|
|
|
|
 
|
[GlZi92]
K. Glasmacher and G. Zimmermann
Chip Assembly in the PLAYOUT VLSI Design System
European Design Automation Conference (EURO-DAC)
|
|
|
|
 
|
[KrKS92]
T. Kropf and R. Kumar and K. Schneider
Bridging the Gap between Hardware-Verification and Design
IFIP World Conference
|
|
|
|
 
|
[ScAZ92]
B. Schürmann and J. Altmeyer and G. Zimmermann
Three-phase chip planning - an improved top-down chip planning strategy
International Conference on Computer-Aided Design (ICCAD)
|
|
|
|
 
|
[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 Logics (TPHOL)
|
|
|
|
 
|
[ScKK92c]
K. Schneider and R. Kumar and T. Kropf
Modelling generic Hardware Structures by Abstract Datatypes
Theorem Proving in Higher Order Logics (TPHOL)
|
|
|
|
 
|
[ScSZ92]
M. Schütze and B. Schürmann and G. Zimmermann
Abbildung eines CAD-Datenmodells auf das kommerzielle objektorientierte Datenbanksystem GemStone
Datenbank Rundbrief
|
|
|
|
 
|
[ScZi92]
B. Schürmann and G. Zimmermann
Estimation of Wiring Area for Hierarchical Design
Technical Report
|
|
|
|
 
|
[GlHZ91]
K. Glasmacher and A. Hess and G. Zimmermann
A Genetic Algorithm for Global Improvement of Macrocell Layouts
International Conference on Computer Design: VLSI in Computer & Processors (ICCD)
|
|
|
|
 
|
[KuKS91a]
R. Kumar and T. Kropf and K. Schneider
Integrating a First-Order Automatic Prover in the HOL Environment
Theorem Proving in Higher Order Logics (TPHOL)
|
|
|
|
 
|
[KuKS91b]
R. Kumar and T. Kropf and K. Schneider
First Steps Towards Automating Hardware Proofs in HOL
Theorem Proving in Higher Order Logics (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)
|
|
|
|
 
|
[ScZi91]
F. Schreiner and G. Zimmermann
Efficient Production System Execution on the PESA Architecture
International Conference on Parallel Processing (ICPP)
|
|
|
|
 
|
[Schn91]
K. Schneider
Ein Sequenzenkalkül für HOL
Master Thesis
|