Sol Swords

20 papers A* 1B 3C 2Journal 1Unranked 11
YearRankTypeTitle / Venue / Authors
2025 C conf
Robust, End-to-end Correctness Proofs of Industrial Divide and Square Root RTL Designs.
ARITH
Sol Swords, Cuong Chau
2023 — ed.
Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, TX, USA and online, November 13-14, 2023.
ACL2
Alessandro Coglio, Sol Swords
2021 — conf
Balancing Automation and Control for Formal Verification of Microprocessors.
CAV (1)
Shilpi Goel, Anna Slobodová, Rob Sumners, Sol Swords
2020 — conf
Generating Mutually Inductive Theorems from Concise Descriptions.
ACL2
Sol Swords
2020 — conf
New Rewriter Features in FGL.
ACL2
Sol Swords
2020 B conf
Verifying x86 instruction implementations.
CPP
Shilpi Goel, Anna Slobodová, Rob Sumners, Sol Swords
2019 J jnl
Verifying x86 Instruction Implementations.
CoRR
Shilpi Goel, Anna Slobodová, Rob Sumners, Sol Swords
2018 — conf
Hint Orchestration Using ACL2's Simplifier.
ACL2
Sol Swords
2018 — conf
Incremental SAT Library Integration Using Abstract Stobjs.
ACL2
Sol Swords
2017 — conf
Meta-extract: Using Existing Facts in Meta-reasoning.
ACL2
Matt Kaufmann, Sol Swords
2017 — conf
Term-Level Reasoning in Support of Bit-blasting.
ACL2
Sol Swords
2015 — conf
Fix Your Types.
ACL2
Sol Swords, Jared Davis
2014 B conf
Microcode Verification - Another Piece of the Microprocessor Verification Puzzle.
ITP
Jared Davis, Anna Slobodová, Sol Swords
2013 — conf
Verified AIG Algorithms in ACL2
ACL2
Jared Davis, Sol Swords
2011 C conf
A flexible formal verification framework for industrial scale validation.
MEMOCODE
Anna Slobodová, Jared Davis, Sol Swords, Warren A. Hunt Jr.
2011 — conf
Bit-Blasting ACL2 Theorems
ACL2
Sol Swords, Jared Davis
2010 B conf
A Mechanically Verified AIG-to-BDD Conversion Algorithm.
ITP
Sol Swords, Warren A. Hunt Jr.
2010 — ch.
Use of Formal Verification at Centaur Technology.
Design and Verification of Microprocessor Systems for High-Assurance Applications
Warren A. Hunt Jr., Sol Swords, Jared Davis, Anna Slobodová
2009 A* conf
Centaur Technology Media Unit Verification.
CAV
Warren A. Hunt Jr., Sol Swords
2006 — conf
Soundness of the simply typed lambda calculus in ACL2.
ACL2
Sol Swords, William R. Cook