SMT Solvers for Rodin

2012 ◽  
pp. 194-207 ◽  
Author(s):  
David Déharbe ◽  
Pascal Fontaine ◽  
Yoann Guyot ◽  
Laurent Voisin
Keyword(s):  
Smt Solvers

scholarly journals On the unusual effectiveness of type-aware operator mutations for testing SMT solvers

2020 ◽  
Vol 4 (OOPSLA) ◽  
pp. 1-25
Author(s):  
Dominik Winterer ◽  
Chengyu Zhang ◽  
Zhendong Su
Keyword(s):  
Smt Solvers

scholarly journals Making Automatic Theorem Provers more Versatile

10.29007/n6j7 ◽  
2018 ◽  
Author(s):  
Simon Cruanes
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Research Directions ◽  
First Order ◽  
Theorem Provers ◽  
Smt Solvers ◽  
Automatic Theorem Provers ◽  
Automatic Theorem

We argue that automatic theorem provers should become more versatile and should be able to tackle problems expressed in richer input formats. Salient research directions include (i) developing tight combinations of SMT solvers and first-order provers; (ii) adding better handling of theories in first-order provers; (iii) adding support for inductive proving; (iv) adding support for user-defined theories and functions; and (v) bringing to the provers some basic abilities to deal with logics beyond first-order, such as higher-order logic.

scholarly journals Extending ACL2 with SMT Solvers

2015 ◽  
Vol 192 ◽  
pp. 61-77 ◽  
Author(s):  
Yan Peng ◽  
Mark Greenstreet
Keyword(s):  
Smt Solvers
Sign in / Sign up

Export Citation Format

Share Document