ABC: An Academic Industrial-Strength Verification Tool. ABC is a public-domain system for logic synthesis and formal verification of binary logic circuits appearing in synchronous hardware designs. ABC combines scalable logic transformations based on And-Inverter Graphs (AIGs), with a variety of innovative algorithms. A focus on the synergy of sequential synthesis and sequential verification leads to improvements in both domains. This paper introduces ABC, motivates its development, and illustrates its use in formal verification.

References in zbMATH (referenced in 36 articles )

Showing results 1 to 20 of 36.
Sorted by year (citations)

1 2 next

  1. Bian, Zhengbing; Chudak, Fabian; Macready, William; Roy, Aidan; Sebastiani, Roberto; Varotti, Stefano: Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results (2020)
  2. Drechsler, Rolf (ed.); Soeken, Mathias (ed.): Advanced Boolean techniques. Selected papers from the 13th international workshop on Boolean problems, Bremen, Germany, September 19--21, 2018 (2020)
  3. Kaufmann, Daniela; Biere, Armin; Kauers, Manuel: Incremental column-wise verification of arithmetic circuits using computer algebra (2020)
  4. Luttenberger, Michael; Meyer, Philipp J.; Sickert, Salomon: Practical synthesis of reactive systems from LTL specifications via parity games (2020)
  5. Temel, Mertcan; Slobodova, Anna; Hunt, Warren A. Jr.: Automated and scalable verification of integer multipliers (2020)
  6. Drucker, Nir; Ho, Hsi-Ming; Ouaknine, Joël; Penn, Michal; Strichman, Ofer: Cyclic-routing of unmanned aerial vehicles (2019)
  7. Finkbeiner, Bernd; Gieseking, Manuel; Hecking-Harbusch, Jesko; Olderog, Ernst-Rüdiger: Model checking data flows in concurrent network updates (2019)
  8. Meuli, Giulia; Schmitt, Bruno; Ehlers, Rüdiger; Riener, Heinz; De Micheli, Giovanni: Evaluating ESOP optimization methods in quantum compilation flows (2019)
  9. Shin, Seung Woo; Thachuk, Chris; Winfree, Erik: Verifying chemical reaction network implementations: a pathway decomposition approach (2019)
  10. Kurshan, Robert P.: Transfer of model checking to industrial practice (2018)
  11. Melham, Tom: Symbolic trajectory evaluation (2018)
  12. Ponce de León, Hernán; Mokhov, Andrey: Compact and efficiently verifiable models for concurrent systems (2018)
  13. Yu, Cunxi; Yasin, Atif; Su, Tiankai; Mishchenko, Alan; Ciesielski, Maciej: Rewriting environment for arithmetic circuit verification (2018)
  14. Büscher, Niklas; Franz, Martin; Holzer, Andreas; Veith, Helmut; Katzenbeisser, Stefan: On compiling Boolean circuits optimized for secure multi-party computation (2017)
  15. Chakraborty, Supratik; Khasidashvili, Zurab; Seger, Carl-Johan H.; Gajavelly, Rajkumar; Haldankar, Tanmay; Chhatani, Dinesh; Mistry, Rakesh: Symbolic trajectory evaluation for word-level verification: theory and implementation (2017)
  16. Faymonville, Peter; Finkbeiner, Bernd; Rabe, Markus N.; Tentrup, Leander: Encodings of bounded synthesis (2017)
  17. Könighofer, Bettina; Alshiekh, Mohammed; Bloem, Roderick; Humphrey, Laura; Könighofer, Robert; Topcu, Ufuk; Wang, Chao: Shield synthesis (2017)
  18. Lonsing, Florian; Seidl, Martina; Van Gelder, Allen: The QBF Gallery: behind the scenes (2016)
  19. Schlaipfer, Matthias; Weissenbacher, Georg: Labelled interpolation systems for hyper-resolution, clausal, and local proofs (2016)
  20. Soeken, Mathias; Mishchenko, Alan; Petkovska, Ana; Sterin, Baruch; Ienne, Paolo; Brayton, Robert K.; De Micheli, Giovanni: Heuristic NPN classification for large functions using AIGs and LEXSAT (2016)

1 2 next