47 citations · 53 across the 17 of their papers we have counts for
10 papers · 1 filter
Solving Set Constraints with Comprehensions and Bounded Quantifiers
Mudathir Mohamed, Nick Feng, Andrew Reynolds +3
Many real applications problems can be encoded easily as quantified formulas in SMT. However, this simplicity comes at the cost of difficulty during solving by SMT solvers. Differe…
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
Yicheng Qian, Joshua Clune, Clark Barrett +1
Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide…
Lean-SMT: An SMT tactic for discharging proof goals in Lean
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan +5
Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof ass…
Integer Reasoning Modulo Different Constants in SMT
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor +4
This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving…
Relational Hoare Logic for Realistically Modelled Machine Code
Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee +4
Many security- and performance-critical domains, such as cryptography, rely on low-level verification to minimize the trusted computing surface and allow code to be written directl…
Cubing for Tuning
Haoze Wu, Clark Barrett, Nina Narodytska
We are exploring the problem of building an automated reasoning procedure that adaptively tunes the high-level solving strategy for a given problem. There are two main distinctive…