Global ETD Search
Search theses and dissertations gathered from participating repositories worldwide. Every result links back to the library that holds it. No account is needed.
Results
Showing 1 to 20 of 20 for “"SMT Solvers"”.
-
Synthesis of domain specific CNF encoders for bit-vector solvers
SMT solvers are at the heart of a number of software engineering tools. These SMT solvers use a SAT solver as the back-end and convert the high-level constraints given by the user down to low-level boolean formulas that can be efficiently mapped to CNF clauses and fed into a SAT solver. Current SMT …
-
Smten and the art of satisfiability-based search
… (SAT) and Satisfiability Modulo Theories (SMT) have been leveraged in solving a wide variety of important and challenging combinatorial search problems, including automatic test generation, logic synthesis, model checking, program synthesis, and software verification. Though in principle …
-
Predicting SMT solver performance for software verification
… (or “goals”) are proved depends as much on the SMT solver as the properties of the goal itself. In this work, we present a method to use syntactic analysis to characterise goals and predict the most appropriate solver via machine-learning techniques. Combining solvers in this way - a …
-
Nelson Oppen combination as a rewrite theory
Solving Satisfiability Modulo Theories (SMT) problems in a key piece in automating tedious mathematical proofs. It involves deciding satisfiability of formulas of a decidable theory, which can often be reduced to solving systems of equalities and disequalities, in a variety of theories such as …
-
Programming Language Foundations for Packet Processing
… automatic decision procedures that rely on SAT/SMT solvers for a compact trusted computing base.
-
SMT-based bounded model checking of multi-threaded software in embedded systems
… (BMC) based on Satisfiability Modulo Theories (SMT) techniques. We present three major novel contributions. First, we extend the encodings from previous SMT-based bounded model checkers to provide more accurate support for variables of finite bit width, bit-vector operations, arrays, structures, …
-
An Effective SMT Engine for Formal Verification
… exploitation of Satisfiability Modulo Theories (SMT) solvers. In this thesis, we present MathSAT, a modern, efficient SMT solver that provides several important functionalities, and can be used as a workhorse engine in formal verification. We develop novel algorithms for two functionalities which …
-
A Constraint-Based Approach to Reactive Task and Motion Planning
… we employ Satisfiability Modulo Theories (SMT) solvers using a new extension of proof rules for Temporal Property Verification. For efficient policy search, we apply domain-specific heuristics to generalize verification failures. Furthermore, the SMT solver enables quantitative …
-
Verification of Hybrid Systems using Satisfiability Modulo Theories
… systems using Satisfiability Modulo Theories (SMT). SMT is an established technique that has been used successfully in many verification approaches, targeted for both hardware and software systems. The use of SMT to verify hybrid systems has been limited, due to the restricted support of …
-
Planning and Scheduling in Temporally Uncertain Domains
… we show how Satisfiability Modulo Theory (SMT) solvers can be exploited to quickly solve different kinds of query in the realm of scheduling under uncertainty. Finally, we address the problem of temporal planning in domains featuring real-time constraints and actions having duration that is …
-
Formal approaches to security-aware robotic motion planning using hyperproperties
… automata-based and satisfiability modulo theory (SMT)-based model checking methods under HyperTWTL specifications. This is because most existing model-checking verification techniques based on both automata and SMT are limited to the analysis of individual trace executions and, as such, may not be …
-
Optimization Modulo Theories with OptiMathSAT
… Reasoning (AR), Satisfiability Modulo Theories (SMT) is an important discipline that allows for dealing with industrial-level decision problems. Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories with the ability to express, and optimize, objective functions. Recently, …
-
Modular SMT-Based Verification of Rule-Based Hardware Designs
… rule-level abstraction for verification using SMT-based verification, e.g. bounded and unbounded model checking. The main aspect of the rule-level abstraction taken advantage of is the modularity. Rule-level modules can only be interacted with through their interface methods, so if a module …
-
Towards Practical Predicate Analysis
… first-order-logic formulas over predicates using SMT solvers, e.g., predicate abstraction, bounded model checking, k-induction, and lazy abstraction with interpolants. We define a configurable framework for predicate-based analyses that allows expressing each of these approaches. This unifying …
-
Analysis and Design of Symmetric Cryptographic Algorithms
… of NORX which exploit the power of SAT- and SMT-solvers and have the potential to be easily adaptable to other encryption schemes as well.
-
Exploiting SAT and SMT Techniques for Automated Reasoning and Ontology Manipulation in Description Logics
… reach of the freely-available state-of-the-art solvers. As a consequence, many problems have been successfully solved by mean of SAT-based techniques and these approaches are currently state-of-the-art in the respective communities (among all Model Checking). Furthermore, the progress in …
-
Supported Programming for Beginning Developers
… a system for test case generation which uses an SMT solver to generate inputs to reach specified lines in a function, and asks the user what the expected outputs would be for those inputs. The resulting test cases check the correctness of the output, rather than merely ensuring the code does not …
-
Specifying and verifying program transformations with PTRANS
Software developers, compiler designers, and formal methods researchers all stand to benefit from improved tools for compiler design and verification. Program correctness for compiled languages depends fundamentally on compiler correctness, and compiler optimizations are usually not formally …
-
Enabling Rich Lightweight Verification of Rust Software
Rust is a novel programming language that is rapidly gaining adoption in the software industry thanks to its performance and safety properties. Among its strengths, Rust's type system is designed to detect at compile time certain kinds of memory-related bugs, such as dangling pointers and null …
-
Towards eliminating expert creative help in automated reasoning
Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-03-28 without embargo terms