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 39 articles )

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

1 2 next

  1. Akshay, S.; Chakraborty, Supratik; Goel, Shubham; Kulal, Sumith; Shah, Shetal: Boolean functional synthesis: hardness and practical algorithms (2021)
  2. Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark Barrett: Pono: A Flexible and Extensible SMT-Based Model Checker (2021) not zbMATH
  3. Barkalov, Alexander; Titarenko, Larysa; Mielcarek, Kamil: Improving characteristics of LUT-based mealy FSMs (2020)
  4. 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)
  5. 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)
  6. Kaufmann, Daniela; Biere, Armin; Kauers, Manuel: Incremental column-wise verification of arithmetic circuits using computer algebra (2020)
  7. Luttenberger, Michael; Meyer, Philipp J.; Sickert, Salomon: Practical synthesis of reactive systems from LTL specifications via parity games (2020)
  8. Meuli, Giulia; Soeken, Mathias; Roetteler, Martin; De Micheli, Giovanni: ROS: resource-constrained oracle synthesis for quantum computers (2020)
  9. Temel, Mertcan; Slobodova, Anna; Hunt, Warren A. jun.: Automated and scalable verification of integer multipliers (2020)
  10. Drucker, Nir; Ho, Hsi-Ming; Ouaknine, Joël; Penn, Michal; Strichman, Ofer: Cyclic-routing of unmanned aerial vehicles (2019)
  11. Finkbeiner, Bernd; Gieseking, Manuel; Hecking-Harbusch, Jesko; Olderog, Ernst-Rüdiger: Model checking data flows in concurrent network updates (2019)
  12. Meuli, Giulia; Schmitt, Bruno; Ehlers, Rüdiger; Riener, Heinz; De Micheli, Giovanni: Evaluating ESOP optimization methods in quantum compilation flows (2019)
  13. Shin, Seung Woo; Thachuk, Chris; Winfree, Erik: Verifying chemical reaction network implementations: a pathway decomposition approach (2019)
  14. Kurshan, Robert P.: Transfer of model checking to industrial practice (2018)
  15. Melham, Tom: Symbolic trajectory evaluation (2018)
  16. Ponce de León, Hernán; Mokhov, Andrey: Compact and efficiently verifiable models for concurrent systems (2018)
  17. Yu, Cunxi; Yasin, Atif; Su, Tiankai; Mishchenko, Alan; Ciesielski, Maciej: Rewriting environment for arithmetic circuit verification (2018)
  18. Büscher, Niklas; Franz, Martin; Holzer, Andreas; Veith, Helmut; Katzenbeisser, Stefan: On compiling Boolean circuits optimized for secure multi-party computation (2017)
  19. 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)
  20. Faymonville, Peter; Finkbeiner, Bernd; Rabe, Markus N.; Tentrup, Leander: Encodings of bounded synthesis (2017)

1 2 next