Now showing items 1-14 of 14

    • Bit-vector Support in Z3-str2 Solver and Automated Exploit Synthesis 

      Subramanian, Sanu (University of Waterloo, 2015-11-30)
      Improper string manipulations are an important cause of software defects, which make them a target for program analysis by hackers and developers alike. Symbolic execution based program analysis techniques that systematically ...
    • CDCL(Crypto) and Machine Learning based SAT Solvers for Cryptanalysis 

      Nejati, Saeed (University of Waterloo, 2020-05-15)
      Over the last two decades, we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers over industrial problems from a variety of applications such as ...
    • Combining Static Analysis and Targeted Symbolic Execution for Scalable Bug-finding in Application Binaries 

      Parvez, Muhammad Riyad (University of Waterloo, 2016-05-18)
      Manual software testing is laborious and prone to human error. Yet, it is the most popular method for quality assurance. Automating the test-case generation promises better effectiveness, especially for exposing “deep” ...
    • Computational Methods for Combinatorial and Number Theoretic Problems 

      Bright, Curtis (University of Waterloo, 2017-04-27)
      Computational methods have become a valuable tool for studying mathematical problems and for constructing large combinatorial objects. In fact, it is often not possible to find large combinatorial objects using human ...
    • Domain Knowledge Guided Testing and Training of Neural Networks 

      Nagisetty, Vineel (University of Waterloo, 2021-08-26)
      The extensive impact of Deep Neural Networks (DNNs) on various industrial applications and research areas within the last decade can not be overstated. However, they are also subject to notable limitations, namely their ...
    • Machine Learning for SAT Solvers 

      Liang, Jia (University of Waterloo, 2018-12-07)
      Boolean SAT solvers are indispensable tools in a variety of domains in computer science and engineering where efficient search is required. Not only does this relieve the burden on the users of implementing their own search ...
    • Novel Neural Network Repair Methods for Data Privacy and Individual Fairness 

      Graves, Laura (University of Waterloo, 2021-08-03)
      Machine learning is increasingly becoming critical to the decisions that control our lives. As these predictive models advance toward ubiquity, the demand for models that are trustworthy, fair, and preserve privacy becomes ...
    • Predictive Runtime Verification of Stochastic Systems 

      Babaee Cheshmeahmadrezaee, Reza (University of Waterloo, 2019-08-13)
      Runtime Verification (RV) is the formal analysis of the execution of a system against some properties at runtime. RV is particularly useful for stochastic systems that have a non-zero probability of failure at runtime. ...
    • Security Analysis Methods for Detection and Repair of DoS Vulnerabilities in Smart Contracts 

      Nassirzadeh, Behkish (University of Waterloo, 2021-04-19)
      In recent years we have witnessed a dramatic increase in the applications of blockchain and smart contracts in a variety of contexts, including supply-chain, decentralized finance, and international money transfers. However, ...
    • StringFuzz: A Fuzzer for String SMT Solvers 

      Blotsky, Dmitry (University of Waterloo, 2018-08-10)
      We introduce StringFuzz, a software tool for automatically testing string SMT solvers. String SMT solvers are specialised software tools for solving the Satisfiability Modulo Theories (SMT) problem with string contraints, ...
    • Strong Induction in Hardware Model Checking 

      Vediramana Krishnan, Hari Govind (University of Waterloo, 2019-08-14)
      Symbolic Model checking is a widely used technique for automated verification of both hardware and software systems. Unbounded SAT-based Symbolic Model Checking (SMC) algorithms are very popular in hardware verification. ...
    • Towards a Theoretical Understanding of the Power of Restart in SAT solvers 

      Li, Chunxiao (University of Waterloo, 2019-09-09)
      Restart policy is a widely used class of techniques integral to the efficiency of conflict-driven clause-learning (CDCL) SAT solvers. While the utility of such policies has been well-established, to-date we still lack a ...
    • Understanding and Enhancing CDCL-based SAT Solvers 

      Zulkoski, Edward (University of Waterloo, 2018-08-02)
      Modern conflict-driven clause-learning (CDCL) Boolean satisfiability (SAT) solvers routinely solve formulas from industrial domains with millions of variables and clauses, despite the Boolean satisfiability problem being ...
    • Z3str4: A Solver for Theories over Strings 

      Berzish, Murphy (University of Waterloo, 2021-06-15)
      Satisfiability Modulo Theories (SMT) solvers supporting rich theories of strings have facilitated numerous industrial applications with the need to reason about string operations and predicates that are present in many ...

      UWSpace

      University of Waterloo Library
      200 University Avenue West
      Waterloo, Ontario, Canada N2L 3G1
      519 888 4883

      All items in UWSpace are protected by copyright, with all rights reserved.

      DSpace software

      Service outages