Project Abstract

Formal verification is a crucial step in ensuring the correctness and reliability of software and hardware systems. Satisfiability Modulo Theories (SMT) solving is a key component of formal verification, enabling the determination of whether a given formula or logical expression can be satisfied. However, existing SMT solvers face challenges in terms of efficiency, scalability, and accuracy, leading to increased verification time and reduced accuracy. The research proposes the development of an efficient SMT solver that leverages novel algorithms and techniques to improve the performance and accuracy of formal verification. The proposed SMT solver aims to address the limitations of existing solvers, enabling faster and more accurate verification of complex systems. The aim of the research is to design and implement an SMT solver that can efficiently handle large and complex formulas, while providing accurate results. The SMT solver will be evaluated on various benchmarks and case studies to demonstrate its effectiveness. The research has led to the development of an SMT solver that outperforms existing solvers in terms of efficiency and scalability. The SMT solver has been applied to various formal verification tasks, resulting in significant reductions in verification time (up to 50%) and improvements in accuracy (up to 20%). Additionally, the SMT solver has been able to handle previously unsolvable formulas, demonstrating its ability to tackle complex verification tasks. The research has demonstrated the effectiveness of our proposed SMT solver in improving the efficiency and accuracy of formal verification. Findings have important implications for the development of reliable software and hardware systems, and contribute to the advancement of formal verification techniques. The proposed solver has the potential to significantly reduce verification time and improve accuracy, enabling the development of more complex and reliable systems.

Keywords: Evaluation, Handling Complexity, Challenges Addressed

 Conference Details

Session: Presentation Stream 4 at Presentation Slot 9

Location: GH001 at Tuesday 7th 13:30 – 17:00

Markers: Neil Carter, Lu Zhang

Course: MSc Advanced Computer Science, Masters PG

Future Plans: I’m looking for work