Releasing VDM proof obligations with SMT solvers

Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design - MEMOCODE '17 ◽

10.1145/3127041.3127066 ◽

2017 ◽

Author(s):

Hsin-Hung Lin ◽

Bow-Yaw Wang

Keyword(s):

Smt Solvers

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

Proceedings of the ACM on Programming Languages ◽

10.1145/3428261 ◽

2020 ◽

Vol 4 (OOPSLA) ◽

pp. 1-25

Author(s):

Dominik Winterer ◽

Chengyu Zhang ◽

Zhendong Su

Keyword(s):

Smt Solvers

Integration of SMT-solvers in B and Event-B development environments

Science of Computer Programming ◽

10.1016/j.scico.2011.03.007 ◽

2013 ◽

Vol 78 (3) ◽

pp. 310-326 ◽

Cited By ~ 10

Author(s):

David Déharbe

Keyword(s):

Smt Solvers

Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-Decomposition

Theory and Applications of Satisfiability Testing – SAT 2018 - Lecture Notes in Computer Science ◽

10.1007/978-3-319-94144-8_22 ◽

2018 ◽

pp. 365-382 ◽

Cited By ~ 4

Author(s):

Shubhani Gupta ◽

Aseem Saxena ◽

Anmol Mahajan ◽

Sorav Bansal

Keyword(s):

Equivalence Checking ◽

Program Equivalence ◽

Smt Solvers ◽

Effective Use

Integrating test and proof in the verifiable spark 2014 language using contracts and SMT solvers

2013 IEEE/AIAA 32nd Digital Avionics Systems Conference (DASC) ◽

10.1109/dasc.2013.6719720 ◽

2013 ◽

Author(s):

Tucker Taft

Keyword(s):

Smt Solvers

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants

Tools and Algorithms for the Construction and Analysis of Systems - Lecture Notes in Computer Science ◽

10.1007/11691372_11 ◽

2006 ◽

pp. 167-181 ◽

Cited By ~ 33

Author(s):

Pascal Fontaine ◽

Jean-Yves Marion ◽

Stephan Merz ◽

Leonor Prensa Nieto ◽

Alwen Tiu

Keyword(s):

Proof Assistants ◽

Interactive Proof ◽

Smt Solvers

Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers

Theoretical Aspects of Computing – ICTAC 2018 - Lecture Notes in Computer Science ◽

10.1007/978-3-030-02508-3_15 ◽

2018 ◽

pp. 273-291 ◽

Cited By ~ 1

Author(s):

Martin Jonáš ◽

Jan Strejček

Keyword(s):

Smt Solvers ◽

Bit Vector

System aspmt2smt: Computing ASPMT Theories by SMT Solvers

Logics in Artificial Intelligence - Lecture Notes in Computer Science ◽

10.1007/978-3-319-11558-0_37 ◽

2014 ◽

pp. 529-542 ◽

Cited By ~ 9

Author(s):

Michael Bartholomew ◽

Joohyung Lee

Keyword(s):

Smt Solvers

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.

Algorithmic Verification of Systems Software Using SMT Solvers

Static Analysis - Lecture Notes in Computer Science ◽

10.1007/978-3-642-03237-0_2 ◽

2009 ◽

pp. 2-2 ◽

Cited By ~ 3

Author(s):

Shaz Qadeer

Keyword(s):

Smt Solvers ◽

Systems Software

Extending ACL2 with SMT Solvers

Electronic Proceedings in Theoretical Computer Science ◽

10.4204/eptcs.192.6 ◽

2015 ◽

Vol 192 ◽

pp. 61-77 ◽

Cited By ~ 4

Author(s):

Yan Peng ◽

Mark Greenstreet

Keyword(s):

Smt Solvers