Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure
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 verificat
- PDF / 1,234,940 Bytes
- 175 Pages / 419.528 x 595.276 pts Page_size
- 77 Downloads / 178 Views
VIEWEG+TEUBNER RESEARCH
Christian Herde
Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure Proof Engines for the Analysis of Hybrid Discrete-Continuous Systems With a foreword by Prof. Dr. Martin Fränzle
VIEWEG+TEUBNER RESEARCH
Bibliographic information published by the Deutsche Nationalbibliothek The Deutsche Nationalbibliothek lists this publication in the Deutsche Nationalbibliografie; detailed bibliographic data are available in the Internet at http://dnb.d-nb.de.
Dissertation Universität Oldenburg, 2010
1st Edition 2011 All rights reserved © Vieweg+Teubner Verlag | Springer Fachmedien Wiesbaden GmbH 2011 Editorial Office: Ute Wrasmann | Anita Wilke Vieweg+Teubner Verlag is a brand of Springer Fachmedien. Springer Fachmedien is part of Springer Science+Business Media. www.viewegteubner.de No part of this publication may be reproduced, stored in a retrieval system or transmitted, in any form or by any means, electronic, mechanical, photocopying, recording, or otherwise, without the prior written permission of the copyright holder. Registered and/or industrial names, trade names, trade descriptions etc. cited in this publication are part of the law for trade-mark protection and may not be used free in any form or by any means even if this is not specifically marked. Cover design: KünkelLopka Medienentwicklung, Heidelberg Printed on acid-free paper Printed in Germany ISBN 978-3-8348-1494-4
Foreword
Over the past decades, we have seen a slow, but steady popularization of automatic verification technology — once the Holy Grail of formal methods in computer science — that is indicative of the maturity the field has achieved. Only few universities do still hesitate to expose undergraduates to the field’s basic methods, the pertinent tools, and their underlying algorithms, and industrial takeover is undeniably gaining impetus, following education with the natural phase delay. Over the years, some basic techniques have become cornerstones of the field, forming identifiable and reappearing building blocks of the plethora of tools that have been built. Among these fundamentals are abstract interpretation, binary decision diagrams, and satisfiability solving, to name just a few. Within this book, you will find an informed account of a number of substantial contributions to the latter field, in particular addressing the domain of satisfiability modulo theories, which has become instrumental to various mechanic verification schemes in hardware and software validation. Despite being based on a PhD thesis, which I had the pleasure to advise, the book elaborates in equal detail on the underlying “folklore” ideas and techniques and on the author’s own contributions, complementing both by extensive pointers to open problems and ideas for further research. I hope you as a reader will find it helpful, no matter whether you are a novice trying to understand satisfiability solving for complex-structured arithmetic constraints or are an expert looking for a clear-cut delineation of the techniques d
Data Loading...
