Kombination formaler und semiformaler Techniken zur Verifikation von C-basierten Systembeschreibungen

• Applicant: Professor Dr. Thomas Kropf
• Subject Area: Software Engineering and Programming Languages
• Term: from 2002 to 2008
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5372288

• Final Report Year: 2008

Final Report Abstract

No abstract available

Publications

• A Visual Approach to Validating System Level Designs. In Proceedings of the 15th international symposium on System Synthesis (ISSS02), Kyoto, Japan, October 2002
  Jochen Klose, Thomas Kropf, Jürgen Ruf
  
• Combination of Simulation and Formal Verification. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV02), Tübingen, Shaker Verlag, Februar 2002
  Jürgen Ruf, Thomas Kropf
  
• Bounded property checking with symbolic simulation. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV03), Bremen, Shaker Verlag, Februar 2003
  Jürgen Ruf, Prakash M. Peranandam
  
• Optimized Temporal Logic Compilation, in Journal on Universal Computer Science (J.UCS). Special Issue on Tools for System Design and Verification, February 2003, Springer Verlag Heidelberg
  Andreas Krebs and J. Ruf
  
• Using Symbolic Simulation for Bounded Property Checking. In Forum on Specification and Design Languages 2003 (FDL03), Frankfurt am Main, September 2003
  Jürgen Ruf, Prakash M. Peranandam, Thomas Kropf, Wolfgang Rosenstiel
  
• Dynamic guiding of bounded property checking. In IEEE International High Level Design Validation and Test Workshop 2004 (HLDVT04), Sonoma Valley, California, USA, November 2004
  Prakash M. Peranandam, Roland J. Weiss, Jürgen Ruf, Thomas Kropf, Wolfgang Rosenstiel
  
• Transactional level verification and coverage metrics by means of symbolic simulation. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV04), Shaker Verlag, Kaiserslautern, Februar 2004
  Prakash M. Peranandam, Roland Weiss, Jürgen Ruf, Thomas Kropf
  
• Efficient and customizable integration of temporal properties into SystemC. In Forum on Specification and Design Languages 2005 (FDL05), Lausanne, Schweiz, September 2005
  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 (HLDVT05), Napa Valley, California, USA, November 2005
  Prakash M. Peranandam, Pradeep K. Nalla, Roland J. Weiss, Jürgen Ruf, Thomas Kropf, Wolfgang Rosenstiel
  
• Parallel bounded property checking with SymC. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV05), München, Februar 2005
  Pradeep K. Nalla, Roland J. Weiss, Jürgen Ruf, Thomas Kropf, Wolfgang Rosenstiel
  
• Symbolic bounded property checking in parallel. In 4th International Workshop on Parallel and Distributed Methods in Verification (PDMC05), Lissabon, Portugal. Electronic Notes in Theoretical Computer Science, Elsevier, 2005
  Pradeep K. Nalla, Roland J. Weiss, Prakash Peranandam, Juergen Ruf, Thomas Kropf, Wolfgang Rosenstiel
  
• Symbolic model checking and simulation with temporal assertions. In Pierre Boulet, Editor, Advances in Design arid Specification Languages for SoCs - Selected Contributions from FDL'04. Springer, September 2005
  Roland J. Weiss, Jürgen Ruf, Thomas Kropf, and Wolfgang Rosenstiel
  
• Temporal properties verification of system level design. In Net.Object Days 2005, Workshop on Object Oriented Software Design for Real Time and Embedded Computer Systems, Erfurt, September 2005
  Djones Lettnin, Roland J. Weiss, Axel Braun, Jürgen Ruf, Wolfgang Rosenstiel
  
• Automatic Generation of Verification Properties for SoC Design from SysML-Diagram. In 3rd International UML for SoC Design Workshop at DAC'06 (UML-SoC06), Juli 2006
  Stefan Lämmermann, Roland J. Weiss, Jürgen Ruf, Thomas Kropf and Wolfgang Rosenstiel
  
• Automatische Eigenschaftsextraktion auf Systemebene aus SystemC Modellen. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV06), Dresden, Februar 2006
  Stefan Lämmermann, Roland J. Weiss, Jürgen Ruf, Thomas Kropf and Wolfgang Rosenstiel
  
• Efficient and customizable integration of temporal properties into SystemC. In Alain Vachoux, Editor, Advances in Design and Specification Languages for SoCs - Selected Contributions from FDL'05, Springer, September 2006
  Roland J. Weiss, Jürgen Ruf, Thomas Kropf, and Wolfgang Rosenstiel
  
• Fast Falsification Based on Symbolic Bounded Property Checking. In IEEE International Design an Automation Conference 2006 (DAC06), San Francisco, California, USA, Juli 2006
  Prakash M. Peranandam, Pradeep K. Nalla, Jürgen Ruf, Roland J. Weiss, Thomas Kropf and Wolfgang Rosenstiel
  
• Monitoring-based Formal Hardware Verification. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV06), Dresden, Februar 2006
  Paul Duplys, Roland J. Weiss, Jürgen Ruf, Thomas Kropf, and Wolfgang Rosenstiel
  
• Optimization of System Traversal by Exploiting Static Information of Partitioned Transition Relation, Dissertation, Wilhelm-Schickard -Institut, Universität Tübingen, Dezember 2006
  Prakash Mohan Pernanandam
  
• SystemC Temporal Checker, Technischer Bericht, ISSN 0946-3852, Wilhelm-Schickard-Institut, Universität Tübingen, November 2006
  Jürgen Ruf, Roland Weiss, Djones Lettnin, Stefan Lämmermann, Thomas Kröpf und Wolfgang Rosenstiel
  
• Coverage Driven Verification applied to Embedded Software. In IEEE Computer Society Annual Symposium on VLSI (ISVLSI07), Porto Alegre, Brazil, Mai 2007
  Djones Lettnin, Markus Winterholer, Axel Braun, Joachim Gerlach, Jürgen Ruf, Thomas Kropf and Wolfgang Rosenstiel
  
• Semiformal Verification of Temporal Properties in Embedded Software. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV07), Erlangen, Germany, März 2007
  Djones Lettnin, Pradeep Nalla, Jürgen Ruf, Roland Weiss, Axel Braun, Joachim Gerlach, Thomas Kropf amd Wolfgang Rosenstiel
  
• Efficient Distributed Bounded Property Checking, Wilhelm-Schickard-Institut,Univer$itäl Tübingen
  Pradeep Kumar Nalla
  
• SymC Manual, Technischer Bericht, Wilhelm-Schickard-Institut, Universität Tübingen, Februar 2008
  Jürgen Ruf, Prakash Penanandram, Pradeep Nalla, Stefan Lämmermann, Djones Lettnin, Jörg Behrend, Thomas Kropf und Wolfgang Rosenstiel