Projekte pro Jahr
Abstract
Automatic synthesis of hardware components from declarative specifications is an ambitious endeavor in computer aided design. Existing synthesis algorithms are often implemented with Binary Decision Diagrams (BDDs), inheriting their scalability limitations. Instead of BDDs, we propose several new methods to synthesize finite-state systems from safety specifications using decision procedures for the satisfiability of quantified and unquantified Boolean formulas (SAT-, QBF- and EPR-solvers). The presented approaches are based on computational learning, templates, or reduction to first-order logic. We also present an efficient parallelization, and optimizations to utilize reachability information and incremental solving. Finally, we compare all methods in an extensive case study. Our new methods outperform BDDs and other existing work on some classes of benchmarks, and our parallelization achieves a super-linear speedup.
Originalsprache | englisch |
---|---|
Titel | Verification, Model Checking, and Abstract Interpretation, 15th International Conference |
Redakteure/-innen | Kenneth L. McMillan, Xavier Rival |
Erscheinungsort | Berlin-Heidelberg |
Herausgeber (Verlag) | Springer |
Seiten | 1-20 |
ISBN (Print) | 978-3-642-54012-7 |
DOIs | |
Publikationsstatus | Veröffentlicht - 2014 |
Veranstaltung | International Conference on Verification, Model Checking, and Abstract Interpretation - San Diego, USA / Vereinigte Staaten Dauer: 19 Jan. 2014 → 21 Jan. 2014 |
Publikationsreihe
Name | Lecture Notes in Computer Science |
---|---|
Herausgeber (Verlag) | Springer |
Band | 8318 |
Konferenz
Konferenz | International Conference on Verification, Model Checking, and Abstract Interpretation |
---|---|
Land/Gebiet | USA / Vereinigte Staaten |
Ort | San Diego |
Zeitraum | 19/01/14 → 21/01/14 |
Fields of Expertise
- Information, Communication & Computing
Treatment code (Nähere Zuordnung)
- Application
Fingerprint
Untersuchen Sie die Forschungsthemen von „SAT-Based Synthesis Methods for Safety Specs“. Zusammen bilden sie einen einzigartigen Fingerprint.Projekte
- 4 Abgeschlossen
-
EU - STANCE - A Source code analysis Toolbox for software security AssuraNCE
Tögl, R., Könighofer, R. & Bloem, R.
1/10/12 → 30/09/15
Projekt: Forschungsprojekt
-
FWF - QUAINT - Quant. Entscheidungsprozeduren Interpolation f. Korrektur
Hofferek, G., Könighofer, R. & Bloem, R.
1/01/12 → 30/09/15
Projekt: Forschungsprojekt
-
RiSE - Rigorous Systems Engineering
Könighofer, R., Khalimov, A., Bloem, R., Könighofer, B. & Jacobs, S.
1/03/11 → 31/08/19
Projekt: Forschungsprojekt