In recent years, Satisfiability Modulo Theories (SMT) solvers have emerged as powerful tools in many formal methods applications, including verification, automated theorem proving, planning and software synthesis. The expressive power of SMT allows problems from many disciplines to be handled in a single unified approach. While SMT solvers are highly effective at handling certain classes of problems due to highly tuned implementations of efficient ground decision procedures, their ability is often limited when reasoning about universally quantified first-order formulas. Since generally this class of problems is undecidable, most SMT solvers use heuristic techniques for answering unsatisfiable when quantified formulas are present. On the other hand, when the problem is satisfiable, solvers using these techniques will either run indefinitely, or give up after some predetermined amount of effort. In a majority of formal methods applications, it is critical that the SMT solver be able to determine when such a formula is satisfiable, especially when it can return some representation of a model for the formula. This dissertation introduces new techniques for finding models for SMT formulas containing quantified first-order formulas. We will focus our attention on finding finite models, that is, models whose domain elements can be represented as a finite set. We give a procedure that is both finite model complete and refutationally complete for a fragment of first-order logic that occurs commonly in practice.

Automated planning as a satisfiability problem is a method developed in theearly nineties. It has some known disadvantages, such as its inefficient encod-ing of numbers. The field of Satisfiability Modulo Teories tries to connectalready established solvers for e.g. linear constraints into SAT-solvers in orderto make reasoning about numerical values more efficient. This thesis combines planning as satisfiability and SMT to perform efficientreasoning about actions that occupy realistic time in Temporal Action Logic,a formalism developed at Linköping University for reasoning about action andchange.

Due to the continued development of Internet technology, more and more people are willing to take advantage of high-interaction and diverse web applications to deal with commercial, knowledge-sharing, and social activities. However, while web applications deeply affect our society by degrees, hackers start exploiting web application vulnerabilities to attack innocent end user and back-end database, and therefore pose significant threat in information security. According to this situation, this paper proposes a detection mechanism based on Model Checking to detect web application vulnerabilities. We reduce the problem whether the vulnerabilities exist or not to a kind of SMT (Satisfiability Modulo Theories) problem, and analyze all of the traces of tainted data flow in web applications to find possible vulnerabilities by SMT solver. The experimental results show that the method we proposed can identify SQL injection and XSS vulnerabilities effectively, and prove our method is a feasible way to find web application vulnerabilities.

An increasing number of applications in verification and security rely on or could benefit from automatic solvers that can check the satisfiability of constraints over a rich set of data types that includes character strings. Unfortunately, most string solvers today are standalone tools that can reason only about some fragment of the theory of strings and regular expressions, sometimes with strong restrictions on the expressiveness of their input language (such as, length bounds on all string variables). These specialized solvers reduce string problems to satisfiability problems over specific data types, such as bit vectors, or to automata decision problems. On the other side, despite their power and success as back-end reasoning engines, general-purpose Satisfiability Modulo Theories (SMT) solvers so far have provided minimal or no native support for string reasoning. This thesis presents a deductive calculus describing a new algebraic approach that allows solving constraints over the theory of unbounded strings and regular expressions natively, without reduction to other problems. We provide proofs of refutation soundness and solution soundness of our calculus, and solution completeness under a fair proof strategy. Moreover, we show that our calculus is a decision procedure for the theory of regular language membership with length constraints. We have implemented our calculus as a string solver for the theory of (unbounded) strings with concatenation, length, and membership in regular languages, and incorporated it into the SMT solver CVC4 to expand its already large set of built-in theories. This work makes CVC4 the first SMT solver that is able to accept and process a rich set of mixed constraints over strings, integers, reals, arrays and other data types. In addition, our initial experimental results show that, over string problems, CVC4 is highly competitive with specialized string solvers with a comparable input language. We believe that the approach we described in this thesis provides a new idea for string-based formal methods.

