| [1] |
Prakash M. Peranandam, Pradeep K. Nalla, Roland J. Weiss, Jürgen Ruf,
Thomas Kropf, and Wolfgang Rosenstiel.
Overlap reduction in symbolic system traversal.
In IEEE International High Level Design Validation and Test
Workshop 2005 (HLDVT 05), November 2005. |
| [2] |
Roland J. Weiss, Jürgen Ruf, Thomas Kropf, and Wolfgang Rosenstiel.
Efficient and customizable integration of temporal properties into
systemc.
Forum on Specification and Design Languages (FDL'05), September
2005. |
| [3] |
Roland J. Weiss, Jürgen Ruf, Thomas Kropf, and Wolfgang Rosenstiel.
Symbolic model checking and simulation with temporal assertions.
In Pierre Boulet, editor, Advances in Design and Specification
Languages for SoCs. Springer, September 2005. |
| [4] |
Djones Lettnin, Roland J. Weiss, Axel Braun, Jürgen Ruf, and Wolfgang
Rosenstiel.
Temporal properties verification of system level design.
In Workshop: Object Oriented Software Design for Real Time and
Embedded Computer Systems, September 2005. |
| [5] |
Pradeep K. Nalla, Roland J. Weiss, Prakash Peranandam, Juergen Ruf, Thomas
Kropf, and Wolfgang Rosenstiel.
Symbolic bounded property checking in parallel.
In 4th International Workshop on Parallel and Distributed
Methods in VerifiCation, Electronic Notes in Theoretical Computer Science.
Elsevier, 2005. |
| [6] |
Pradeep K. Nalla, Roland J. Weiss, Jürgen Ruf, Thomas Kropf, and Wolfgang
Rosenstiel.
Parallel bounded property checking with SymC.
In Wolfgang Ecker, editor, Modellierung und Verifikation, 8.
GI/ITG/GMM Workshop, 2005. |
| [7] |
Prakash M. Peranandam, Roland J. Weiss, Jürgen Ruf, Thomas Kropf, and
Wolfgang Rosenstiel.
Dynamic guiding of bounded property checking.
In IEEE International High Level Design Validation and Test
Workshop 2004 (HLDVT 04), November 2004. [ .pdf ] |
| [8] |
Stephan Flake, Wolfgang Müller, Ulrich Pape, and Jürgen Ruf.
Specification and formal verification of temporal properties of
production automation systems.
In Ehrig et. al., editor, Integration of Software Specification
Techniques for Applications in Engineering, volume 3147 of Lecture
Notes in Computer Science, pages 206-226. Springer, September 2004. |
| [9] |
Jürgen Ruf, Roland J. Weiss, Thomas Kropf, and Wolfgang Rosenstiel.
Modeling and formal verification of production automation systems.
In Ehrig et. al., editor, Integration of Software Specification
Techniques for Applications in Engineering, volume 3147 of Lecture
Notes in Computer Science, pages 541-566. Springer, September 2004. [ .pdf ] |
| [10] |
P. Peranandam, R. Weiss, J. Ruf, and T. Kropf.
Transactional level verification and coverage metrics by means of
symbolic simulation.
In Methoden und Beschreibungssprachen zur Modellierung und
Verifikation von Schaltungen und Systemen. GI/ITG/GMM Workshop, Shaker
Verlag, February 2004. [ .ps.gz | .pdf ] |
| [11] |
Jürgen Ruf and Thomas Kropf.
Symbolic verification and analysis of discrete timed systems.
Journal on Formal Methods in System Design, 23(1):67-108, July
2003. |
| [12] |
J. Ruf and P. Peranandam.
Bounded property checking with symbolic simulation.
In Methoden und Beschreibungssprachen zur Modellierung und
Verifikation von Schaltungen und Systemen, pages 209-218. GI/ITG/GMM
Workshop, Shaker Verlag, February 2003. |
| [13] |
Jürgen Ruf, Prakash M. Peranandam, Thomas Kropf, and Wolfgang Rosenstiel.
Bounded property checking with symbolic simulation.
In Forum on Specification and Design Languages 2003, 2003. |
| [14] |
J. Ruf and T. Kropf.
Symbolic verification and analysis of discrete timed systems.
Formal Methods in System Design, 2003. |
| [15] |
Andreas Krebs and Jürgen Ruf.
Optimized temporal logic compilation.
Journal of Universal Computer Science, Special Issue on Tools
for System Design and Verification, 9(2):120-137, 2003. |
| [16] |
J. Ruf and T. Kropf.
Formal data analysis of timed finite state systems.
In Euro Micro Conference on Real-Time Systems (ECRTS). IEEE
Computer Society Press, June 2002. |
| [17] |
J. Ruf and T. Kropf.
Formal data analysis of timed finite state systems.
In 14th Euromicro Conference on Real-Time Systems (ECRTS),
Vienna, Austria, June 2002. IEEE Computer Society Press. |
| [18] |
Jürgen Ruf and Thomas Kropf.
Combination of simulation and formal verification.
In J. Ruf, editor, Methoden und Beschreibungssprachen zur
Modellierung und Verifikation von Schaltungen und Systemen, pages 134-143,
Tübingen, March 2002. GI/ITG/GMM, Shaker Verlag. |
| [19] |
Stephan Flake, Wolfgang Müller, and Jürgen Ruf.
Structured english for model checking specification.
In Klaus Waldschmidt and Christoph Grimm, editors, Methoden und
Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und
Systemen, 3. GI/ITG/GMM Workshop, pages 99-108. VDE Verlag, 2002. |
| [20] |
Jochen Klose, Thomas Kropf, and Jürgen Ruf.
A visual approach to validating system level designs.
In 15th International Symposium on Systems Synthesis, pages
186-191. ACM Press, 2002. |
| [21] |
A. Krebs and J. Ruf.
Optimized temporal logic compilation.
In W. Reif D. Haneberg, G. Schellhorn, editor, 5th Workshop on
Tools for System Design and verification (FM-TOOLS), pages 77-82, 2002. |
| [22] |
J. Klose, J. Ruf, and T. Kropf.
A visual approach to validating system level designs.
In 15.th International Symposioum on System Synthesis (ISSS),
pages 186 - 191, Kyoto, Japan, 2002. IEEE Computer Society Press. |
| [23] |
S. Flake, W. Müller, U. Pape, and J. Ruf.
Analyzing timing constraints in flexible manufacturing systems.
In Intelligent Manufacturing Systems, Dubai, March 2001. |
| [24] |
J. Ruf.
Data analysis of timed finite state systems.
In Methoden und Beschreibungssprachen zur Modellierung und
Verifikation von Schaltungen und Systemen, Meißen, Germany, March 2001. |
| [25] |
Jürgen Ruf, Dirk W. Hoffmann, Thomas Kropf, and Wolfgang Rosenstiel.
Simulation-guided property checking based on a multi-valued
AR-automata.
In Wolfgang Nebel and Ahmed Jerraya, editors, Design, Automation
and Test in Europe 2001, pages 742-748. IEEE Press, 2001. |
| [26] |
W. Reif, J. Ruf, G. Schellhorn, and T. Vollmer.
Correctness of efficient real-time model checking.
Journal on Universal Computer Science (www.jucs.org), 2001. |
| [27] |
J. Ruf.
RAVEN: Real-time analyzing and verification environment.
Journal on Universal Computer Science (www.jucs.org), 2001. |
| [28] |
J. Ruf, D. W. Hoffmann, T. Kropf, and W. Rosenstiel.
Simulation-guided property checking based on multi-valued
AR-automata.
In Design Automation and Test in Europe (DATE). IEEE Conmputer
Society Press, Los Alamitos, 2001. |
| [29] |
W. Müller, J. Ruf, D. W. Hoffmann, J. Gerlach, T. Kropf, and W. Rosenstiel.
Formal semantics of behavioral SystemC.
In Design Automation and Test in Europe (DATE). IEEE Conmputer
Society Press, Los Alamitos, 2001. |
| [30] |
W. Reif, J. Ruf, G. Schellhorn, and T. Vollmer.
Do you trust your model checker?
In S. Johnson and W. A. Hunt, editors, Formal Methods in
Computer Auded Design (FMCAD), Lecture Notes in Computer Science, Austin,
TX, November 2000. Springer-Verlag. |
| [31] |
J. Ruf, D. W. Hoffmann, T. Kropf, and W. Rosenstiel.
Checking temporal properties under simulation of executable
specifications.
In Workshop on High Level Description, Test and Verification
(HLDTV 2000). IEEE Computer Society Press, Los Alamitos, November 2000. |
| [32] |
J. Ruf, D. W. Hoffmann, T. Kropf, and W. Rosenstiel.
Simulation based validation of FLTL formulas in executable system
descriptions.
In R. Seepold, editor, Forum on Design Languages (FDL 2000),
pages 311-319, Tübingen, Germany, September 2000. Sig.-VHDL and ECSI. |
| [33] |
D. W. Hoffmann and T. Kropf.
Efficient design error correction of digital circuits.
In Proceedings of the 18th IEEE Internation Conference on
Computer Design (ICCD). IEEE, September 2000. |
| [34] |
J. Ruf and T. Kropf.
Analyzing real-time systems.
In P. Marwedel and I. Bolsens, editors, Design Automation and
Test in Europe (DATE), pages 243-248, Los Alamitos, CA, March 2000. IEEE
Compter Society Press. |
| [35] |
J. Ruf.
A toolset for the symbolic examination of finite state transition
systems.
In K. Waldschmidt and C. Grimm, editors, Methoden und
Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und
Systemen, Forschungs-Report, pages 69-78, Berlin, Germany, February 2000.
VDE Verlag. |
| [36] |
J. Ruf.
Techniken zur Modellierung und Verifikation von
Echtzeitsystemen.
Logos-Verlag, Berlin, 2000. |
| [37] |
J. Ruf.
Raven: Real-time analyzing and verification environment.
Technical report, WSI 2000-3, University of Tübingen, Germany,
2000. |
| [38] |
J. Ruf.
Formal verification of timing properties on a holonic material
transport system.
Technical report, WSI 2000-2, University of Tübingen, Germany,
2000. |
| [39] |
Jürgen Ruf.
Techniken zur Modellierung und Verifikation von
Echtzeitsystemen.
Logos-Verlag, Berlin, 2000. |
| [40] |
D. W. Hoffmann and T. Kropf.
Exploiting hierarchy for multiple error correction of combinational
circuits.
In Proceedings of the 3rd Design, Automation, and Test
Conference in Europe (DATE), Paris, France, 2000. IEEE. |
| [41] |
D. W. Hoffmann and T. Kropf.
Can automatic design error correction be applied to large circuits?
In Proceedings of the Symposium on Digital Systems Design
(DSD), Maastricht, The Netherlands, 2000. |
| [42] |
D. W. Hoffmann, J. Ruf, T. Kropf, and W. Rosenstiel.
Simulation meets verification - verifying temporal properties in
SystemC.
In Proceedings of the Symposium on Digital Systems Design
(DSD), Maastricht, The Netherlands, 2000. |
| [43] |
D. W. Hoffmann and T. Kropf.
Automatic error correction of tri-state circuits.
In Proceedings of the 17th IEEE Internation Conference on
Computer Design (ICCD), Austin, TX, October 1999. IEEE. |
| [44] |
K. Schneider and D. Hoffmann.
A HOL conversion for translating linear time temporal logic to
ω-automata.
In Y. Bertot, G. Dowek, Ch. Paulin-Mohring, and L. Théry,
editors, Higher Order Logic Theorem Proving and its Applications,
Lecture Notes in Computer Science, Nice, France, September 1999. Springer
Verlag. |
| [45] |
J. Ruf and T. Kropf.
Modeling and checking networks of communicating real-time processes.
In L. Pierre and T. Kropf, editors, Correct Hardware Design and
Verification Methods (CHARME), volume 1703 of Lecture Notes in Computer
Science, pages 256-279, Bad Herrenalb, Germany, September 1999.
Springer-Verlag. |
| [46] |
D. W. Hoffmann and T. Kropf.
Automatic error correction of large circuits using boolean
decomposition and abstraction.
In Proceedings of the Conference on Correct Hardware Design and
Verification Methods (CHARME), Bad Herrenalb, Germany, September 1999. |
| [47] |
T. Kropf, J. Gerlach, J. Haufe, M. Kortke, and M. Weiß.
Methodischer HW/SW-Entwurf des GSM
Sprachtranscodec-Algorithmus.
Informationstechnik und Technische Informatik (it&ti),
(2):46-50, March 1999. |
| [48] |
J. Ruf and T. Kropf.
Modeling real-time systems with i/o-interval structures.
In Methoden und Beschreibungssprachen zur Modellierung und
Verifikation von Schaltungen und Systemen, pages 91-100. GI/ITG/GMM
Workshop, Shaker Verlag, March 1999. |
| [49] |
D. W. Hoffmann and T. Kropf.
Using BDD-based decomposition for automatic error correction of
combinatorial circuits.
Technical Report 6/99, University of Karlsruhe, March 1999. |
| [50] |
M. Huhn, K. Schneider, Th. Kropf, and G. Logothetis.
Verifying imprecisely working arithmetic circuits.
In Design, Automation and Test in Europe (DATE' 98). IEEE
Computer Society Press, February 1999. |
| [51] |
D. W. Hoffmann and T. Kropf.
Automatic error correction of large circuits using boolean
decomposition and abstraction.
submitted to CHARME99, February 1999.
temporarily available at http://goethe.ira.uka.de/~hoff. |
| [52] |
Jürgen Ruf and Thomas Kropf.
Modeling and checking networks of communicating real-time process.
In Laurence Pierre and Thomas Kropf, editors, 10th IFIP WG 10.5
Advanced Research Working Conference on Correct Hardware Design and
Verification Methods, volume 1703 of Lecture Notes in Computer
Science, pages 256-279. Springer, 1999. |
| [53] |
D. W. Hoffmann and T. Kropf.
AC/3 V1.00 - A Tool for Automatic Error Correction of
Combinatorial Circuits.
Technical Report 5/99, University of Karlsruhe, 1999.
available at http://goethe.ira.uka.de/~hoff. |
| [54] |
J. Ruf.
Techniken zur Modellierung und Verifikation von
Echtzeitsystemen.
Lecture Notes in Computer Science. Logos Verlag, Berlin, Germany,
1999. |
| [55] |
D. W. Hoffmann and T. Kropf.
AC/3 V3.0 - A tool for automatic error correction of
combinational circuits.
User manual, 1999. |
| [56] |
Jürgen Ruf and Thomas Kropf.
Using MTBDDs for composition and model checking of real-time
systems.
In FMCAD 1998. Springer, November 1998. |
| [57] |
W. Grass, T. Kropf, and M. Mutz.
Formale Methoden bei der Spezifikation von Hardware.
Informationstechnik und Technische Informatik (it&ti), (3),
June 1998. |
| [58] |
R. Reetz, K. Schneider, and T. Kropf.
Formal specification in VHDL for formal hardware verification.
In Design, Automation and Test in Europe (DATE' 98). IEEE
Computer Society Press, February 1998. |
| [59] |
T. Kropf, J. Ruf, K. Schneider, and M. Wild.
A synchronous language for modeling and verifying real time and
embedded systems.
In GI/ITG/GME Workshop: Methoden des Entwurfs und der
Verifikation digitaler Schaltungen und Systeme und Beschreibungssprachen und
Modellierung von Schaltungen und Systemen, pages 11-20.
HNI-Verlagsschriften, ISBN 3-931466-35-3, 1998. |
| [60] |
T. Kropf, J. Ruf, K. Schneider, and M. Wild.
The synchronous system description language PURR.
In Open Project Workshop on System Design Automation (SDA98),
Dresden, Germany, 1998. |
| [61] |
J. Ruf and T. Kropf.
Using MTBDDs for composition and model checking of real-time
systems.
Technical Report SFB358-C2-1/98, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, January 1998.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-1-98.ps.gz. |
| [62] |
J. Ruf and T. Kropf.
Using MTBDDs for discrete timed symbolic model checking.
Multiple-Valued Logic - An International Journal, 1998.
Special Issue on Decision Diagrams. |
| [63] |
D.W. Hoffmann and T. Kropf.
Verification of a GF(2m) Multiplier-Circuit for Digital
Signal Processing.
Technical Report 22/98, University of Karlsruhe, 1998.
available at http://goethe.ira.uka.de/~hoff. |
| [64] |
J. Ruf and T. Kropf.
Symbolic model checking for a discrete clocked temporal logic with
intervals.
In E. Cerny and D.K. Probst, editors, Conference on Correct
Hardware Design and Verification Methods (CHARME), pages 146-166, Montreal,
Canada, October 1997. IFIP WG 10.5, Chapman and Hall. |
| [65] |
T. Kropf.
Formal Hardware Verification - Methods and Systems in
Comparison, volume 1287 of Lecture Notes in Computer Science.
Springer Verlag, state of the art report edition, August 1997. |
| [66] |
K. Schneider and T. Kropf.
The C@S system: Combining proof strategies for system verification.
In T. Kropf, editor, Formal Hardware Verification - Methods and
Systems in Comparison, volume 1287 of Lecture Notes in Computer
Science, pages 248-329. Springer Verlag, state of the art report edition,
August 1997. |
| [67] |
T. Kropf.
Hardware-Verifikation - Verfahren und Werkzeuge zum
Entwurf korrekter Schaltungen und Systeme.
habilitation thesis (in German), May 1997. |
| [68] |
R. Reetz, K. Schneider, and T. Kropf.
Formale Spezifikation und Verifikation mit VHDL.
In R. Hagelauer, editor, GI/ITG/GMM Workshop Methoden des
Entwurfs und der Verifikation digitaler Systeme, pages 97-108, Linz,
Österreich, April 1997. |
| [69] |
J. Ruf and T. Kropf.
Symbolic model checking for a discrete clocked temporal logic with
intervals.
Technical Report SFB358-C2-1/97, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, April 1997.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-1-97.ps.gz. |
| [70] |
T. Kropf and J. Ruf.
Using MTBDDs for discrete timed symbolic model checking.
In European Design and Test Conference (EDTC), pages 182-187,
Paris, France, March 1997. IEEE Computer Society Press (Los Alamitos,
California). |
| [71] |
R. Reetz, K. Schneider, and T. Kropf.
Verificationbench: Formale Spezifikation in VHDL.
In D. Monjau, editor, GI/ITG/GME Workshop
Hardwarebeschreibungssprachen und Modellierungsparadigmen, pages 94-103,
Holzhau, Deutschland, February 1997. |
| [72] |
D. W. Hoffmann.
Kompositionale Verfahren für die Zeitbehaftete
Modellprüfung.
Master's thesis, Universität Karlsruhe, Karlsruhe, 1997. |
| [73] |
J. Ruf and T. Kropf.
A new algorithm for discrete timed symbolic model checking.
In O. Maler, editor, Hybrid and Real-Time Systems,
pages 18-32, Grenoble, France, 1997. Springer Verlag, LNCS 1201. |
| [74] |
K. Schneider and T. Kropf.
Verifying Hardware Correctness by Combining Theorem
Proving and Model Checking.
Technical Report SFB358-C2-2/96, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, December 1996.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-2-96.ps.gz. |
| [75] |
K. Schneider and T. Kropf.
A unified approach for combining different formalisms for hardware
verification.
In M. Srivas and A. Camilleri, editors, International Conference
on Formal Methods in Computer Aided Design (FMCAD), volume 1166 of
Lecture Notes in Computer Science, pages 202-217, Palo Alto, USA, November
1996. Springer Verlag. |
| [76] |
R. Reetz and T. Kropf.
Evaluating possibilities for formally sound simulation and
verification of VHDL.
In S. Singh and M. Sheeran, editors, Workshop on Designing
Correct Circuits, Electronic Workshops in Computing, Baastad, Sweden,
September 1996. Springer Verlag. |
| [77] |
T. Kropf and J. Ruf.
Using MTBDDs for discrete timed symbolic model checking.
Technical Report SFB358-C2-5/96, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, August 1996.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-5-96.ps.gz. |
| [78] |
R. Reetz and T. Kropf.
Principles of formal verification tools for VHDL.
In W. Ecker, editor, SIG-VHDL Spring '96 Working Conference,
pages 133-144, Dresden, Germany, May 1996. Shaker Verlag. |
| [79] |
J. Frößl, J. Gerlach, and T. Kropf.
An Efficient Algorithm for Real-Time Model Checking.
In European Design and Test Conference (EDTC), pages 15-21,
Paris, France, March 1996. IEEE Computer Society Press (Los Alamitos,
California). |
| [80] |
J. Frößl, T. Kropf, and K. Schneider.
Bewertung temporaler Logiken in der Hardware-Verifikation.
In B. Straube and J. Schoenherr, editors, GI/ITG/GME Workshop
Methoden des Entwurfs und der Verifikation digitaler Systeme, pages 31-40.
Shaker Verlag, March 1996. |
| [81] |
J. Ruf.
Untersuchung von erweiterten zellularautomaten mit variabler
nachbarschaft.
Master's thesis, Universität Karlsruhe, March 1996. |
| [82] |
K. Schneider and T. Kropf.
A unified approach for combining different formalisms for hardware
verification.
In B. Straube and J. Schoenherr, editors, GI/ITG/GME Workshop
Methoden des Entwurfs und der Verifikation digitaler Systeme, pages
131-141. Shaker Verlag, March 1996. |
| [83] |
J. Frößl, T. Kropf, and K. Schneider.
Einsatz temporaler Logik in der Hardwareverifikation.
Technical Report SFB358-C2-4/96, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, January 1996.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-4-96.ps.gz. |
| [84] |
R. Reetz and T. Kropf.
Evaluating Possibilities for Formally Sound Simulation and
Verification of VHDL.
Technical Report SFB358-C2-1/96, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, January 1996.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-1-96.ps.gz. |
| [85] |
K. Schneider and T. Kropf.
Verifying Hardware Correctness by Combining Theorem
Proving and Model Checking.
Technical Report SFB358-C2-5/95, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, December 1995.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-5-95.ps.gz. |
| [86] |
J. Frößl, J. Gerlach, and T. Kropf.
Symbol Model Checking for Real-Time Circuits and
Specifications.
In ACM International Workshop on Timing Issues in the
Specification and Synthesis of Digital Systems (TAU), Washington, Seattle,
November 1995. |
| [87] |
R. Reetz and T. Kropf.
A Flowgraph Semantics of VHDL: Toward a VHDL
Verification Workbench in HOL.
Formal Methods in System Design, 7(1/2):73-100, August 1995.
Kluwer Academic Publishers, ISSN: 0925-9856. |
| [88] |
T. Kropf.
VLSI-Entwurf - Vorgehen, Methoden, Automatisierung,
volume 17 of Thomson's Aktuelle Tutorien.
International Thomson Publishing, Bonn, April 1995. |
| [89] |
J. Frößl and T. Kropf.
Verifying Real-Time Properties of MOS-Transistor
Circuits.
In European Design and Test Conference (EDTC), pages 314-319,
Paris, March 1995. IEEE Computer Society Press. |
| [90] |
R. Reetz and T. Kropf.
A Flowgraph Semantics of VHDL: A Basis for Hardware
Verification with VHDL.
In C. Delgado Kloos and P.T. Breuer, editors, Formal Semantics
for VHDL, volume 307 of The Kluwer international series in
engineering and computer science, chapter 7, pages 205-238. Kluwer Academic
Publishers, Madrid, Spain, March 1995. |
| [91] |
K. Schneider, T. Kropf, and T. Thiessenhusen.
Spezifikation und Verifikation systolischer Felder mit Logik
höherer Ordnung.
In W. Grass and M. Mutz, editors, GI/ITG Workshop Anwendung
formaler Methoden beim Entwurf von Hardwaresystemen, Berichte aus der
Informatik, pages 71-78, Passau, March 1995. GI/ITG, Shaker Verlag. |
| [92] |
J. Frößl and T. Kropf.
Layoutabhängige formale Verifikation von
MOS-Transistorschaltungen durch Model-Checking.
In International Scientific Kolloquium, Technical University
Ilmenau, 1995. |
| [93] |
O. Haberl and Th. Kropf.
A Hierarchical Self Test Methodology for Chips, Boards
and Systems.
Journal of Electronic Testing: Theory and Applications (JETTA),
6:85-106, 1995. |
| [94] |
K. Schneider, T. Kropf, and T. Thiessenhusen.
Spezifikation und Verifikation systolischer Felder mit Logik
höherer Ordnung.
Technical Report SFB358-A1C2-1/95, Universität Karlsruhe,
Institut für Rechnerentwurf und Fehlertoleranz, January 1995.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-A1C2-1-95.ps.gz. |
| [95] |
J. Frößl and T. Kropf.
Layout-driven Formal Verification of MOS Transistor
Circuits.
Technical Report SFB358-C2-12/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, October 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-12-94.ps.gz. |
| [96] |
T. Kropf, K. Schneider, and R. Kumar.
A Formal Framework for High Level Synthesis.
In T. Kropf and R. Kumar, editors, International Conference on
Theorem Provers in Circuit Design (TPCD), volume 901 of Lecture Notes
in Computer Science, pages 223-238, Bad Herrenalb, Germany, September 1994.
Springer-Verlag.
published 1995. |
| [97] |
T. Kropf.
Benchmark-Circuits for Hardware-Verification.
In T. Kropf and R. Kumar, editors, International Conference on
Theorem Provers in Circuit Design (TPCD), volume 901 of Lecture Notes
in Computer Science, pages 1-12, Bad Herrenalb, Germany, September 1994.
Springer-Verlag.
published 1995. |
| [98] |
R. Reetz and T. Kropf.
Simplifying Deep Embedding: A Formalised Code
Generator.
In T.F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and its Applications, volume 859 of Lecture Notes in
Computer Science, pages 378-390, Malta, September 1994. Springer-Verlag. |
| [99] |
R. Reetz and T. Kropf.
Simplifying Deep Embedding: Generating Formal Compilers
in HOL.
Technical Report SFB358-C2-7/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, September 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-7-94.ps.gz. |
| [100] |
R. Reetz and T. Kropf.
A Flowgraph Semantics of VHDL: Toward a VHDL verification
workbench in HOL.
Technical Report SFB358-C2-11/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, September 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-11-94.ps.gz. |
| [101] |
K. Schneider, R. Kumar, and T. Kropf.
Automating Verification by Functional Abstraction at the
System Level.
In T.F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and its Applications, volume 859 of Lecture Notes in
Computer Science, pages 391-406, Malta, September 1994. Springer-Verlag. |
| [102] |
R. Reetz and T. Kropf.
Formalisierung eines Flußgraphmodells in Logik höherer
Ordnung und dessen Anwendung in der Hardware-Verifikation.
In D. Monjau, editor, Rechnergestützter Entwurf und
Architektur mikroelektronischer Systeme, pages 193-202, Oberwiesenthal,
Germany, May 1994. Society for Computer Science (GI) e.V. |
| [103] |
J. Frößl and T. Kropf.
Verifikation des Zeitverhaltens von
MOS-Transistor-Schaltungen durch Model Checking.
In GI/ITG Workshop Anwendung formaler Methoden im
Systementwurf. GI/ITG, Universität Frankfurt, Interner Bericht Nr. 6/94,
March 1994. |
| [104] |
O.F. Haberl and T. Kropf.
Self Testable Boards with Standard IEEE 1149.5 Module
Test and Maintenance (MTM).
In European Design and Test Conference (EDTC), pages 220-226,
Paris, France, March 1994. IEEE. |
| [105] |
K. Schneider, T. Kropf, and R. Kumar.
Control-Path Oriented Verification of Sequential Generic
Circuits with Control and Data Path.
In European Design and Test Conference (EDTC), pages 648-652,
Paris, France, March 1994. IEEE Computer Society Press. |
| [106] |
K. Schneider, T. Kropf, and R. Kumar.
Hardwareverifikation braucht mehr als Model-Checking.
In H. Eveking, editor, GI/ITG Workshop Anwendung formaler
Methoden im Systementwurf. GI/ITG, Universität Frankfurt, Interner
Bericht Nr. 6/94, March 1994. |
| [107] |
J. Frößl and T. Kropf.
A New Model to Uniformly Represent the Function and
Timing of MOS Transistor Circuits and its Application to VHDL
Simulation.
In European Design and Test Conference (EDTC), pages 343-348,
1994. |
| [108] |
J. Frößl and T. Kropf.
A new model to uniformly represent the function and timing of MOS
transistor circuits and its application to VHDL simulation.
Technical Report SFB358-C2-2/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-2-94.ps.gz. |
| [109] |
J. Frößl and T. Kropf.
Verifikation des Zeitverhaltens von
MOS-Transistor-Schaltungen durch Model Checking.
Technical Report SFB358-C2-3/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1994. |
| [110] |
T. Kropf, K. Schneider, and R. Kumar.
A formal framework for high-level synthesis.
Technical Report SFB358-C2-5/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-5-94.ps.gz. |
| [111] |
T. Kropf.
Benchmark-circuits for hardware-verification.
Technical Report SFB358-C2-4/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-4-94.ps.gz. |
| [112] |
R. Reetz and T. Kropf.
A Flowgraph Model for Formalizing the Semantics of VHDL
in HOL.
In C. Delgado Kloos, editor, EuroFORM workshop, Las Navas del
Marqué, Ávila, Spain, January 1994. Universidad Politécnica de
Madrid, Spain. |
| [113] |
R. Reetz and T. Kropf.
Simplifying Deep Embedding: A Formalised Code
Generator.
Technical Report SFB358-C2-8/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-8-94.ps.gz. |
| [114] |
R. Reetz and T. Kropf.
Formalisierung eines Flußgraphmodells in Logik höherer
Ordnung und dessen Anwendung in der Hardware-Verifikation.
Technical Report SFB358-C2-6/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-6-94.ps.gz. |
| [115] |
A. Schneider, B. Straube, K. Schneider, and T. Kropf.
Verifikation eines digitalen Netzwerkes mit Hilfe des
Beweissystems HOL.
Technical Report SFB358-C-1/94, FHG Dresden/Universität
Karlsruhe, Institut für Rechnerentwurf und Fehlertoleranz, 1994. |
| [116] |
K. Schneider, T. Kropf, and R. Kumar.
Accelerating Tableaux Proofs using Compact Representations.
Journal of Formal Methods in System Design, 5:145-176, 1994. |
| [117] |
K. Schneider, T. Kropf, and R. Kumar.
Why Hardware Verification Needs more than Model Checking.
In Higher Order Logic Theorem Proving and its Applications,
Malta, 1994. |
| [118] |
K. Schneider, T. Kropf, and R. Kumar.
Control-path oriented verification of sequential generic circuits
with control and data path.
Technical Report SFB358-C2-9/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-9-94.ps.gz. |
| [119] |
K. Schneider, T. Kropf, and R. Kumar.
Why hardware verification needs more than model checking.
Technical Report SFB358-C2-10/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-10-94.ps.gz. |
| [120] |
K. Schneider, R. Kumar, and T. Kropf.
Automating verification by functional abstraction at the system
level.
Technical Report SFB358-C2-13/94, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1994.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-13-94.ps.gz. |
| [121] |
K. Schneider, T. Kropf, and R. Kumar.
Kontrollpfad-orientierte Verifikation generischer Datenpfade.
In E.I.S.-Workshop (Entwurf integrierter Schaltungen), pages
249-256, Tübingen, November 1993. |
| [122] |
R. Reetz and T. Kropf.
Hardwarebeschreibungssprachen und formale Verifikation.
Technical Report SFB358-C2-4/93, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, September 1993.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-4-93.ps.gz. |
| [123] |
K. Schneider, R. Kumar, and T. Kropf.
Eliminating Higher-Order Quantifiers to Obtain Decision
Procedures for Hardware Verification.
In J.J. Joyce and C.-J.H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications, volume 780 of Lecture Notes in
Computer Science, pages 386-400, Vancouver, Canada, August 1993. University
of British Columbia, Springer-Verlag, published 1994. |
| [124] |
K. Schneider, R. Kumar, and T. Kropf.
Alternative Proof Procedures for Finite-State Machines in
Higher-Order Logic.
In J.J. Joyce and C.-J.H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications, volume 780 of Lecture Notes in
Computer Science, pages 213-227, Vancouver, Canada, August 1993. University
of British Columbia, Springer-Verlag, published 1994. |
| [125] |
T. Kropf, R. Kumar, and K. Schneider.
Embedding Hardware Verification within a Commercial Design
Framework.
In G.J. Milne and L. Pierre, editors, Conference on Correct
Hardware Design and Verification Methods (CHARME), volume 683 of
Lecture Notes in Computer Science, pages 242-257, Arles, France, May 1993.
IFIP WG10.2, Springer-Verlag. |
| [126] |
K. Schneider, R. Kumar, and T. Kropf.
Hardware-Verification using First Order BDDs.
In D. Agnew, L. Claesen, and R. Camposano, editors, IFIP
Conference on Computer Hardware Description Languages and their Applications
(CHDL), pages 35-52, Ottawa, Canada, April 1993. IFIP WG10.2, CHDL'93, IEEE
COMPSOC, Elsevier Science Publishers B.V., Amsterdam, Netherland. |
| [127] |
O.F. Haberl and T. Kropf.
A Chip for a Hierarchical Boundary-Scan Architecture.
In BIST-DFT Workshop, Charleston, South-Carolina, USA, March
1993. |
| [128] |
O.F. Haberl and T. Kropf.
Ein Chip zur Unterstützung des hierarchischen und
boundary-scan kompatiblen Selbsttests für Baugruppen und Systeme.
In Workshop Testmethoden und Zuverläßigkeit von
Schaltungen und Systemen, Holzau, Erzgebirge, March 1993. ITG/GI. |
| [129] |
R. Reetz and T. Kropf.
Ein formales Flußgraphmodell zur Integration von
Hardwarebeschreibungssprachen in die Hardware-Verifikation.
In T. Kropf, R. Kumar, and D. Schmid, editors, GI/ITG Workshop
Formale Methoden zum Entwurf korrekter Systeme, pages 49-60, Bad Herrenalb,
March 1993. GI/ITG, Universität Karlsruhe, Interner Bericht Nr. 10/93. |
| [130] |
T. Kropf, R. Kumar, and D. Schmid.
Workshop Formale Methoden zum Entwurf korrekter Systeme.
Technical Report SFB358-C2-3/93, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, February 1993.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-3-93.ps.gz. |
| [131] |
J. Frößl and T. Kropf.
A unified Model for the Boolean and Timing Behavior of
MOS Transistor Circuits.
In International Workshop on Power and Timing Modelling and
Optimization (PATMOS93), pages 86-99, La Grande Motte, France, 1993. |
| [132] |
J. Frößl and T. Kropf.
A unified model for the boolean and timing behavior of MOS
transistor circuits.
Technical Report SFB358-C2-5/93, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1993.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-5-93.ps.gz. |
| [133] |
T. Kropf, R. Kumar, and K. Schneider.
Embedding Hardware Verification within a Commercial Design
Framework.
Technical Report SFB358-C2-6/93, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1993.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-6-93.ps.gz. |
| [134] |
T. Kropf.
Ein einheitlicher Ansatz zur Verifikation und
Testerzeugung für digitale Schaltungen mit temporaler Logik,
volume 174 of Reihe 9: Elektronik.
VDI Verlag, Düsseldorf, 1993.
ISBN 3-18-147409-6. |
| [135] |
T. Kropf.
Hardware-verifikation.
Vorlesung im SS'93, 1993.
Institut für Rechnerentwurf und Fehlertoleranz, Universität
Karlsruhe. |
| [136] |
R. Kumar, K. Schneider, and T. Kropf.
Structuring and Automating Hardware Proofs in a
Higher-Order Theorem-Proving Environment.
International Journal of Formal System Design, pages 165-230,
1993. |
| [137] |
R. Kumar, K. Schneider, and T. Kropf.
Structuring and automating hardware proofs in a higher-order
theorem-proving environment.
Technical Report SFB358-C2-1/93, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1993.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-1-93.ps.gz. |
| [138] |
K. Schneider, T. Kropf, and R. Kumar.
Accelerating Tableaux Proofs using Compact Representations.
Technical Report SFB358-C2-2/93, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1993.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-2-93.ps.gz. |
| [139] |
K. Schneider, R. Kumar, and T. Kropf.
Hardware-Verification using First Order BDD's.
Technical Report SFB358-C2-7/93, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1993.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-7-93.ps.gz. |
| [140] |
K. Schneider, R. Kumar, and T. Kropf.
Alternative Proof Procedures for Finite-State Machines in
Higher-Order Logic.
Technical Report SFB358-C2-8/93, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1993.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-8-93.ps.gz. |
| [141] |
K. Schneider, R. Kumar, and T. Kropf.
Eliminating Higher-Order Quantifiers to Obtain Decision
Procedures for Hardware Verification.
Technical Report SFB358-C2-9/93, Universität Karlsruhe, Institut
für Rechnerentwurf und Fehlertoleranz, 1993.
ftp://goethe.ira.uka.de/pub/hvg/techreports/SFB358-C2-9-93.ps.gz. |
| [142] |
O.F. Haberl and T. Kropf.
HIST: A Methodology for the Automatic Insertion of a
Hierarchical Self-Test.
In International Test Conference (ITC), pages 732-741,
Baltimore, September 1992. |
| [143] |
T. Kropf, R. Kumar, and K. Schneider.
Bridging the gap between hardware-verification and design.
In IFIP World Conference, Madrid, September 1992. IFIP. |
| [144] |
K. Schneider, R. Kumar, and T. Kropf.
Efficient Representation and Computation of Tableau Proofs.
In L.J.M. Claesen and M.J.C. Gordon, editors, Higher Order Logic
Theorem Proving and its Applications, pages 39-58, Leuven, Belgium,
September 1992. North-Holland. |
| [145] |
K. Schneider, R. Kumar, and T. Kropf.
Modelling generic Hardware Structures by Abstract
Datatypes.
In L. Claesen and M.J.C. Gordon, editors, Higher Order Logic
Theorem Proving and its Applications, pages 419-429, Leuven, Belgium,
September 1992. IFIP TC10/WG10.2, Elsevier Science Publishers. |
| [146] |
O.F. Haberl and T. Kropf.
A Methodology for the Insertion of a Hierarchical and
Boundary-Scan Compatible Self-Test.
In IEEE VLSI Test Symposium, pages 37-42, Atlantic City,
New Jersey, April 1992. |
| [147] |
O.F. Haberl and T. Kropf.
A Chip Solution to Hierarchical and Boundary-Scan
Compatible Board Level BIST.
In Great Lakes Symposium on VLSI (GLS-VLSI), pages 16-21,
Kalamazoo, Michigan, February 1992. |
| [148] |
K. Schneider, R. Kumar, and T. Kropf.
The FAUST prover.
In D. Kapur, editor, Conference on Automated Deduction (CADE),
volume 607 of Lecture Notes in Computer Science, pages 766-770,
Saratoga Springs, New York, 1992. Springer-Verlag. |
| [149] |
O.F. Haberl, J. Frößl, and T. Kropf.
A self-testable boundary-scan compatible hardware implementation of
an extended DES algorithm.
In Workshop Secure Design and Test of Crypto-Chips, Gmunden,
Österreich, October 1991. IFIP WG 10.5. |
| [150] |
T. Kropf and H.-J. Wunderlich.
A Common Approach to Test Generation and
Hardware-Verification Based on Temporal Logic.
In International Test Conference (ITC), pages 57-66,
Nashville, October 1991. |
| [151] |
R. Kumar, T. Kropf, and K. Schneider.
Integrating a First-Order Automatic Prover in the HOL
Environment.
In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors,
Higher Order Logic Theorem Proving and its Applications, pages
170-176, Davis, California, August 1991. IEEE Computer Society, ACM SIGDA,
IEEE Computer Society Press. |
| [152] |
R. Kumar, T. Kropf, and K. Schneider.
First Steps Towards Automating Hardware Proofs in HOL.
In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors,
Higher Order Logic Theorem Proving and its Applications, pages
190-193, Davis, California, August 1991. IEEE Computer Society, ACM SIGDA,
IEEE Computer Society Press. |
| [153] |
K. Schneider, R. Kumar, and T. Kropf.
Structuring Hardware Proofs: First steps towards Automation
in a Higher-Order Environment.
In A. Halaas and P.B. Denyer, editors, International Conference
on Very Large Scale Integration (VLSI), pages 81-90, Edinburgh, Scotland,
August 1991. IFIP Transactions, North-Holland. |
| [154] |
K. Schneider, R. Kumar, and T. Kropf.
Automating most Parts of Hardware Proofs in HOL.
In K.G. Larsen and A. Skou, editors, Workshop on Computer Aided
Verification (CAV), volume 575 of Lecture Notes in Computer Science,
pages 365-375, Aalborg, July 1991. Springer-Verlag. |
| [155] |
T. Kropf and H.-J. Wunderlich.
A Unified Approach for Hardware Verification and Test
Generation.
In IEEE Workshop on Design for Testability, Vail, Colorado,
April 1991. IEEE. |
| [156] |
U. Kebschull and T. Kropf.
Efficient Representation of the Ring-Sum Expansion for
Boolean Verification.
In European Design Automation Conference, Poster Session, 1991. |
| [157] |
T. Kropf, J. Frößl, W. Beller, and T. Giesler.
A Hardware Implementation of a Modified DES-Algorithm.
In EUROMICRO, pages 59-66. North-Holland, August 1990. |
| [158] |
T. Kropf and H.-J. Wunderlich.
Hierarchische Testmustergenerierung für sequentielle
Schaltungen.
In Workshop Testmethoden und Zuverläßigkeit von
Schaltungen und Systemen, Gut Ising, Chiemsee, March 1990. ITG/GI. |
| [159] |
N. Wehn, M. Glesner, K. Gebauer, and T. Kropf.
A New Floorplanning Approach for Hierarchical Macrocell
Design.
In IASTED, 1987. |
This file has been generated by bibtex2html 1.74
