Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure

Proof Engines for the Analysis of Hybrid Discrete-Continuous Systems

  • Book
  • © 2011

Overview

Authors:
  1. Christian Herde
    View author publications

    You can also search for this author in PubMed   Google Scholar

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 (6 chapters)

  1. Front Matter

    Pages I-XVII
    Download chapter PDF

  2. Introduction

    • Christian Herde
    Pages 1-13

  3. Hybrid Dynamical Systems

    • Christian Herde
    Pages 15-35

  4. Extending DPLL for Pseudo-Boolean Constraints

    • Christian Herde
    Pages 37-58

  5. Integration of DPLL-SAT and Linear Programming

    • Christian Herde
    Pages 59-79

  6. Integration of DPLL and Interval Constraint Solving

    • Christian Herde
    Pages 81-131

  7. Conclusion

    • Christian Herde
    Pages 133-144

  8. Back Matter

    Pages 145-163
    Download chapter PDF
Back to top

Keywords

About this book

Due to the growing use of more and more complex computerized systems in safety-critical applications, the formal verification of such systems is increasingly gaining importance. Many automatic and semi-automatic schemes for hardware and software verification ultimately rely on decision procedures for discharging the proof obligations generated during the verification process.

Christian Herde deals with the development of such procedures, providing methods for efficiently solving formulae comprising complex Boolean combinations of linear, polynomial, and transcendental arithmetic constraints, involving thousands of Boolean-, integer-, and real-valued variables. Although aiming at providing tool support for the verification of hybrid discrete-continuous systems, most of the techniques he describes are general purpose and have applications in many other domains, like operations research, planning, software validation, and electronic design automation.

About the author

Dr. Christian Herde completed his doctoral thesis under the supervision of Prof. Dr. Martin Fränzle at the Department of Computing Science at the University of Oldenburg, Germany.

Bibliographic Information

  • Book Title: Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure

  • Book Subtitle: Proof Engines for the Analysis of Hybrid Discrete-Continuous Systems

  • Authors: Christian Herde

  • DOI: https://doi.org/10.1007/978-3-8348-9949-1

  • Publisher: Vieweg+Teubner Verlag Wiesbaden

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

  • Copyright Information: Vieweg+Teubner Verlag | Springer Fachmedien Wiesbaden GmbH, Wiesbaden 2011

  • Softcover ISBN: 978-3-8348-1494-4Published: 10 February 2011

  • eBook ISBN: 978-3-8348-9949-1Published: 29 March 2011

  • Edition Number: 1

  • Number of Pages: XVII, 163

  • Number of Illustrations: 30 b/w illustrations

  • Topics: Theory of Computation, Computer Science, general

Publish with us

Policies and ethics

Back to top

Search

Navigation