- Publications
-
- Generating and Exploiting Automated Reasoning Proof Certificates
Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
Communications of ACM
Published
by ACM
- Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Journal of Automated Reasoning
Published
by Springer
- Combining Stable Infiniteness and (Strong) Politeness
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Journal of Automated Reasoning
Published
by Springer
-
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness
Guilherme Toledo, Yoni Zohar, Clark Barrett
Proceedings of CADE'2023
Published
by Springer
-
Combining Finite Combination Properties: Finite Models and Busy Beavers
Guilherme Toledo, Yoni Zohar, Clark Barrett
Proceedings of FroCos'2023
Published
by Springer
-
Formal Verification of Bit-Vector Invertibility Conditions in Coq
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
Proceedings of FroCos'2023
Published
by Springer
-
DNN Verification, Reachability, and the Exponential Function Problem
Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz
Proceedings of CONCUR'2023
Published
by Schloss Dagstuhl
- Flexible Proof Production in an Industrial-Strength SMT Solver
Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark Barrett
Proceedings of IJCAR'2022
Published
by Springer
- Reasoning About Vectors Using an SMT Theory of Sequences.
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark Barrett, Cesare Tinelli
Proceedings of IJCAR'2022
Published
by Springer
- Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices.
Ori Lahav and Yoni Zohar
Proceedings of IJCAR'2022
Published
by Springer
- Polite Combination of
Algebraic Datatypes
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal
Fontaine, Clark Barrett
Journal of Automated Reasoning
Published
by Springer
- cvc5: A Versatile and
Industrial-Strength SMT Solver
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer,
Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed,
Aina Niemetz, Andres Notzli, Alex Ozdemir, Mathias Preiner, Andrew
Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar
Best Tool Paper Award
Proceedings of TACAS'2022
Published
by Springer
- Bit-Precise Reasoning via
Int-Blasting
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Notzli,
Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare
Tinelli
Proceedings of VMCAI'2022
Published
by Springer
- Politeness and Stable
Infiniteness: Stronger Together
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds,
Clark Barrett, Cesare Tinelli
Proceedings of CADE'2021
Published
by Springer
- Towards Satisfiability
Modulo Parametric Bit-vectors
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark
Barrett, Cesare Tinelli
Journal of Automated Reasoning
Published by Springer
- Smt-Switch: A
Solver-Agnostic C++ API for SMT Solving
Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan,
Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli,
Clark Barrett
Proceedings of SAT'2021
Published by Springer
- The Move Prover
Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp,
Sam Blackshear, Junkil Park, Yoni Zohar, Clark Barrett, David L.
Dill
Proceedings of CAV'2020
Published
by Springer
- Politeness for the Theory
of Algebraic Datatypes
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal
Fontaine, Clark Barrett
Best Paper Award
Proceedings of IJCAR'2020
Published
by Springer
- Modal extension of ideal
paraconsistent four-valued logic and its subsystem
Norihiro Kamide and Yoni Zohar
Annals of Pure and Applied Logic, 2020
Published by elsevier
- Towards
Bit-Width-Independent Proofs in SMT Solvers
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark
Barrett, Cesare Tinelli
Proceedings of CADE'2019
Published
by Springer
- DRAT-based Bit-Vector
Proofs in CVC4
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark
Barrett
Proceedings of SAT'2019
Published
by Springer
- Verifying Bit-vector
Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett, Cesare
Tinelli
PxTP'2019
Published
by EPTCS
- Pure Sequent Calculi:
Analyticity and Decision Procedure
Ori Lahav and Yoni Zohar
Transactions on Computational Logic, 2019
Published by
ACM
- Automating Automated
Reasoning: The Case of Two Generic Automated Reasoning
Tools
Yoni Zohar, Dmitry Tishkovsky, Renate A. Schmidt, Anna
Zamansky
Description Logic, Theory Combination, and All That, 2019
Published
by Springer
- Towards Automated Reasoning
in Herbrand Structures
Liron Cohen, Reuben N S Rowe, Yoni Zohar
Journal of Logic and Computation, 2019
Published by Oxford University Press
- Finite Model Property for
Modal Ideal Paraconsistent Four-Valued Logic
Norihiro Kamide and Yoni Zohar
Proceedings of ISMVL'2019
Published by IEEE Xplore
- Completeness and
Cut-Elimination for First-Order Ideal Paraconsistent Four-Valued
Logic
Norihiro Kamide and Yoni Zohar
Studia Logica, 2019
Published by
Springer
- Rexpansions of
Non-deterministic Matrices and Their Applications in Non-classical
Logics
Arnon Avron and Yoni Zohar
Review of Symbolic Logic, 2018
Published by Cambridge University Press
- Yet another paradefinite
logic: The role of conflation
Norihiro Kamide and Yoni Zohar
Logic Journal of the IGPL, 2018
Published by Oxford University Press
- From the Subformula
Property to Cut-Admissibility in Propositional Sequent
Calculi
Ori Lahav and Yoni Zohar
Journal of Logic and Computation, 2018
Published by Oxford University Press
- Online Detection of
Effectively Callback Free Objects with Applications to Smart
Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky,
Noam Rinetzky, Mooly Sagiv, Yoni Zohar
Proceedings of POPL'2018
Published by
ACM
- Reasoning Inside The Box:
Deduction in Herbrand Logics
Liron Cohen, Yoni Zohar
Proceedings of GCAI'2017
Published by
EasyChair Publications
- Cut-Admissibility as a
Corollary of the Subformula Property
Ori Lahav and Yoni Zohar
Best Paper Award
Proceedings of TABLEAUX'2017
Published
by SpringerLink
- Sequent
Systems for Negative Modalities
Ori Lahav, João Marcos, Yoni Zohar
Logica Universalis, 2017
Published
by SpringerLink
- Non-deterministic
Matrices in Action: Expansions, Refinements, and
Rexpansions
Arnon Avron and Yoni Zohar
Proceedings of ISMVL'2017
Published by IEEE
Xplore
- It ain't necessarily so:
Basic Sequent Systems for Negative Modalities
Ori Lahav, João Marcos, Yoni Zohar
Proceedings of AIML'2016
Published by
College Publications
- Gen2sat: An Automated
Tool for Deciding Derivability in Analytic Pure Sequent
Calculi
Yoni Zohar and Anna Zamansky
Proceedings of IJCAR'2016
Published
by SpringerLink
- `Mathematical’ does not
mean `Boring’: integrating software assignments to enhance learning
of logico-mathematical concepts
Anna Zamansky and Yoni Zohar
Proceedings of Cognise'2016
Published
by SpringerLink
- SAT-based Decision
Procedure for Analytic Pure Sequent Calculi
Ori Lahav and Yoni Zohar
Proceedings of IJCAR'2014
Published
by SpringerLink
- On the Construction of
Analytic Sequent Calculi for Sub-classical Logics
Ori Lahav and Yoni Zohar
Proceedings of WoLLIC'2014
Published
by SpringerLink
- Theses
-