Erscheinungsdatum: 08/2007, Medium: Buch, Einband: Gebunden, Titel: SAT-Based Scalable Formal Verification Solutions, Autor: Ganai, Malay // Gupta, Aarti, Verlag: Springer-Verlag GmbH // Springer US, Sprache: Englisch, Schlagworte: EDV // Theorie // Software-Entw // Software Engineering // Elektrotechnik // Bauelement // elektronisch // Baustein // Elektronik // Bauelemente // Schaltung // Grundschaltung // Standardschaltung // CAD // Computer Aided Design // Informatik // Datenverarbeitung // Anwendungen // Betrieb // Verwaltung // CAM // Computer Aided Manufacturing // Computer-Aided Design // Unternehmensanwendungen // Computerunterstützte Fertigung, Rubrik: Anwendungs-Software, Seiten: 330, Reihe: Series on Integrated Circuits and Systems, Informationen: Gb, Gewicht: 719 gr, Verkäufer: averdo
The verification of systems to guarantee their correct behavior is discussed in this book. The mainly applied algorithmic method is the model checking technique combined with algorithms for solving the satisfiability problem (short: SAT). SAT-based verification of discrete systems has become one of the most effective technique within the last 10 years, such that industrial as well as academic applications heavily rely on it. The book covers the whole range of a SAT-based tool application. We propose extensions and concepts that concentrate on the core of a SAT-solver. However, these proposals are then transferred to novel verification models. Moreover, we describe approaches that incorporate the structure of the problem to exploit knowledge gained during the verification process on the level of the SAT-solver. The main focus of the book is on the verification of incomplete system designs, which occur for example in the early phase of a design. We describe various SAT-based modeling concepts that vary regarding their expressiveness and computational resources. The proposed methods are evaluated experimentally to guarantee their applicability in practice.
This book constitutes the proceedings of the 11th International Symposium on NASA Formal Methods, NFM 2019, held in Houston, TX, USA, in May 2019.The 20 full and 8 short papers presented in this volume were carefully reviewed and selected from 102 submissions. The papers focus on formal verification, including theorem proving, model checking, and static analysis, advances in automated theorem proving including SAT and SMT solving, use of formal methods in software and system testing, run-time verification, techniques and algorithms for scaling formal methods, such as abstraction and symbolic methods, compositional techniques, as well as parallel and/or distributed techniques, code generation from formally verified models, safety cases and system safety, formal approaches to fault tolerance, theoretical advances and empirical evaluations of formal methods techniques for safety-critical systems, including hybrid and embedded systems, formal methods in systems engineering and model-based development, correct-by-design controller synthesis, formal assurance methods to handle adaptive systems.
This book constitutes the refereed proceedings of the 26th International Symposium on Model Checking Software, SPIN 2019, held in Beijing, China, in July 2019.The 11 full papers presented and 2 demo-tool papers, were carefully reviewed and selected from 29 submissions. Topics covered include formal verification techniques for automated analysis of software, formal analysis for modeling languages, such as UML/state charts, formal specification languages, temporal logic, design-by-contract, model checking, automated theorem proving, including SAT and SMT, verifying compilers, abstraction and symbolic execution techniques, and much more.