|
|
|
|
|
[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 |
|
|
|
|
[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 Logic (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) |
|
|
|
|
|
[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 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) |
|
|
|
|
|
[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 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 |
|
|
|
|
|
[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 |
|
|
|
|
|
[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, (AKA) Verlag |
|
|
|
|
|
[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 Logic (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 |
||
|
|
|
|
[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) |
|
|
|
|
|
[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) |
|
|
|
|
[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) |
|
|
|
|
|
[QZBK00] S. Queins and G. Zimmermann and M. Becker and M. Kronenburg and C. Peper and R. Merz and J. Schäfer The Light Control Case Study: Problem Description Journal of Universal Computer Science (J.UCS) |
|
|
|
|
|
[Schn00] K. Schneider A Verified Hardware Synthesis for Esterel Workshop on Distributed and Parallel Embedded Systems (DIPES) |
|
|
|
|
[Zill00] R. Ziller Microprocessadores: Conceitos Importantes publisher |
|
|
|
|
[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 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 |
|
|
|
|
[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 |
|
|
|
|
[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 |
|
|
|
|
[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 |
|
|
|
|
|
[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 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) |
|
|
|
|
[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 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) |
|
|
|
|
[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 |
|
|
|
[Zimm90] G. Zimmermann VLSI layout synthesis Congress of the Brazilian Society of Microelectronics (SBMICRO) |
||
|
|
|
[Zimm90a] G. Zimmermann VLSI area estimation tolerances - Shape function generation vs. floorplanning Euro ASIC |
|
|
|
|
[SiZi89] E. Siepmann and G. Zimmermann An Object-Oriented Datamodel for the VLSI Design System PLAYOUT Design Automation Conference (DAC) |
|
|
|
|
[Zimm89] G. Zimmermann PLAYOUT - A Hierarchical Design System Information Processing, IFIP World Computer Congress |
|
|
|
[MeZi88] K. Mehlhorn and G. Zimmermann SFB 124: VLSI-Entwurfsmethoden und Parallelität Jahrestagung der Gesellschaft für Informatik: Vernetzte und komplexe Informatik-Systeme |
||
|
|
|
[ScZi88] F. Schreiner and G. Zimmermann Parallelism in the PESA I Multiprocessor International Conference on Fifth Generation Computer Systems (FGCS) |
||
|
|
|
[ScZi88a] F. Schreiner and G. Zimmermann Parallelism in the PESA I Multiprocessor Jahrestagung der Gesellschaft für Informatik: Vernetzte und komplexe Informatik-Systeme |
||
|
|
|
|
[Zimm88] G. Zimmermann A New Area and Shape Function Estimation Technique for VLSI Layouts Design Automation Conference (DAC) |
|
|
|
|
[Zimm88a] G. Zimmermann PLAYOUT - A Hierarchical Layout System Jahrestagung der Gesellschaft für Informatik: Vernetzte und komplexe Informatik-Systeme |
|
|
|
[ScZi87] F. Schreiner and G. Zimmermann PESA-I A Parallel Architecture for Production Systems International Conference on Parallel Processing (ICPP) |
|
|
|
|
[Zimm81] G. Zimmermann Computer Aided Synthesis of Digital Systems Computer Hardware Description Languages and Their Applications |
|
|
|
[Zimm80] G. Zimmermann MDS- the MIMOLA design method Digital Systems |
|
|
|
|
[Zimm79] G. Zimmermann The MIMOLA Design System: A Computer-Aided Processor Design Method Design Automation Conference (DAC) |
|
|
|
[Zimm76] G. Zimmermann Eine Methode zum Entwurf von Digitalrechnern mit der Programmiersprache MIMOLA Jahrestagung der Gesellschaft für Informatik |
|