abstract: Knowledge representation and reasoning is a prominent subject of study within the field of artificial intelligence that is concerned with the symbolic representation of knowledge in such a way to facilitate automated reasoning about this knowledge. Often in real-world domains, it is necessary to perform defeasible reasoning when representing default behaviors of systems. Answer Set Programming is a widely-used knowledge representation framework that is well-suited for such reasoning tasks and has been successfully applied to practical domains due to efficient computation through grounding--a process that replaces variables with variable-free terms--and propositional solvers similar to SAT solvers. However, some domains provide a challenge for grounding-based methods such as domains requiring reasoning about continuous time or resources. To address these domains, there have been several proposals to achieve efficiency through loose integrations with efficient declarative solvers such as constraint solvers or satisfiability modulo theories solvers. While these approaches successfully avoid substantial grounding, due to the loose integration, they are not suitable for performing defeasible reasoning on functions. As a result, this expressive reasoning on functions must either be performed using predicates to simulate the functions or in a way that is not elaboration tolerant. Neither compromise is reasonable; the former suffers from the grounding bottleneck when domains are large as is often the case in real-world domains while the latter necessitates encodings to be non-trivially modified for elaborations. This dissertation presents a novel framework called Answer Set Programming Modulo Theories (ASPMT) that is a tight integration of the stable model semantics and satisfiability modulo theories. This framework both supports defeasible reasoning about functions and alleviates the grounding bottleneck. Combining the strengths of Answer Set Programming and satisfiability modulo theories enables efficient continuous reasoning while still supporting rich reasoning features such as reasoning about defaults and reasoning in domains with incomplete knowledge. This framework is realized in two prototype implementations called MVSM and ASPMT2SMT, and the latter was recently incorporated into a non-monotonic spatial reasoning system. To define the semantics of this framework, we extend the first-order stable model semantics by Ferraris, Lee and Lifschitz to allow "intensional functions" and provide analyses of the theoretical properties of this new formalism and on the relationships between this and existing approaches. / Dissertation/Thesis / Doctoral Dissertation Computer Science 2016

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:47:31Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:47:47Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:48:08Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Made available in DSpace on 2017-02-07T17:48:08Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) Previous issue date: 2016-09-13 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The software development for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, consumer electronics companies usually invest a lot of resources in fast and automatic verification mechanisms, in order to create robust systems and reduce product recall rates. In addition, further development-time reduction and system robustness can be achieved through cross-platform frameworks, such as Qt, which favor the reliable port of software stacks to different devices. Based on that, the present work proposes a simplified version of the Qt framework, which is integrated into a checker based on satisfiability modulo theories (SMT), name as the efficient SMT-based bounded model checker (ESBMC++), for verifying actual Qt-based applications, and presents a success rate of 89%, for the developed benchmark suite. We also evaluate our simplified version of the Qt framework using other state-of-the-art verifiers for C++ programs and an evaluation about their level of compliance. It is worth mentioning that the proposed methodology is the first one to formally verify Qt-based applications, which has the potential to devise new directions for software verification of portable code. / O desenvolvimento de software para sistemas embarcados tem crescido rapidamente, o que na maioria das vezes acarreta em um aumento da complexidade associada a esse tipo de projeto. Como consequência, as empresas de eletrônica de consumo costumam investir recursos em mecanismos de verificação rápida e automática, com o intuito de desenvolver sistemas robustos e assim reduzir as taxas de recall de produtos. Além disso, a redução no tempo de desenvolvimento e na robustez dos sistemas desenvolvidos podem ser alcançados através de frameworks multi-plataformas, tais como Qt, que oferece um conjunto de bibliotecas (gráficas) confiáveis para vários dispositivos embarcados. Desta forma, este trabalho propõe uma versão simplificada do framework Qt que integrado a um verificador baseado nas teorias do módulo da satisfatibilidade, denominado Efficient SMT-Based Bounded Model Checker (ESBMC++), verifica aplicações reais que ultilizam o Qt, apresentando uma taxa de sucesso de 89%, para os benchmarks desenvolvidos. Com a versão simplificada do framework Qt proposto, também foi feita uma avaliação ultilizando outros verificadores que se encontram no estado da arte para verificação de programas em C++ e uma avalição a cerca de seu nível de conformidade. Dessa maneira, a metodologia proposta se afirma como a primeira a verificar formalmente aplicações baseadas no framework Qt, além de possuir um potencial para desenvolver novas frentes para a verificação de código portátil.

