Polite Combination of Algebraic Datatypes by Sheng, Ying, Zohar, Yoni, Ringeissen, Christophe, Lange, Jane, Fontaine, Pascal, Barrett, Clark

“…Abstract Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. …”
Get full text

Trigger Selection Strategies to Stabilize Program Verifiers by Leino, K. Rustan M., Pit-Claudel, Clement F.

“…SMT-based program verifiers often suffer from the so-called butterfly effect, in which minor modifications to the program source cause significant instabilities in verification times, which in turn may lead to spurious verification failures and a degraded user experience. …”
Get full text
Get full text

Trigger Selection Strategies to Stabilize Program Verifiers by Leino, K. Rustan M., Pit-Claudel, Clément

“…SMT-based program verifiers often suffer from the so-called butterfly effect, in which minor modifications to the program source cause significant instabilities in verification times, which in turn may lead to spurious verification failures and a degraded user experience. …”
Get full text
Get full text

SyGuS-Comp 2017: Results and Analysis by Alur, Rajeev, Fisman, Dana, Singh, Rishabh, Solar-Lezama, Armando

“…Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis Competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. …”
Get full text

Stepwise refinement of heap-manipulating code in Chalice by Leino, K. Rustan M., Yessenov, Kuat T

“…This paper describes a system with automated tool support for refinement, powered by a state-of-the-art verification engine that uses an SMT solver. Unlike previous refinement systems, users of the presented system interact only via declarations in the programming language. …”
Get full text
Get full text

A fully verified container library by Tschannen, Julian, Furia, Carlo A., Polikarpova, Nadezhda

“…Keywords: Deductive verification; SMT; Object-oriented software; Containers; AutoProof…”
Get full text
Get full text

SyGuS-Comp 2016: Results and Analysis by Alur, Rajeev, Fisman, Dana, Singh, Rishabh, Solar-Lezama, Armando

“…Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis Competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. …”
Get full text

Alloy*: a general-purpose higher-order relational constraint solver by Milicevic, Aleksandar, Near, Joseph P, Kang, Eunsuk, Jackson, Daniel

“…Some tasks, however, most notably those involving synthesis, are inherently higher order; these are typically handled by embedding a first-order solver (such as a SAT or SMT solver) in a domain-specific algorithm. Using strategies similar to those used in such algorithms, we show how to extend a first-order solver (in this case Kodkod, a model finder for relational logic used as the engine of the Alloy Analyzer) so that it can handle quantifications over higher-order structures. …”
Get full text

A language for automatically enforcing privacy policies

“…We have implemented Jeeves as a Scala library using an SMT solver as a model finder. In this paper we describe the dynamic and static semantics of Jeeves and the properties about policy enforcement that the semantics guarantees. …”
Get full text

TiML: a functional language for practical complexity analysis with invariants by Chlipala, Adam, Wang, Peng, Want, Di

“…The programmer provides type annotations, and the typechecker generates verification conditions that are discharged by an SMT solver. Type and index inference are supported to lower annotation burden, and, furthermore, big-O complexity can be inferred from recurrences generated during typechecking by a recurrence solver based on heuristic pattern matching (e.g. using the Master Theorem to handle divide-and-conquer-like recurrences). …”
Get full text

CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives by Kuepper, Joel, Erbsen, Andres, Gross, Jason, Conoly, Owen, Sun, Chuyue, Tian, Samuel, Wu, David, Chlipala, Adam, Chuengsatiansup, Chitchanok, Genkin, Daniel, Wagner, Markus, Yarom, Yuval

“…On the formal-verification side, we connect to the Fiat Cryptography framework (which translates functional programs into C-like IR code) and extend it with a new formally verified program-equivalence checker, incorporating a modest subset of known features of SMT solvers and symbolic-execution engines. The overall prototype is quite practical, e.g. producing new fastest-known implementations of finite-field arithmetic for both Curve25519 (part of the TLS standard) and the Bitcoin elliptic curve secp256k1 for the Intel 12��ℎ and 13��ℎ generations.…”
Get full text

Verification of microarchitectural refinements in rule-based systems by Dave, Nirav H., Katelman, Michael, King, Myron Decker, Mithal, Arvind

Get full text
Get full text
Get full text

Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations by Chowdhury, Rezaul, Itzhaky, Shachar, Singh, Rohit, Solar Lezama, Armando, Yessenov, Kuat T, Lu, Yongquan, Leiserson, Charles E

“…These transformations formalize the divide-and conquer technique; a visualization interface helps users to interactively guide the process, while an SMT-based back-end verifies each step and takes care of low-level reasoning required for parallelism. …”
Get full text
Get full text
Get full text
Get full text
Get full text