Skip to main content
SpringerLink
Log in

Complete Symbolic Simulation of SystemC Models

Efficient Formal Verification of Finite Non-Terminating Programs

  • Book
  • © 2016

Overview

Authors:
  1. Vladimir Herdt

    1. Bremen, Germany

    View author publications

    You can also search for this author in PubMed   Google Scholar

  • Study in Computer Sciences
  • Includes supplementary material: sn.pub/extras

Part of the book series: BestMasters (BEST)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (7 chapters)

  1. Front Matter

    Pages i-xix
    Download chapter PDF

  2. Introduction

    • Vladimir Herdt
    Pages 1-6

  3. Preliminaries

    • Vladimir Herdt
    Pages 7-32

  4. Static Partial Order Reduction in Stateful Model Checking

    • Vladimir Herdt
    Pages 33-40

  5. Dynamic Partial Order Reduction in Stateful Model Checking

    • Vladimir Herdt
    Pages 41-51

  6. State Subsumption Reduction

    • Vladimir Herdt
    Pages 53-68

  7. Heuristic Symbolic Subsumption

    • Vladimir Herdt
    Pages 69-95

  8. Experiments

    • Vladimir Herdt
    Pages 97-115

  9. Back Matter

    Pages 117-162
    Download chapter PDF
Back to top

Keywords

About this book

In his master thesis, Vladimir Herdt presents a novel approach, called complete symbolic simulation, for a more efficient verification of much larger (non-terminating) SystemC programs. The approach combines symbolic simulation with stateful model checking and allows to verify safety properties in (cyclic) finite state spaces, by exhaustive exploration of all possible inputs and process schedulings. The state explosion problem is alleviated by integrating two complementary reduction techniques. Compared to existing approaches, the complete symbolic simulation works more efficiently, and therefore can provide correctness proofs for larger systems, which is one of the most challenging tasks, due to the ever increasing complexity.

Authors and Affiliations

  • Bremen, Germany

    Vladimir Herdt

About the author

Vladimir Herdt is working as Research Assistant in the Group of Computer Architecture at the University of Bremen, where he is pursuing his PhD degree. 

Bibliographic Information

  • Book Title: Complete Symbolic Simulation of SystemC Models

  • Book Subtitle: Efficient Formal Verification of Finite Non-Terminating Programs

  • Authors: Vladimir Herdt

  • Series Title: BestMasters

  • DOI: https://doi.org/10.1007/978-3-658-12680-3

  • Publisher: Springer Vieweg Wiesbaden

  • eBook Packages: Computer Science, Computer Science (R0)

  • Copyright Information: Springer Fachmedien Wiesbaden 2016

  • Softcover ISBN: 978-3-658-12679-7Published: 29 March 2016

  • eBook ISBN: 978-3-658-12680-3Published: 16 March 2016

  • Series ISSN: 2625-3577

  • Series E-ISSN: 2625-3615

  • Edition Number: 1

  • Number of Pages: XIX, 162

  • Number of Illustrations: 26 b/w illustrations

  • Topics: Computer Hardware, Software Engineering/Programming and Operating Systems, Mathematics of Computing

Publish with us

Policies and ethics

Back to top

Search

Navigation