Browsing Engineering (Faculty of) by Supervisor "Ganesh, Vijay"
Now showing items 1-8 of 8
-
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” ... -
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 ... -
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. ... -
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 ...