Satisfiability (SAT) and satisfiability modulo theories (SMT) solvers are high-performance automated propositional and first-order theorem provers, used as underlying tools in many formal verification and artificial intelligence systems. Theoretic and engineering advancement of solver technologies improved the performance of modern solvers; however, the increased complexity of those solvers calls for formal verification of those tools themselves. This thesis discusses two methods to formally certify SAT/SMT solvers. The first method is generating proofs from solvers and certifying those proofs. Because new theories are constantly added to SMT solvers, a flexible framework to safely add new inference rules is necessary. The proposal is to use a meta-language called LFSC, which is based on Edinburgh Logical Framework. SAT/SMT logics have been encoded in LFSC, and the encoding can be easily and modularly extended for new logics. It is shown that an optimized LFSC checker can certify SMT proofs efficiently. The second method is using a verified programming language to implement a SAT solver and verify the code statically. Guru is a pure functional programming language with support for dependent types and theorem proving; Guru also allows for efficient code generation by means of resource typing. A modern SAT solver, called versat, has been implemented and verified to be correct in Guru. The performance of versat is shown to be comparable with that of the current proof checking technology.

Many bugs are reported during the software maintenance phase, and in order for asoftware product to have a longer life, it must effectively handle and resolve thesebugs. As a result, when cost and time are considered, a prioritized list of bugs isrequired for all products. Due to some factors, such as user expertise, the numberof bugs, the priority methodology, and how critical the software is, developing a prioritization technique that includes user inputs and preset bug constraints to producea final prioritization list of software bugs is challenging. Our approach to solvingthe prioritization problem involves combining an SMT solver with user interactionto provide the best possible solution. Our findings suggest that this strategy outperforms both random and non-interactive bug prioritization methods.

Prioritization of software requirements is an important part of the requirements engineering process within the industry of software development. There are many different methods for achieving the most optimal order of software requirements, a list that shows in what order the requirements should be implemented. This degree project utilizes the SMT-based solver Z3 for an interactive prioritization algorithm. Previous studies have shown good results with another SMT-based solver called Yices. With the newer Z3 from Microsoft, the results have been improved further, and the tool is based on Python, and the framework for Z3 is called Z3PY. Experiments have been conducted on a set of different software requirements derived from a project in the healthcare industry and show that the Z3 solution is, in general, improving the requirements prioritization compared to other mentioned solutions in the study that has been tested on the same set of requirements. Results show that the Z3 solution outperformed the other SMT-based solution Yices by 2-4% regarding disagreement and by 3% regarding average distance. The results are significantly improved based on an ANOVA test with a p-value <= 0.05.

With the advent of advanced program analysis and constraint solving techniques, several test generation tools use variants of symbolic execution. Symbolic techniques have been shown to be very effective in path-based test generation; however, they fail to scale to large programs due to the exponential number of paths to be explored. In this thesis, we focus on tackling this path explosion problem and propose search strategies to achieve quick branch coverage under symbolic execution, while exploring only a fraction of paths in the program. We present a reachability-guided strategy that makes use of the reachability graph of the program to explore unvisited portions of the program and a conflict driven backtracking strategy that utilizes conflict analysis to perform nonchronological backtracking. We also propose error-directed search strategies, that are aimed at catching bugs in the program faster, by targeting those parts of the program where bugs are likely to be found or those that are hard to reach. We present experimental evidence that these strategies can significantly reduce the search space and improve the speed of test generation for programs. / Master of Science