Browsing Engineering (Faculty of) by Supervisor "Ganesh, Vijay"
Now showing items 1-15 of 15
-
AlphaSMT: A Reinforcement Learning Guided SMT Solver
(University of Waterloo, 2023-06-19)Satisfiability Modulo Theories (SMT) solvers are programs that decide whether a first-order logic formula is satisfiable. Over the last two decades, these solvers have become central to many methods and tools in fields as ... -
Bit-vector Support in Z3-str2 Solver and Automated Exploit Synthesis
(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
(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
(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” ... -
Domain Knowledge Guided Testing and Training of Neural Networks
(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 ... -
Generative Adversarial Networks for ECG generation, translation, imputation and denoising
(University of Waterloo, 2022-08-30)Artificial Intelligence is increasingly being used in medical applications. One challenge present in AI in medicine is not having high quality datasets available for training machine learning models. In this work, I explore ... -
Machine Learning for SAT Solvers
(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
(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
(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. ... -
Prioritized Unit Propagation and Extended Resolution Techniques for SAT Solvers
(University of Waterloo, 2023-08-29)NP-complete problems like the Boolean Satisfiability (SAT) Problem are ubiquitous in computer science, mathematics, and engineering. Consequently, researchers have developed algorithms such as Conflict-Driven Clause-Learning ... -
Security Analysis Methods for Detection and Repair of DoS Vulnerabilities in Smart Contracts
(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
(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
(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
(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 ... -
Z3str4: A Solver for Theories over Strings
(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 ...