# Browsing by Subject "Theorem proving"

Now showing 1 - 5 of 5

- Results Per Page
1 5 10 20 40 60 80 100

- Sort Options
Ascending Descending

Item Efficient, mechanically-verified validation of satisfiability solvers(2015-05) Wetzler, Nathan David; Hunt, Warren A., 1958-; Heule, Marijn, 1979-; Biere, Armin; Lifschitz, Vladimir; Moore, J Strother; Ramachandran, VijayaShow more Satisfiability (SAT) solvers are commonly used for a variety of applications, including hardware verification, software verification, theorem proving, debugging, and hard combinatorial problems. These applications rely on the efficiency and correctness of SAT solvers. When a problem is determined to be unsatisfiable, how can one be confident that a SAT solver has fully exhausted the search space? Traditionally, unsatisfiability results have been expressed using resolution or clausal proof systems. Resolution-based proofs contain perfect reconstruction information, but these proofs are extremely large and difficult to emit from a solver. Clausal proofs rely on rediscovery of inferences using a limited number of techniques, which typically takes several orders of magnitude longer than the solving time. Moreover, neither of these proof systems has been able to express contemporary solving techniques such as bounded variable addition. This combination of issues has left SAT solver authors unmotivated to produce proofs of unsatisfiability. The work from this dissertation focuses on validating satisfiability solver output in the unsatisfiability case. We developed a new clausal proof format called DRAT that facilitates compact proofs that are easier to emit and capable of expressing all contemporary solving and preprocessing techniques. Furthermore, we implemented a validation utility called DRAT-trim that is able to validate proofs in a time similar to that of the discovery time. The DRAT format has seen widespread adoption in the SAT community and the DRAT-trim utility was used to validate the results of the 2014 SAT Competition. DRAT-trim uses many advanced techniques to realize its performance gains, so why should the results of DRAT-trim be trusted? Mechanical verification enables users to model programs and algorithms and then prove their correctness with a proof assistant, such as ACL2. We designed a new modeling technique for ACL2 that combines efficient model execution with an agile and convenient theory. Finally, we used this new technique to construct a fast, mechanically-verified validation tool for proofs of unsatisfiability. This research allows SAT solver authors and users to have greater confidence in their results and applications by ensuring the validity of unsatisfiability results.Show more Item Formal verification of application and system programs based on a validated x86 ISA model(2016-12) Goel, Shilpi; Hunt, Warren A., 1958-; Alvisi, Lorenzo; Kaufmann, Matt; Lin, Calvin; Moore, J S; Watson, RobertShow more Two main kinds of tools available for formal software verification are point tools and general-purpose tools. Point tools are targeted towards bug-hunting or proving a fixed set of properties, such as establishing the absence of buffer overflows. These tools have become a practical choice in the development and analysis of serious software systems, largely because they are easy to use. However, point tools are limited in their scope because they are pre-programmed to reason about a fixed set of behaviors. In contrast, general-purpose tools,like theorem provers, have a wider scope. Unfortunately, they also have a higher user overhead. These tools often use incomplete and/or unrealistic software models, in part to reduce this overhead. Formal verification based on such a model can be restrictive because it does not account for program behaviors that rely on missing features in the model. The results of such formal verification undertakings may be unreliable --- consequently, they can offer a false sense of security. This dissertation demonstrates that formal verification of complex program properties can be made practical, without any loss of accuracy or expressiveness, by employing a machine-code analysis framework implemented using a mechanical theorem prover. To this end, we constructed a formal and executable model of the x86 Instruction-Set Architecture using the ACL2 theorem-proving system. This model includes a specification of 400+ x86 opcodes and architectural features like segmentation and paging. The model's high execution speed allows it to be validated routinely by performing co-simulations against a physical x86 processor --- thus, formal analysis based on this model is reliable. We also developed a general framework for x86 machine-code analysis that can lower the overhead associated with the verification of a broad range of program properties, including correctness with respect to behavior, security, and resource requirements. We illustrate the capabilities of our framework by describing the verification of two application programs, population count and word count, and one system program, zero copy.Show more Item Parallelizing an interactive theorem prover : functional programming and proofs with ACL2(2012-12) Rager, David Lawrence; Hunt, Warren A., 1958-; Browne, James C; Kaufmann, Matt; Moore, J S; Sawada, Jun; Witchel, EmmettShow more Multi-core systems have become commonplace, however, theorem provers often do not take advantage of the additional computing resources in an interactive setting. This research explores automatically using these additional resources to lessen the delay between when users submit conjectures to the theorem prover and when they receive feedback from the prover that is useful in discovering how to successfully complete the proof of a particular theorem. This research contributes mechanisms that permit applicative programs to execute in parallel while simultaneously preparing these programs for verification by a semi-automatic reasoning system. It also contributes a parallel version of an automated theorem prover, with management of user interaction issues, such as output and how inherently single-threaded, user-level proof features can be configured for use with parallel computation. Finally, this dissertation investigates the types of proofs that are amenable to parallel execution. This investigation yields the result that almost all proof attempts that require a non-trivial amount of time can benefit from parallel execution. Proof attempts executed in parallel almost always provide the aforementioned feedback sooner than if they executed serially, and their execution time is often significantly reduced.Show more Item A verified framework for symbolic execution in the ACL2 theorem prover(2010-12) Swords, Sol Otis; Hunt, Warren A., 1958-; Baumgartner, Jason R.; Boyer, Robert S.; Cook, William; Moore, J S.Show more Mechanized theorem proving is a promising means of formally establishing facts about complex systems. However, in applying theorem proving methodologies to industrial-scale hardware and software systems, a large amount of user interaction is required in order to prove useful properties. In practice, the human user tasked with such a verification must gain a deep understanding of the system to be verified, and prove numerous lemmas in order to allow the theorem proving program to approach a proof of the desired fact. Furthermore, proofs that fail during this process are a source of confusion: the proof may either fail because the conjecture was false, or because the prover required more help from the user in order to reach the desired conclusion. We have implemented a symbolic execution framework inside the ACL2 theorem prover in order to help address these issues on certain problem domains. Our framework introduces a proof strategy that applies bit-level symbolic execution using BDDs to finite-domain problems. This proof strategy is a fully verified decision procedure for such problems, and on many useful problem domains its capacity vastly exceeds that of exhaustive testing. Our framework also produces counterexamples for conjectures that it determines to be false. Our framework seeks to reduce the amount of necessary user interaction in proving theorems about industrial-scale hardware and software systems. By increasing the automation available in the prover, we allow the user to complete useful proofs while understanding less of the detailed implementation of the system. Furthermore, by producing counterexamples for falsified conjectures, our framework reduces the time spent by the user in trying to determine why a proof failed.Show more Item Verifying filesystems for abstract separation logic-based program verification in the ACL2 theorem prover(2021-05-21) Mehta, Mihir Parang; Cook, William Randall; Bornholt, James; Lifschitz, Vladimir; Rossbach, Christopher; Swords, SolShow more The field of filesystem verification has been receiving steady attention from researchers from the filesystem and verification worlds, but some aspects remain unexplored. Considering it important to verify an existing filesystem with the property of binary compatibility - i.e. a filesystem which maintains a disk image in a state that can be read by existing implementations of that filesystem - we develop LoFAT, an efficient implementation of FAT32 in the language of the ACL2 theorem prover. Devising HiFAT, a directory-tree model of FAT32, we prove it to abstract LoFAT. This refinement relationship allows us to quickly prototype a number of filesystem calls in LoFAT, which we later replace with more efficient implementations that retain their correctness properties. We also validate LoFAT by co-simulation against mature implementations of FAT32, namely, the mtools and the Linux implementation of FAT32. Considering it important to support code proofs, i.e. proofs of correctness of programs making use of the filesystem, we develop such proofs for programs interacting with LoFAT. Initially relying on read-over-write properties of LoFAT, we later develop an abstract separation logic layer on top of HiFAT, which abstracts it and therefore abstract LoFAT. This layer, AbsFAT, allows us to concisely represent filesystem states and file operations on them. We show some code proofs that are simplified with the use of AbsFAT. Finally, we investigate the use of abstract separation logic to model concurrent operations on the filesystem. Choosing to focus on single-core concurrency, we use the standard approach which involves an oracle, i.e. an uninterpreted function that decides which of the waiting threads at any moment gets to execute the next instruction. We demonstrate a proof of code correctness based on this model, and conclude with some ideas for future workShow more